Exact affine metric barrier for two pairs of facet-normal rays
ProvedHirsch.affine_pair_conditioning_optimumFor every real 0<e<1 and every positive definite Gram matrix G=[[X,Z],[Z,Y]], let s_1^2=e^2(XY-Z^2)/(X(X+2eZ+e^2Y)) and s_2^2=e^2(XY-Z^2)/(Y(Y+2eZ+e^2X)). These are the squared sines between a and a+e b, and between b and b+e a, for linearly independent vectors a,b with Gram matrix G. Then min(s_1^2,s_2^2)<=e^2 for EVERY such G, and equality is attained by X=Y=1,Z=-e. Thus choosing an arbitrary invertible affine coordinate change cannot make both pairs better separated than e. The target is this exact algebraic metric optimum. Realization as genuine facets of a simple octagon and higher-dimensional products, the graph-diameter formula, and diagonal gain-graph recognition are separately justified in the accompanying research note, not silently part of the Lean statement.
import Mathlib set_option autoImplicit false
theorem Hirsch.affine_pair_conditioning_optimum (e : ℝ) (he : 0 < e) (he1 : e < 1) :
(∀ X Y Z : ℝ, 0 < X → 0 < Y → Z ^ 2 < X * Y →
min (e ^ 2 * (X * Y - Z ^ 2) /
(X * (X + 2 * e * Z + e ^ 2 * Y)))
(e ^ 2 * (X * Y - Z ^ 2) /
(Y * (Y + 2 * e * Z + e ^ 2 * X))) ≤ e ^ 2) ∧
∃ X Y Z : ℝ, 0 < X ∧ 0 < Y ∧ Z ^ 2 < X * Y ∧
min (e ^ 2 * (X * Y - Z ^ 2) /
(X * (X + 2 * e * Z + e ^ 2 * Y)))
(e ^ 2 * (X * Y - Z ^ 2) /
(Y * (Y + 2 * e * Z + e ^ 2 * X))) = e ^ 2 := by sorry