IndisputableMonolith.Geometry.FourTetSignedDeficit

   1import Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
   2import Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
   3import IndisputableMonolith.Geometry.CayleyMengerPolynomial
   4import IndisputableMonolith.Geometry.CayleyMengerMatrix
   5import IndisputableMonolith.Geometry.DihedralCayleyMenger
   6import IndisputableMonolith.Geometry.DihedralDerivatives
   7
   8/-!
   9# Signed Regge Deficit Angles on a Four-Tetrahedron Hinge Star (THEOREM tier)
  10
  11This module produces the first kernel-checked signed Regge-convention deficit
  12angles on an ABSTRACT four-tet star in the repository: an explicit one-parameter
  13family of hinge configurations whose star-local deficit is strictly positive for
  14one parameter sign and strictly negative for the other, in the weak-field regime,
  15with explicit mesh bounds.  "Abstract star" means the object is squared-edge data
  16for four congruent tetrahedra around a common hinge, certified nondegenerate by
  17the Cayley-Menger sign (cm3 > 0); it is not an encoded `Triangulation3D` instance
  18and no coordinate embedding of the closed 4-cycle link is formalized here.
  19
  20## Configuration (panel-locked design)
  21
  22Four congruent tetrahedra share an interior hinge edge AB in a closed 4-cycle link.
  23Each tetrahedron (A, B, P, Q) carries squared edges |AB|^2 = l, |AP|^2 = |BP|^2 =
  24|AQ|^2 = |BQ|^2 = m, |PQ|^2 = p.  In the repository edge convention (vertex 0 = A,
  25vertex 1 = B, vertices 2, 3 the equatorial pair) this is the squared-edge vector
  26(a0, a1, a2, a3, a4, a5) = (l, m, m, m, m, p), and the hinge AB is edge 0.
  27
  28By congruence all four dihedral angles at AB are equal, with common cosine q given
  29by the repository's Cayley-Menger cofactor formula `dihedralCos3Sq`.  PROSE
  30COMMENTARY (offline sympy derivation, NOT kernel-checked in this generality): for
  31general (l, m, p) the cofactors are C34 = -l(l - 4m + 2p), C33 = C44 = l(l - 4m),
  32giving
  33
  34  q(l, m, p) = (l - 4m + 2p) / (l - 4m).
  35
  36The KERNEL-CHECKED case is the slice l = m = 1 proved in
  37`fourTet_centralDihedralCosine`: q(p) = (3 - 2p)/3, with sanity anchor
  38q(1) = 1/3, the regular tetrahedron (`fourTet_regular_sanity`).
  39
  40At l = m = 1 the flat value is p0 = 3/2 (where q = 0 and theta = pi/2 exactly,
  41closing the 4-cycle flat).  The deformation family p(h) = (3/2)(1 - h) gives
  42q = h on the nose, hence
  43
  44  deficit(h) = 2*pi - 4*arccos(h) = 4*arcsin(h),
  45
  46so the SIGN of the deficit is certified by the sign of the rational quantity q = h:
  47no arccos evaluation, no interval arithmetic, no native_decide.
  48
  49## Main results (all THEOREM tier, kernel checked, zero sorry, zero new axioms)
  50
  51* `fourTet_centralDihedralCosine`: the hinge dihedral cosine equals (3 - 2p)/3.
  52* `fourTet_regular_sanity`: q = 1/3 at p = 1 (regular tetrahedron anchor).
  53* `fourTet_nondegenerate`: cm3 > 0 for |h| < 1 (the Cayley-Menger nondegeneracy
  54  certificate; a coordinate embedding is not formalized here).
  55* `fourTet_deficit_eq`: star deficit = 2*pi - 4*arccos(q).
  56* `fourTet_deficit_sign`: 0 < q implies 0 < deficit; q < 0 implies deficit < 0.
  57* `fourTet_weak_pair`: the weak-field certificate at q = +h^2 and q = -h^2 with
  58  mesh bound (all squared edges <= 3), cm3-nondegeneracy, opposite-signed
  59  deficits, and magnitude bound |deficit| <= 2*pi*h^2.
  60* `even_ledger_cannot_match_signed_regge`: a standalone algebraic parity fact
  61  (no even function of the deformation parameter can match the signed deficit
  62  family on a punctured interval); see its docstring for the disclosure of how
  63  it relates to the ledger no-go without importing it.
  64
  65## Convention note (NOT a triangulation bridge)
  66
  67`ReggeActionConcrete.deficitAngle` is defined as 2*pi minus the sum over incident
  68tetrahedra of `dihedralAngle3Sq` applied to squared-edge data.  This module's
  69star-local deficit follows the same 2*pi - sum convention with the same
  70`DihedralDerivatives.dihedralAngle3Sq` on the same kind of squared-edge data;
  71`starDeficit_convention_note` records the trivial constant-sum rewrite that makes
  72this explicit.  It does NOT instantiate `ReggeActionConcrete.deficitAngle` on an
  73encoded `Triangulation3D` object; that instantiation remains future work.
  74
  75## Import firewall
  76
  77Imports are Mathlib plus Geometry modules only.  No ledger, Cost, SevenGaps, or
  78Gravity module is imported, and no flatness assumption (in particular not
  79`FlatConfiguration.flat_deficit_zero`) is used anywhere.
  80
  81## Scope
  82
  83This is an existence certificate for signed weak-field deficits in Regge classes;
  84it is not a statement about the N=5 periodic Freudenthal torus.
  85
  86Two further scoping disclosures.  First, realizability: the formalized
  87nondegeneracy statement is the Cayley-Menger sign certificate cm3 > 0 for each
  88tetrahedron; the existence of a coordinate embedding of the tetrahedra (and of
  89the closed 4-cycle link around the hinge) is standard given cm3 > 0 but is not
  90formalized in this file.  Second, quantifier domains: several theorems below are
  91stated over all real parameters because they are true as algebraic identities in
  92that generality; the geometric reading applies only on the nondegenerate range
  93(|h| < 1, equivalently 0 < p < 3), as flagged in the individual docstrings.
  94-/
  95
  96namespace IndisputableMonolith
  97namespace Geometry
  98namespace FourTetSignedDeficit
  99
 100open CayleyMengerPolynomial CayleyMengerMatrix DihedralCayleyMenger
 101
 102noncomputable section
 103
 104/-! ## The four-tet star squared-edge data -/
 105
 106/-- Squared-edge data of one tetrahedron of the four-tet star with hinge
 107squared length 1, spoke squared lengths 1, and rim squared length `p`:
 108(a0, a1, a2, a3, a4, a5) = (1, 1, 1, 1, 1, p).  The hinge AB is edge 0. -/
 109def starSq (p : ℝ) : SqEdges :=
 110  fun e =>
 111    match e with
 112    | ⟨0, _⟩ => 1
 113    | ⟨1, _⟩ => 1
 114    | ⟨2, _⟩ => 1
 115    | ⟨3, _⟩ => 1
 116    | ⟨4, _⟩ => 1
 117    | ⟨5, _⟩ => p
 118    | ⟨n + 6, h⟩ => absurd h (by omega)
 119
 120/-- The rim squared length along the deformation family: p(h) = (3/2)(1 - h).
 121The flat value is p(0) = 3/2, where the hinge dihedral cosine vanishes. -/
 122def starP (h : ℝ) : ℝ := 3 / 2 * (1 - h)
 123
 124/-- THEOREM: the Cayley-Menger polynomial of the star tetrahedron is
 1252p(3 - p), strictly positive exactly on the open rim range 0 < p < 3.
 126Scoping note: this is a polynomial identity, stated (and true) for all real p;
 127the geometric reading applies only where cm3 > 0. -/
 128theorem star_cm3 (p : ℝ) : cm3 (starSq p) = 2 * p * (3 - p) := by
 129  have h0 : starSq p 0 = 1 := rfl
 130  have h1 : starSq p 1 = 1 := rfl
 131  have h2 : starSq p 2 = 1 := rfl
 132  have h3 : starSq p 3 = 1 := rfl
 133  have h4 : starSq p 4 = 1 := rfl
 134  have h5 : starSq p 5 = p := rfl
 135  unfold cm3
 136  rw [h0, h1, h2, h3, h4, h5]
 137  ring
 138
 139/-- THEOREM (nondegeneracy certificate): for |h| < 1 the star tetrahedron has
 140strictly positive Cayley-Menger polynomial, cm3 > 0.  This is the standard
 141determinantal certificate for realizability as a Euclidean tetrahedron; the
 142coordinate embedding itself is not formalized in this file. -/
 143theorem fourTet_nondegenerate (h : ℝ) (hh : |h| < 1) :
 144    0 < cm3 (starSq (starP h)) := by
 145  have hb := abs_lt.mp hh
 146  rw [star_cm3]
 147  have hp : 0 < starP h := by unfold starP; nlinarith [hb.2]
 148  have hq : starP h < 3 := by unfold starP; nlinarith [hb.1]
 149  nlinarith
 150
 151/-! ## Cayley-Menger cofactors of the star tetrahedron at the hinge
 152
 153The hinge AB is edge 0; `oppositeCMVertices 0 = (3, 4)`.  The three cofactors
 154needed by `dihedralCos3Sq` are computed explicitly, mirroring the normal-form
 155minor technique of `CayleyMengerMatrix`. -/
 156
 157/-- Normal form of the (3,4) Cayley-Menger minor of the star tetrahedron. -/
 158def starMinor34Matrix (p : ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
 159  !![(0 : ℝ), 1, 1, 1;
 160     1, 0, 1, 1;
 161     1, 1, 0, 1;
 162     1, 1, 1, p]
 163
 164theorem det_starMinor34 (p : ℝ) :
 165    Matrix.det (starMinor34Matrix p) = 2 * p - 3 := by
 166  unfold starMinor34Matrix
 167  rw [Matrix.det_succ_row_zero]
 168  simp [Fin.sum_univ_succ, Matrix.det_fin_three, Fin.succAbove]
 169  ring
 170
 171theorem star_minor_34_eq (p : ℝ) :
 172    Matrix.submatrix (cmMatrix3 (starSq p)) (Fin.succAbove (3 : Fin 5))
 173      (Fin.succAbove (4 : Fin 5)) = starMinor34Matrix p := by
 174  ext i j
 175  fin_cases i <;> fin_cases j <;>
 176    simp [starMinor34Matrix, cmMatrix3, starSq, Fin.succAbove]
 177
 178/-- THEOREM: the off-diagonal hinge cofactor C34 of the star tetrahedron. -/
 179theorem star_cofactor_34 (p : ℝ) :
 180    cmCofactor3 (starSq p) 3 4 = 3 - 2 * p := by
 181  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 182  simp [show ¬ Even (7 : Nat) by norm_num]
 183  rw [star_minor_34_eq, det_starMinor34]
 184  ring
 185
 186theorem star_minor_33_eq (p : ℝ) :
 187    Matrix.submatrix (cmMatrix3 (starSq p)) (Fin.succAbove (3 : Fin 5))
 188      (Fin.succAbove (3 : Fin 5)) = regularUnitDiagMinorMatrix := by
 189  ext i j
 190  fin_cases i <;> fin_cases j <;>
 191    simp [regularUnitDiagMinorMatrix, cmMatrix3, starSq, Fin.succAbove]
 192
 193/-- THEOREM: the diagonal cofactor C33 of the star tetrahedron. -/
 194theorem star_cofactor_33 (p : ℝ) :
 195    cmCofactor3 (starSq p) 3 3 = -3 := by
 196  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 197  simp [show Even (6 : Nat) by norm_num]
 198  rw [star_minor_33_eq, det_regularUnitDiagMinorMatrix]
 199
 200theorem star_minor_44_eq (p : ℝ) :
 201    Matrix.submatrix (cmMatrix3 (starSq p)) (Fin.succAbove (4 : Fin 5))
 202      (Fin.succAbove (4 : Fin 5)) = regularUnitDiagMinorMatrix := by
 203  ext i j
 204  fin_cases i <;> fin_cases j <;>
 205    simp [regularUnitDiagMinorMatrix, cmMatrix3, starSq, Fin.succAbove]
 206
 207/-- THEOREM: the diagonal cofactor C44 of the star tetrahedron. -/
 208theorem star_cofactor_44 (p : ℝ) :
 209    cmCofactor3 (starSq p) 4 4 = -3 := by
 210  unfold cmCofactor3 cmCofactorSign3 cmMinor3
 211  simp [show Even (8 : Nat) by norm_num]
 212  rw [star_minor_44_eq, det_regularUnitDiagMinorMatrix]
 213
 214/-- THEOREM: the cofactor denominator at the hinge is the constant 3. -/
 215theorem star_denom (p : ℝ) : dihedralDenom3 (starSq p) 0 = 3 := by
 216  unfold dihedralDenom3
 217  simp only [oppositeCMVertices]
 218  rw [star_cofactor_33, star_cofactor_44]
 219  rw [show ((-3 : ℝ) * (-3 : ℝ)) = (3 : ℝ) ^ 2 by norm_num]
 220  exact Real.sqrt_sq (by norm_num)
 221
 222/-! ## The rational hinge dihedral cosine -/
 223
 224/-- THEOREM (the rational certificate): the dihedral cosine at the hinge AB,
 225computed by the repository's Cayley-Menger cofactor formula `dihedralCos3Sq`,
 226equals the explicit rational function (3 - 2p)/3 of the rim squared length.
 227This is the kernel-checked l = m = 1 slice of the prose-only general formula
 228q(l, m, p) in the module header.  Scoping note: stated for all real p as an
 229identity of the cofactor formula; the dihedral-angle reading applies on the
 230nondegenerate range 0 < p < 3. -/
 231theorem fourTet_centralDihedralCosine (p : ℝ) :
 232    dihedralCos3Sq (starSq p) 0 = (3 - 2 * p) / 3 := by
 233  unfold dihedralCos3Sq
 234  simp only [oppositeCMVertices]
 235  rw [star_cofactor_34, star_denom]
 236
 237/-- THEOREM (sanity anchor): at p = 1 the star tetrahedron is regular and the
 238hinge dihedral cosine is 1/3, matching `dihedralCos3_regularUnit`. -/
 239theorem fourTet_regular_sanity : dihedralCos3Sq (starSq 1) 0 = 1 / 3 := by
 240  rw [fourTet_centralDihedralCosine]
 241  norm_num
 242
 243/-- THEOREM: along the deformation family p(h) = (3/2)(1 - h) the hinge
 244dihedral cosine equals the deformation parameter h exactly.  Scoping note:
 245stated for all real h as an identity; a cosine reading requires |h| <= 1 and
 246the nondegenerate geometric range is |h| < 1. -/
 247theorem star_q (h : ℝ) : dihedralCos3Sq (starSq (starP h)) 0 = h := by
 248  rw [fourTet_centralDihedralCosine]
 249  unfold starP
 250  ring
 251
 252/-! ## The star-local deficit -/
 253
 254/-- Star-local Regge deficit at the hinge AB: 2*pi minus the sum of the four
 255equal dihedral angles of the congruent incident tetrahedra, each computed by
 256the repository's `DihedralDerivatives.dihedralAngle3Sq` on the star data. -/
 257def starDeficit (h : ℝ) : ℝ :=
 258  2 * Real.pi - 4 * DihedralDerivatives.dihedralAngle3Sq (starSq (starP h)) 0
 259
 260/-- Convention note (a trivial constant-sum rewrite, NOT a triangulation
 261bridge): this records that the standalone `starDeficit` follows the same
 2622*pi - sum-over-incident-tetrahedra convention, with the same
 263`DihedralDerivatives.dihedralAngle3Sq`, as `ReggeActionConcrete.deficitAngle`.
 264It does NOT instantiate `ReggeActionConcrete.deficitAngle` on an encoded
 265`Triangulation3D` object; that instantiation remains future work. -/
 266theorem starDeficit_convention_note (h : ℝ) :
 267    starDeficit h =
 268      2 * Real.pi -
 269        ∑ _τ : Fin 4, DihedralDerivatives.dihedralAngle3Sq (starSq (starP h)) 0 := by
 270  unfold starDeficit
 271  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
 272  norm_num
 273
 274/-- THEOREM: the star deficit equals 2*pi - 4*arccos(q) with q = h the
 275rational hinge cosine. -/
 276theorem fourTet_deficit_eq (h : ℝ) :
 277    starDeficit h = 2 * Real.pi - 4 * Real.arccos h := by
 278  unfold starDeficit DihedralDerivatives.dihedralAngle3Sq
 279  rw [star_q]
 280
 281/-- THEOREM: closed arcsin form of the star deficit. -/
 282theorem starDeficit_eq_arcsin (h : ℝ) :
 283    starDeficit h = 4 * Real.arcsin h := by
 284  rw [fourTet_deficit_eq, Real.arccos_eq_pi_div_two_sub_arcsin]
 285  ring
 286
 287/-- THEOREM: the deficit vanishes at the flat value h = 0 (p = 3/2). -/
 288theorem starDeficit_flat : starDeficit 0 = 0 := by
 289  rw [starDeficit_eq_arcsin, Real.arcsin_zero]
 290  ring
 291
 292/-- THEOREM: the star deficit is an odd function of the deformation
 293parameter, deficit(-h) = -deficit(h). -/
 294theorem starDeficit_odd (h : ℝ) : starDeficit (-h) = -starDeficit h := by
 295  rw [starDeficit_eq_arcsin, starDeficit_eq_arcsin, Real.arcsin_neg]
 296  ring
 297
 298/-- THEOREM (the signed-deficit contact certificate): the sign of the star
 299deficit is the sign of the rational hinge cosine q = h.  A strictly positive
 300q gives a strictly positive deficit, a strictly negative q gives a strictly
 301negative deficit.  Scoping note: stated for all real h (arcsin is constant
 302beyond [-1, 1], so the statement stays true); the geometric reading applies
 303on the nondegenerate range |h| < 1. -/
 304theorem fourTet_deficit_sign (h : ℝ) :
 305    (0 < h → 0 < starDeficit h) ∧ (h < 0 → starDeficit h < 0) := by
 306  constructor
 307  · intro hp
 308    rw [starDeficit_eq_arcsin]
 309    have := Real.arcsin_pos.mpr hp
 310    linarith
 311  · intro hn
 312    rw [starDeficit_eq_arcsin]
 313    have := Real.arcsin_lt_zero.mpr hn
 314    linarith
 315
 316/-! ## Weak-field magnitude bounds -/
 317
 318/-- Chord bound for arcsin on the nonnegative unit interval:
 319arcsin(x) <= (pi/2) * x. -/
 320private theorem arcsin_le_pi_div_two_mul (x : ℝ) (h0 : 0 ≤ x) (h1 : x ≤ 1) :
 321    Real.arcsin x ≤ Real.pi / 2 * x := by
 322  have hy0 : 0 ≤ Real.arcsin x := Real.arcsin_nonneg.mpr h0
 323  have hy1 : Real.arcsin x ≤ Real.pi / 2 := Real.arcsin_le_pi_div_two x
 324  have hsin : Real.sin (Real.arcsin x) = x := Real.sin_arcsin (by linarith) h1
 325  have hkey : 2 / Real.pi * Real.arcsin x ≤ Real.sin (Real.arcsin x) :=
 326    Real.mul_le_sin hy0 hy1
 327  rw [hsin] at hkey
 328  have hpi : (0 : ℝ) < Real.pi := Real.pi_pos
 329  have hexp : Real.pi / 2 * (2 / Real.pi * Real.arcsin x) = Real.arcsin x := by
 330    field_simp
 331  have hmul := mul_le_mul_of_nonneg_left hkey
 332    (by positivity : (0 : ℝ) ≤ Real.pi / 2)
 333  rw [hexp] at hmul
 334  exact hmul
 335
 336/-- Absolute chord bound for arcsin on the closed unit interval. -/
 337private theorem abs_arcsin_le_abs (x : ℝ) (hx : |x| ≤ 1) :
 338    |Real.arcsin x| ≤ Real.pi / 2 * |x| := by
 339  rcases le_or_gt 0 x with hx0 | hx0
 340  · rw [abs_of_nonneg hx0, abs_of_nonneg (Real.arcsin_nonneg.mpr hx0)]
 341    exact arcsin_le_pi_div_two_mul x hx0 (by rwa [abs_of_nonneg hx0] at hx)
 342  · have hx1 : -x ≤ 1 := by
 343      rw [abs_of_neg hx0] at hx
 344      linarith
 345    rw [abs_of_neg hx0, abs_of_neg (Real.arcsin_lt_zero.mpr hx0)]
 346    rw [← Real.arcsin_neg]
 347    exact arcsin_le_pi_div_two_mul (-x) (by linarith) hx1
 348
 349/-- THEOREM (weak-field magnitude): |deficit(h)| <= 2*pi*|h| for |h| <= 1. -/
 350theorem starDeficit_abs_le (h : ℝ) (hh : |h| ≤ 1) :
 351    |starDeficit h| ≤ 2 * Real.pi * |h| := by
 352  rw [starDeficit_eq_arcsin, abs_mul]
 353  have hbound := abs_arcsin_le_abs h hh
 354  rw [show |(4 : ℝ)| = 4 by norm_num]
 355  linarith
 356
 357/-- THEOREM (mesh bound): every squared edge of the star tetrahedron is at
 358most 3 for |h| <= 1. -/
 359theorem star_mesh_bound (h : ℝ) (hh : |h| ≤ 1) (e : Fin 6) :
 360    starSq (starP h) e ≤ 3 := by
 361  have hb := abs_le.mp hh
 362  have hp : starP h ≤ 3 := by unfold starP; nlinarith [hb.1]
 363  fin_cases e
 364  · show (1 : ℝ) ≤ 3; norm_num
 365  · show (1 : ℝ) ≤ 3; norm_num
 366  · show (1 : ℝ) ≤ 3; norm_num
 367  · show (1 : ℝ) ≤ 3; norm_num
 368  · show (1 : ℝ) ≤ 3; norm_num
 369  · exact hp
 370
 371/-! ## The weak-field pair certificate -/
 372
 373/-- THEOREM (the weak-field signed pair, Test B certificate): for every
 3740 < h < 1 the pair of configurations at rim parameters p0 - (3/2)h^2 and
 375p0 + (3/2)h^2 (that is, deformation parameters +h^2 and -h^2, with
 376p0 = 3/2 the flat value) satisfies:
 377
 3781. explicit rational hinge cosines q = +h^2 and q = -h^2;
 3792. strictly positive deficit on the first, strictly negative on the second;
 3803. exact antisymmetry, deficit(-h^2) = -deficit(+h^2);
 3814. mesh bound: all squared edges of both configurations are at most 3;
 3825. nondegeneracy certificate: cm3 > 0 for both configurations (the
 383   Cayley-Menger sign; a coordinate embedding is not formalized here);
 3846. weak-field magnitude bound |deficit| <= 2*pi*h^2 on both sides. -/
 385theorem fourTet_weak_pair (h : ℝ) (h0 : 0 < h) (h1 : h < 1) :
 386    dihedralCos3Sq (starSq (starP (h ^ 2))) 0 = h ^ 2 ∧
 387    dihedralCos3Sq (starSq (starP (-h ^ 2))) 0 = -h ^ 2 ∧
 388    0 < starDeficit (h ^ 2) ∧
 389    starDeficit (-h ^ 2) < 0 ∧
 390    starDeficit (-h ^ 2) = -starDeficit (h ^ 2) ∧
 391    (∀ e : Fin 6, starSq (starP (h ^ 2)) e ≤ 3 ∧ starSq (starP (-h ^ 2)) e ≤ 3) ∧
 392    0 < cm3 (starSq (starP (h ^ 2))) ∧
 393    0 < cm3 (starSq (starP (-h ^ 2))) ∧
 394    |starDeficit (h ^ 2)| ≤ 2 * Real.pi * h ^ 2 ∧
 395    |starDeficit (-h ^ 2)| ≤ 2 * Real.pi * h ^ 2 := by
 396  have hsq_pos : 0 < h ^ 2 := by positivity
 397  have hsq_lt : h ^ 2 < 1 := by nlinarith
 398  have habs_pos : |h ^ 2| ≤ 1 := by
 399    rw [abs_of_pos hsq_pos]; linarith
 400  have habs_neg : |-h ^ 2| ≤ 1 := by
 401    rw [abs_neg, abs_of_pos hsq_pos]; linarith
 402  have habs_pos' : |h ^ 2| < 1 := by
 403    rw [abs_of_pos hsq_pos]; exact hsq_lt
 404  have habs_neg' : |-h ^ 2| < 1 := by
 405    rw [abs_neg, abs_of_pos hsq_pos]; exact hsq_lt
 406  refine ⟨star_q (h ^ 2), star_q (-h ^ 2), ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
 407  · exact (fourTet_deficit_sign (h ^ 2)).1 hsq_pos
 408  · exact (fourTet_deficit_sign (-h ^ 2)).2 (neg_lt_zero.mpr hsq_pos)
 409  · exact starDeficit_odd (h ^ 2)
 410  · intro e
 411    exact ⟨star_mesh_bound (h ^ 2) habs_pos e, star_mesh_bound (-h ^ 2) habs_neg e⟩
 412  · exact fourTet_nondegenerate (h ^ 2) habs_pos'
 413  · exact fourTet_nondegenerate (-h ^ 2) habs_neg'
 414  · have := starDeficit_abs_le (h ^ 2) habs_pos
 415    rwa [abs_of_pos hsq_pos] at this
 416  · have := starDeficit_abs_le (-h ^ 2) habs_neg
 417    rwa [abs_neg, abs_of_pos hsq_pos] at this
 418
 419/-! ## The even-ledger obstruction corollary -/
 420
 421/-- THEOREM (standalone algebraic parity fact): no function that is EVEN in
 422the deformation parameter can equal a signed deficit family on a punctured
 423interval around the flat point.  Pure algebra; no geometric or ledger content
 424is used in the statement or proof.
 425
 426Disclosure of the intended composition: the seven-gaps campaign's parity no-go
 427(`LedgerBridgeNoGo`) shows ledger J-deficits are even in the deformation
 428parameter.  Composing that result with this lemma would give "no ledger
 429J-deficit matches the signed star deficit family", but that composition is NOT
 430performed in Lean here: the import firewall of this lane forbids ledger
 431imports, deliberately, so the composition lives at the campaign level.  This
 432lemma is consistent with, but independent of, `LedgerBridgeNoGo`. -/
 433theorem even_ledger_cannot_match_signed_regge
 434    {δ g : ℝ → ℝ} {h₀ : ℝ} (hpos : 0 < h₀)
 435    (hsign : ∀ h : ℝ, 0 < h → h < h₀ → 0 < δ h ∧ δ (-h) < 0)
 436    (heven : ∀ h : ℝ, g (-h) = g h) :
 437    ¬ (∀ h : ℝ, 0 < |h| → |h| < h₀ → g h = δ h) := by
 438  intro hmatch
 439  have hh : 0 < h₀ / 2 := half_pos hpos
 440  have hlt : h₀ / 2 < h₀ := half_lt_self hpos
 441  obtain ⟨hδp, hδn⟩ := hsign (h₀ / 2) hh hlt
 442  have habs : |h₀ / 2| = h₀ / 2 := abs_of_pos hh
 443  have h1 : g (h₀ / 2) = δ (h₀ / 2) :=
 444    hmatch _ (by rw [habs]; exact hh) (by rw [habs]; exact hlt)
 445  have habs2 : |-(h₀ / 2)| = h₀ / 2 := by rw [abs_neg, habs]
 446  have h2 : g (-(h₀ / 2)) = δ (-(h₀ / 2)) :=
 447    hmatch _ (by rw [habs2]; exact hh) (by rw [habs2]; exact hlt)
 448  rw [heven] at h2
 449  linarith
 450
 451/-- THEOREM: instantiation on the explicit star deficit family with h₀ = 1. -/
 452theorem even_cannot_match_starDeficit
 453    (g : ℝ → ℝ) (heven : ∀ h : ℝ, g (-h) = g h) :
 454    ¬ (∀ h : ℝ, 0 < |h| → |h| < 1 → g h = starDeficit h) :=
 455  even_ledger_cannot_match_signed_regge one_pos
 456    (fun h hp _ =>
 457      ⟨(fourTet_deficit_sign h).1 hp,
 458       (fourTet_deficit_sign (-h)).2 (neg_lt_zero.mpr hp)⟩)
 459    heven
 460
 461/-! ## Status flags -/
 462
 463/-- Status record for the signed-deficit contact certificate lane. -/
 464structure FourTetSignedDeficitStatus where
 465  signed_deficit_kernel_checked : Bool
 466  weak_field_pair_constructed : Bool
 467  firewall_no_ledger_imports : Bool
 468  n5_torus_extension_open : Bool
 469
 470/-- The status of this module.  The N=5 periodic Freudenthal torus extension
 471is CLOSED by the Analysis lift
 472`FreudenthalN5TorusSignedDeficitLift.n5FaceDiagHingeDeficit_eq_faceDiagStarDeficit`
 473(field name retained; value flipped). -/
 474def status : FourTetSignedDeficitStatus where
 475  signed_deficit_kernel_checked := true
 476  weak_field_pair_constructed := true
 477  firewall_no_ledger_imports := true
 478  n5_torus_extension_open := false
 479
 480theorem status_signed_deficit_kernel_checked :
 481    status.signed_deficit_kernel_checked = true := rfl
 482
 483theorem status_weak_field_pair_constructed :
 484    status.weak_field_pair_constructed = true := rfl
 485
 486theorem status_firewall_no_ledger_imports :
 487    status.firewall_no_ledger_imports = true := rfl
 488
 489/-- Closed counterpart of the former openness rfl-anchor. -/
 490theorem status_n5_torus_extension_closed :
 491    status.n5_torus_extension_open = false := rfl
 492
 493end
 494
 495end FourTetSignedDeficit
 496end Geometry
 497end IndisputableMonolith
 498