Sharp light sources characterization of ellipsoids by flat shadow boundaries

### What is the conjecture
Let $K \subset \mathbb{R}^n$, $n \geq 3$, be a convex body with boundary $\partial K$ of class $C^3$. A point light source $u \in \mathbb{R}^n \setminus K$ creates a **shadow boundary** on $K$ consisting of all points of tangency of rays emanating from $u$ to $K$. The shadow boundary is called **flat** if it is contained in an affine hyperplane.

A set of at least $d$ points in a $d$-dimensional affine space is in general linear position with respect to $p$ if no $d$ of them lie in an affine hyperplane passing through $p$.

The author proves that if every boundary point $p \in \partial K$ admits $L(n)$ point light sources on the tangent hyperplane $T_p \partial K$ in general linear position with respect to $p$ that create flat shadow boundaries, then $K$ must be an ellipsoid, where $L(n) = n+2$ for $n \ge 4$. Furthermore, the unit ball of $\ell_p^n$ ($p > 1, p \neq 2$) demonstrates that $n$ light sources are not sufficient. The sharp minimal number of light sources is conjectured to be $n+1$:

**Conjecture (Zawalski, 2026):** Let $K \subset \mathbb{R}^n$, $n \geq 3$, be a convex body with boundary of class $C^3$. Suppose that for every point $p \in \partial K$, there are at least $n+1$ point light sources on the tangent hyperplane $T_p \partial K$ in a general linear position with respect to $p$ that create flat shadow boundaries on $K$. Then $K$ is an ellipsoid.

* **Source Paper:** *On flat shadow boundaries from point light sources and the characterization of ellipsoids* ([arXiv:2603.29130](https://arxiv.org/abs/2603.29130), [HTML](https://arxiv.org/html/2603.29130), [PDF](https://arxiv.org/pdf/2603.29130))
* **Authors:** Bartłomiej Zawalski
* **In-Paper Location:** [Conjecture (top of page)](https://arxiv.org/pdf/2603.29130v1#page=20) in Section 3 "Bounds on the number of point light sources"
* **OpenConjecture ID:** 1383 ([OpenConjecture](https://github.com/davisrbr/conjectures-arxiv))

### Prerequisites needed
Smooth hypersurfaces, convexity, affine independence, and quadratic forms are supported in Mathlib4:
* Differentiable and $C^k$ functions: [`Mathlib.Analysis.Calculus.ContDiff.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ContDiff/Basic.html)
* Convex sets: [`Mathlib.Analysis.Convex.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Convex/Basic.html)
* Inner product spaces: [`Mathlib.Analysis.InnerProductSpace.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/Basic.html)
* Affine independence and general position: [`Mathlib.LinearAlgebra.AffineSpace.Independent`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/AffineSpace/Independent.html)
* Quadratic forms and ellipsoids: [`Mathlib.LinearAlgebra.QuadraticForm.Basic`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/QuadraticForm/Basic.html)

### Choose either option
- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

This issue was generated by an AI agent and reviewed by me.