ZonotopeBridge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Generic bridge from a proved directional projection-volume formula to the explicit zonotope. The brightness formula is an explicit hypothesis of these helper lemmas; no final counterexample theorem assumes it.

theorem OAI.ProjectionCounterexample.projectionBody_eq_zonotope line 19
Source documentation
A unit-direction brightness formula identifies the actual projection body.
```
theorem projectionBody_eq_zonotope {d : ℕ} (P : Set (E d)) (c : ℝ) (hc : 0 < c)
    (hbrightness : ∀ u : E d, ‖u‖ = 1 →
      projectionVolume P u = c * DiagonalZonotope.support (WithLp.ofLp u)) :
    projectionBody P = DiagonalZonotope.euclidean c := by
…
```
Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.projectionVolume, OAI.DiagonalZonotope.support, OAI.ProjectionCounterexample.projectionBody, OAI.DiagonalZonotope.euclidean
theorem OAI.ProjectionCounterexample.projection_zonotope_is_body_and_attains line 46
Source documentation
The brightness hypothesis gives both a genuine body and support attainment.
```
theorem projection_zonotope_is_body_and_attains {d : ℕ} (P : Set (E d))
    (c : ℝ) (hc : 0 < c)
    (hbrightness : ∀ u : E d, ‖u‖ = 1 →
      projectionVolume P u = c * DiagonalZonotope.support (WithLp.ofLp u)) :
    IsConvexBody (projectionBody P) ∧
      ∀ u : E d, ‖u‖ = 1 → ∃ x ∈ projectionBody P, ⟪u, x⟫ = projectionVolume P u := by
…
```
Mentions: OAI.ProjectionCounterexample.E, OAI.ProjectionCounterexample.projectionVolume, OAI.DiagonalZonotope.support, OAI.ProjectionCounterexample.IsConvexBody, OAI.ProjectionCounterexample.projectionBody