Conditional assembly of the unit-slack theorem

This module states the δ = 1 specialization of the paper's main result in terms of three structural inputs. The reduction and extremal construction are fully discharged: Theorem 2.1, the simplex/exponential identification of (2.1), and the α = 0 centroid-halfspace inequality are the only inputs.

theorem Feige.sharp_unit_slack_feige_of_paper_inputs {n : ℕ} (hcal : UniversalCalibration dirichletK) (hid : SimplexExponentialIdentification n) (hcentroid : SimplexCentroidHalfspaceProperty) : IsOptimalFixedDimensionalFeigeBound n (sharpConstant n)

The δ = 1 specialization of Theorem 1.1, assembled from Theorem 2.1 and the two geometric facts identifying and bounding the Dirichlet statistic.