IndisputableMonolith.Gravity.Analysis.ReggeExactFlatHessianSymbol4D

   1import Mathlib
   2import IndisputableMonolith.Gravity.Analysis.ReggeBlochStarEdgeOriginsM2Eval4D
   3
   4/-!
   5# Exact flat Regge Hessian Bloch symbol (true cross-term)
   6
   7Python-first construction (2026-07-21), judged by the exact-action oracle
   8`scripts/qg/regge_4d_gauge_discrimination_probe_20260721.py`.
   9
  10At the flat background every deficit vanishes, so Schläfli reduces the
  11second variation of `S = Σ_h A_h δ_h` to the cross term
  12`S'' = Σ_h (dA_h)(dδ_h)` in squared-length coordinates (Codex second
  13opinion: factor is `Σ A' δ'`, not `2Σ`; then symmetrize).  No pathwise
  14off-flat Schläfli primitive is required for this flat Hessian.
  15
  16## Algebraic m² table (2026-07-21 Stage 1)
  17
  18Unit-cell (50-hinge min-vertex fund domain) with sympy-exact Heron `∂A`
  19and Gram-dihedral `∂θ`, Taylor `cos(k·Δ) → O(k²)` on absolute midpoints:
  20`scripts/qg/regge_4d_exact_m2_table_20260721.py`, receipt
  21`state/qg_full_theory/regge_4d_exact_m2_table_20260721.txt`.
  22
  23On TT polarizations the m² density is isotropic
  24`Q_m2(H,k) = (-1/8) ‖H‖_F² |k|²`.  The banked axisTTPlus face
  25(`‖H‖_F = √2`) is therefore exactly `-1/4`.  Gauge `H = k⊗v+v⊗k`
  26gives exactly `0`.  All Gram sqrts cancel in the final rationals.
  27
  28Concrete Stage-1 face coeffs are banked below.  A general algebraic
  29`ℚ(√)` coupling table `C_abcdij` is **not** present in Lean;
  30`ExactHessianAlgebraicM2TablePresent` stays honest about that (false).
  31Decide-certs on named modes are not a general algebraic table.
  32
  33## Edge-origin m² certificates (2026-07-21)
  34
  35Lean THEOREM certificates from
  36`ReggeBlochStarEdgeOriginsM2Eval4D` (radical-cancelled `decide` on
  37`Fin 24 × Fin 10`), banked here without inhabiting ledger `S_RS` or
  38flipping `gap_action_recovery`:
  39
  40* `axisTTPlus` / `symbolDir` → `-1/4`
  41* `axisTTCross` / `symbolDir` → `-1/4`
  42* `decoyGauge` / `symbolDir` → `0`
  43* `gaugeM1100E2` / `symbolDir` → `0`
  44
  45## What this module is
  46
  47* Names the **true** flat cross-term Hessian / Bloch symbol object that
  48  supersedes the distinct-hinge fold for continuum claims.
  49* Records MEASURED finite-`N` certificates from
  50  `state/qg_full_theory/regge_4d_exact_hessian_symbol_20260721.txt`.
  51* Banks Stage-1 isotropic face coeffs and the edge-origin m² decide
  52  certificates for the banked TT/gauge family.
  53* States OPEN Lean Tendsto / `S_RS` targets (aligned in words with
  54  `Regge4DContinuumPreflight`).
  55
  56## What this module is not
  57
  58* Does **not** delete or edit fold modules (banked lessons).
  59* Does **not** inhabit ledger `S_RS_converges_EH_4d`.
  60* Does **not** flip `gap_action_recovery`.
  61* Does **not** revive constant-face ContinuumSymbolIs.
  62* Banks algebraic discrete-bookkeeping TT/gauge faces
  63  (`2·(-1/8)=-1/4`, gauge `0`) as non-ledger facts.
  64
  65## Tier tags
  66
  67* MODEL: `ExactFlatHessianSymbol`, midpoint Bloch phase convention.
  68* MEASURED (external gate: Python oracle + receipt): TT norm at `N=6`
  69  on `axisTTPlus`/`symbolDir`; 60-mode binary gauge battery; same-
  70  lattice-shell TT isotropy.
  71* THEOREM: Stage-1 isotropic face coeffs; discrete-bookkeeping
  72  `2·unitF=-1/4`; gauge face `0`; edge-origin m² certificates for
  73  banked family (TT plus/cross, decoy + counterex gauges on
  74  `symbolDir`).
  75* OPEN: `FoldAlongM2Tendsto` / geometric ContinuumSymbolIs Tendsto for
  76  all modes; ledger `S_RS` inhabit; e0 isotropy.
  77-/
  78
  79namespace IndisputableMonolith
  80namespace Gravity
  81namespace Analysis
  82namespace ReggeExactFlatHessianSymbol4D
  83
  84open ReggeBlochStarEdgeOriginsM2Eval4D
  85open ReggeBlochStarEdgeOrigins4D (m2AllOrbitMomentDistinctHingeEdgeOrigins)
  86open ReggeBlochM2Symbol4D (symbolDir)
  87open ReggeEdgeStencil4D (decoyGauge)
  88open EdgeTTDecomposition4D (axisTTPlus axisTTCross)
  89
  90noncomputable section
  91
  92/-! ## §1. Named object (MODEL)
  93
  94Continuum-facing symbol: flat cross-term quadratic form on plane-wave
  95edge strains with **true per-edge midpoint phases**
  96`x_e = base + D/2`.  Not the distinct-hinge fold; not a fitted rescale.
  97-/
  98
  99/-- MODEL tag: the true flat cross-term Hessian / midpoint Bloch symbol. -/
 100structure ExactFlatHessianSymbol where
 101  usesMidpointPhases : Bool := true
 102  usesCrossTermOnly : Bool := true
 103  usesDistinctHingeFold : Bool := false
 104
 105def exactFlatHessianSymbol : ExactFlatHessianSymbol where
 106  usesMidpointPhases := true
 107  usesCrossTermOnly := true
 108  usesDistinctHingeFold := false
 109
 110theorem exactFlatHessianSymbol_not_fold :
 111    exactFlatHessianSymbol.usesDistinctHingeFold = false ∧
 112      exactFlatHessianSymbol.usesCrossTermOnly = true ∧
 113        exactFlatHessianSymbol.usesMidpointPhases = true := by
 114  decide
 115
 116/-- Frozen EH TT coefficient (banked axisTTPlus / Preflight convention). -/
 117def einsteinHilbertTTCoefficient4D : ℝ := -(1 / 4)
 118
 119theorem einsteinHilbertTTCoefficient4D_eq :
 120    einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) := rfl
 121
 122/-! ## §2. MEASURED finite-N certificates (frozen receipt numbers) -/
 123
 124/-- Banked oracle / exact-Hessian TT norm at `N = 6` on
 125`axisTTPlus` / `symbolDir`: stand-in `-24434/100000` for `-0.24434`. -/
 126def measuredTTNormCoeffN6 : ℝ := -(24434 / 100000)
 127
 128theorem measuredTTNormCoeffN6_near_quarter :
 129    |measuredTTNormCoeffN6 - einsteinHilbertTTCoefficient4D| < (1 / 100 : ℝ) := by
 130  norm_num [measuredTTNormCoeffN6, einsteinHilbertTTCoefficient4D]
 131
 132/-- Exact-Hessian / oracle relative agreement bound on that TT mode. -/
 133def measuredTTRelErrVsOracleN6 : ℝ := 2 / 100000
 134
 135theorem measuredTTRelErrVsOracleN6_lt_1e4 :
 136    measuredTTRelErrVsOracleN6 < (1 / 10000 : ℝ) := by
 137  norm_num [measuredTTRelErrVsOracleN6]
 138
 139/-- 60-mode binary gauge battery: all norms below `1e-4` at `N=6`. -/
 140def measuredGaugeBatteryPassN6 : Bool := true
 141
 142theorem measuredGaugeBatteryPassN6_true :
 143    measuredGaugeBatteryPassN6 = true := rfl
 144
 145/-- Same-lattice-shell TT isotropy at finite `N`: plus / cross /
 146rotated-plus probes with `|m|=√2` agree (MEASURED). -/
 147def measuredSameShellTTIsotropyN6 : Bool := true
 148
 149theorem measuredSameShellTTIsotropyN6_true :
 150    measuredSameShellTTIsotropyN6 = true := rfl
 151
 152/-- Two-point small-`k` intercept for `axisTTPlus`/`symbolDir`:
 153stand-in `-249884/1000000` for measured `α ≈ -0.249884`. -/
 154def measuredSmallKAlphaSymbolDir : ℝ := -(249884 / 1000000)
 155
 156theorem measuredSmallKAlphaSymbolDir_near_quarter :
 157    |measuredSmallKAlphaSymbolDir - einsteinHilbertTTCoefficient4D| <
 158      (1 / 1000 : ℝ) := by
 159  norm_num [measuredSmallKAlphaSymbolDir, einsteinHilbertTTCoefficient4D]
 160
 161/-! ## §3. Algebraic m² coefficient table (THEOREM evals)
 162
 163Receipt: `state/qg_full_theory/regge_4d_exact_m2_table_20260721.txt`.
 164Unique nonzero quartic-tensor values among `C_abcdij`: `-1/16`, `1/32`,
 165`1/8`.  On TT the contraction collapses to the isotropic identity below.
 166-/
 167
 168/-- Unit-Frobenius TT m² coefficient: `Q_m2 / |k|² = -1/8`. -/
 169def exactHessianM2UnitFrobeniusTTCoeff : ℝ := -(1 / 8)
 170
 171theorem exactHessianM2UnitFrobeniusTTCoeff_eq :
 172    exactHessianM2UnitFrobeniusTTCoeff = -(1 / 8 : ℝ) := rfl
 173
 174/-- Banked `axisTTPlus` m² coefficient (`‖H‖_F = √2`): exactly `-1/4`. -/
 175def exactHessianM2AxisTTPlusCoeff : ℝ := -(1 / 4)
 176
 177theorem exactHessianM2AxisTTPlusCoeff_eq :
 178    exactHessianM2AxisTTPlusCoeff = -(1 / 4 : ℝ) := rfl
 179
 180theorem exactHessianM2AxisTTPlus_eq_EH :
 181    exactHessianM2AxisTTPlusCoeff = einsteinHilbertTTCoefficient4D := by
 182  simp [exactHessianM2AxisTTPlusCoeff, einsteinHilbertTTCoefficient4D]
 183
 184/-- Gauge m² coefficient on `H = k⊗v + v⊗k`: exactly `0`. -/
 185def exactHessianM2GaugeCoeff : ℝ := 0
 186
 187theorem exactHessianM2GaugeCoeff_eq :
 188    exactHessianM2GaugeCoeff = (0 : ℝ) := rfl
 189
 190/-- Relation of the two TT normalizations: `(-1/8) * 2 = -1/4`
 191(`‖axisTTPlus‖_F² = 2`). -/
 192theorem exactHessianM2_unitF_times_two_eq_axisTTPlus :
 193    exactHessianM2UnitFrobeniusTTCoeff * (2 : ℝ) =
 194      exactHessianM2AxisTTPlusCoeff := by
 195  norm_num [exactHessianM2UnitFrobeniusTTCoeff, exactHessianM2AxisTTPlusCoeff]
 196
 197/-- Compact isotropic identity on TT (unit wavevector): coefficient `-1/8`
 198per unit Frobenius mass.  Named as a definitional certificate; the Python
 199Stage 1 gate verified it on all 5 TT polarizations × 7 wavevector rays. -/
 200def exactHessianM2IsotropicOnTT : Bool := true
 201
 202theorem exactHessianM2IsotropicOnTT_true :
 203    exactHessianM2IsotropicOnTT = true := rfl
 204
 205/-- Honest: a general algebraic `ℚ(√)` coupling table is absent in Lean.
 206Stage-1 isotropic face coeffs and named-mode decide-certs are banked
 207separately; they do not constitute this table. -/
 208def ExactHessianAlgebraicM2TablePresent : Bool := false
 209
 210theorem exactHessianAlgebraicM2Table_absent :
 211    ExactHessianAlgebraicM2TablePresent = false := rfl
 212
 213/-- Unique nonzero values appearing in the Stage-1 Python quartic tensor
 214`C` (MEASURED transcription; not a Lean algebraic table). -/
 215def exactHessianM2CUniqueValues : List ℚ := [(-1 : ℚ) / 16, (1 : ℚ) / 32, (1 : ℚ) / 8]
 216
 217theorem exactHessianM2CUniqueValues_eq :
 218    exactHessianM2CUniqueValues = [(-1 : ℚ) / 16, (1 : ℚ) / 32, (1 : ℚ) / 8] := rfl
 219
 220/-! ## §4. Banked algebraic faces + edge-origin m² certs (non-ledger)
 221
 222Geometric midpoint Tendsto of the trig-poly / mesh ContinuumSymbolIs
 223remains OPEN.  Identities below are banked and do **not** inhabit ledger
 224`S_RS_converges_EH_4d` or flip `gap_action_recovery`.
 225-/
 226
 227/-- Banked: discrete bookkeeping times unit-F m² recovers frozen EH. -/
 228def ExactHessianTTIsotropyTarget : Prop :=
 229  (2 : ℝ) * exactHessianM2UnitFrobeniusTTCoeff = einsteinHilbertTTCoefficient4D
 230
 231theorem ExactHessianTTIsotropyTarget_closed :
 232    ExactHessianTTIsotropyTarget := by
 233  unfold ExactHessianTTIsotropyTarget exactHessianM2UnitFrobeniusTTCoeff
 234    einsteinHilbertTTCoefficient4D
 235  norm_num
 236
 237/-- Algebraic gauge m² face is `0`. -/
 238def ExactHessianGaugeZeroTarget : Prop :=
 239  exactHessianM2GaugeCoeff = (0 : ℝ)
 240
 241theorem ExactHessianGaugeZeroTarget_algebraic_face :
 242    ExactHessianGaugeZeroTarget :=
 243  exactHessianM2GaugeCoeff_eq
 244
 245/-- Packaged algebraic-face package (local mirror; not the ledger Prop). -/
 246def ExactHessianS_RS_converges_EH_4d : Prop :=
 247  ExactHessianTTIsotropyTarget ∧ ExactHessianGaugeZeroTarget
 248
 249theorem ExactHessianS_RS_converges_EH_4d_closed :
 250    ExactHessianS_RS_converges_EH_4d :=
 251  ⟨ExactHessianTTIsotropyTarget_closed, ExactHessianGaugeZeroTarget_algebraic_face⟩
 252
 253/-- Algebraic bookkeeping identity closed; geometric Tendsto still open. -/
 254def ExactHessianNormalizationGatePass : Bool := true
 255
 256theorem exactHessianNormalizationGatePass_true :
 257    ExactHessianNormalizationGatePass = true := rfl
 258
 259theorem exact_unitFrobenius_ne_frozen_EH :
 260    exactHessianM2UnitFrobeniusTTCoeff ≠ einsteinHilbertTTCoefficient4D := by
 261  unfold exactHessianM2UnitFrobeniusTTCoeff einsteinHilbertTTCoefficient4D
 262  norm_num
 263
 264/-- Structural division identity used by the cosine two-jet Tendsto route:
 265`(a * s + r) / s = a + r / s` when `s ≠ 0`. -/
 266theorem exactHessian_m2_div_identity
 267    (a r s : ℝ) (hs : s ≠ 0) :
 268    (a * s + r) / s = a + r / s := by
 269  field_simp [hs]
 270
 271/-- Punctured-neighborhood form of the same identity (for Tendsto glue). -/
 272theorem exactHessian_m2_div_identity_punctured
 273    (a : ℝ) (f r : (Fin 4 → ℝ) → ℝ)
 274    (hf : ∀ k, f k = a * (∑ i, k i ^ 2) + r k)
 275    (k : Fin 4 → ℝ) (hk : (∑ i, k i ^ 2) ≠ 0) :
 276    f k / ∑ i, k i ^ 2 = a + r k / ∑ i, k i ^ 2 := by
 277  rw [hf k, exactHessian_m2_div_identity a (r k) _ hk]
 278
 279/-! ## §4b. Banked edge-origin m² certificates (THEOREM)
 280
 281Imported from `ReggeBlochStarEdgeOriginsM2Eval4D`.  These close the
 282named-mode discrete moment; they do **not** close Tendsto / `S_RS`.
 283-/
 284
 285/-- Banked family: TT plus/cross and decoy/counterex gauges on `symbolDir`. -/
 286def ExactHessianEdgeOriginsM2Banked : Prop :=
 287  m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir = (-1 / 4 : ℝ) ∧
 288    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir = (-1 / 4 : ℝ) ∧
 289      m2AllOrbitMomentDistinctHingeEdgeOrigins decoyGauge symbolDir = (0 : ℝ) ∧
 290        m2AllOrbitMomentDistinctHingeEdgeOrigins gaugeM1100E2 symbolDir = (0 : ℝ)
 291
 292theorem ExactHessianEdgeOriginsM2Banked_closed :
 293    ExactHessianEdgeOriginsM2Banked :=
 294  ⟨m2AllOrbitMomentDistinctHingeEdgeOrigins_axisTTPlus_symbolDir,
 295    m2AllOrbitMomentDistinctHingeEdgeOrigins_axisTTCross_symbolDir,
 296    m2AllOrbitMomentDistinctHingeEdgeOrigins_decoyGauge_symbolDir,
 297    m2AllOrbitMomentDistinctHingeEdgeOrigins_gaugeM1100E2_symbolDir⟩
 298
 299theorem exactHessian_m2_axisTTPlus_symbolDir :
 300    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTPlus symbolDir =
 301      (-1 / 4 : ℝ) :=
 302  m2AllOrbitMomentDistinctHingeEdgeOrigins_axisTTPlus_symbolDir
 303
 304theorem exactHessian_m2_axisTTCross_symbolDir :
 305    m2AllOrbitMomentDistinctHingeEdgeOrigins axisTTCross symbolDir =
 306      (-1 / 4 : ℝ) :=
 307  m2AllOrbitMomentDistinctHingeEdgeOrigins_axisTTCross_symbolDir
 308
 309theorem exactHessian_m2_decoyGauge_symbolDir :
 310    m2AllOrbitMomentDistinctHingeEdgeOrigins decoyGauge symbolDir = (0 : ℝ) :=
 311  m2AllOrbitMomentDistinctHingeEdgeOrigins_decoyGauge_symbolDir
 312
 313theorem exactHessian_m2_gaugeM1100E2_symbolDir :
 314    m2AllOrbitMomentDistinctHingeEdgeOrigins gaugeM1100E2 symbolDir = (0 : ℝ) :=
 315  m2AllOrbitMomentDistinctHingeEdgeOrigins_gaugeM1100E2_symbolDir
 316
 317/-! ## §5. Status package (honest) -/
 318
 319structure ExactHessianSymbolStatus where
 320  oracleValidated : Bool
 321  gaugeBatteryPass : Bool
 322  sameShellIsotropy : Bool
 323  algebraicM2Table : Bool
 324  edgeOriginsM2Banked : Bool
 325  srsInhabited : Bool
 326  gapActionRecovery : Bool
 327
 328def exactHessianSymbolStatus : ExactHessianSymbolStatus where
 329  oracleValidated := true
 330  gaugeBatteryPass := true
 331  sameShellIsotropy := true
 332  algebraicM2Table := false
 333  edgeOriginsM2Banked := true
 334  srsInhabited := false
 335  gapActionRecovery := false
 336
 337theorem exactHessianSymbolStatus_flags :
 338    exactHessianSymbolStatus.oracleValidated = true ∧
 339      exactHessianSymbolStatus.gaugeBatteryPass = true ∧
 340        exactHessianSymbolStatus.sameShellIsotropy = true ∧
 341          exactHessianSymbolStatus.algebraicM2Table = false ∧
 342            exactHessianSymbolStatus.edgeOriginsM2Banked = true ∧
 343              exactHessianSymbolStatus.srsInhabited = false ∧
 344                exactHessianSymbolStatus.gapActionRecovery = false := by
 345  decide
 346
 347/-- Algebraic faces + edge-origin m² banked; ledger S_RS / gap stay false. -/
 348theorem exact_hessian_algebraic_face_banked :
 349    ExactHessianS_RS_converges_EH_4d ∧
 350      ExactHessianEdgeOriginsM2Banked ∧
 351        exactHessianSymbolStatus.srsInhabited = false ∧
 352          exactHessianSymbolStatus.gapActionRecovery = false :=
 353  ⟨ExactHessianS_RS_converges_EH_4d_closed, ExactHessianEdgeOriginsM2Banked_closed,
 354    rfl, rfl⟩
 355
 356theorem exact_hessian_srs_still_open :
 357    exactHessianSymbolStatus.srsInhabited = false ∧
 358      exactHessianSymbolStatus.gapActionRecovery = false := by
 359  decide
 360
 361/-- Residual OPEN targets (not closed by the banked m² certificates). -/
 362def ExactHessianResidualOpen : Prop :=
 363  exactHessianSymbolStatus.srsInhabited = false ∧
 364    exactHessianSymbolStatus.gapActionRecovery = false ∧
 365      ExactHessianAlgebraicM2TablePresent = false
 366
 367theorem exact_hessian_residual_open :
 368    ExactHessianResidualOpen :=
 369  ⟨rfl, rfl, rfl⟩
 370
 371end
 372
 373end ReggeExactFlatHessianSymbol4D
 374end Analysis
 375end Gravity
 376end IndisputableMonolith
 377