Centered polar of the cyclic polytope C(n,d)
DefinitionHirsch_cyclic_polarFor , the cyclic polytope is the convex hull of the moment-curve points , . Its centered polar is the H-polytope
where is the centroid of the moment-curve points (an interior point of , so the polar is well-defined and the polytope is bounded). It is a simple -polytope with exactly facets; its vertices correspond to the facets of (determined by Gale's evenness condition), and its graph is the dual graph of .
This family is the vehicle for a referee-verified diameter bound (cyclic_polar_hirsch) and its balanced-range exactness (cyclic_polar_diameter_balanced): it is the correct supporting construction for the campaign's Hirsch-type results on cyclic polars, established after an earlier draft (thin_cone_separator_conductance) was found to cite this same research file for an unrelated, unsupported wedge/solid-angle claim and was dropped rather than published.
Formalization Note momentPt n d i uses i : Fin n as the 1-based index i.val+1; momentCentroid is the arithmetic mean of the n moment points; cyclicPolarA/cyclicPolarB are the row normals/right-hand-sides fed to the mission's shared Hpoly constructor.
import Mathlib
import Definitions.Def_Hirsch_model
/-!
# Polars of cyclic polytopes as explicit H-polytopes
For `n > d`, the cyclic polytope `C(n, d)` is the convex hull of the `n` points
`p_i = (i, i^2, …, i^d)` on the moment curve, `1 ≤ i ≤ n`. Its facets are determined
by Gale's evenness condition. The **centered polar** is the H-polytope
`cyclicPolar n d = { x ∈ ℝ^d : ⟨p_i − c, x⟩ ≤ 1 for all i }`,
where `c` is the vertex centroid, an interior point. It is a simple `d`-polytope with
exactly `n` facets whose vertices correspond to the facets of `C(n, d)`; its graph is the
dual graph of the cyclic polytope. (Campaign notes `attempt_thin.md`, Lemma 1.)
-/
namespace Hirsch
/-- The moment-curve point `(i, i^2, …, i^d)` for `i : Fin n` (1-based). -/
noncomputable def momentPt (n d : ℕ) (i : Fin n) : EuclideanSpace ℝ (Fin d) :=
WithLp.toLp 2 (fun j : Fin d => ((i.val + 1 : ℕ) : ℝ) ^ (j.val + 1))
/-- The vertex centroid of the `n` moment-curve points. -/
noncomputable def momentCentroid (n d : ℕ) : EuclideanSpace ℝ (Fin d) :=
(1 / (n : ℝ)) • ∑ i : Fin n, momentPt n d i
/-- Normals of the centered polar: `p_i − c`. -/
noncomputable def cyclicPolarA (n d : ℕ) : Fin n → EuclideanSpace ℝ (Fin d) :=
fun i => momentPt n d i - momentCentroid n d
/-- Right-hand sides of the centered polar: all equal to `1`. -/
noncomputable def cyclicPolarB (n d : ℕ) : Fin n → ℝ := fun _ => 1
/-- The centered polar of the cyclic polytope `C(n, d)`. -/
noncomputable def cyclicPolar (n d : ℕ) : Set (EuclideanSpace ℝ (Fin d)) :=
Hpoly (cyclicPolarA n d) (cyclicPolarB n d)
end Hirsch