IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCloser

   1import IndisputableMonolith.Gravity.Analysis.ReggeTTAlgebraicCloser
   2
   3/-!
   4# Regge TT continuum closer: `ReggeTTContinuumIsotropyTarget` is closed
   5
   6QG full-theory campaign, Paper C / Pillar 1, production stage C-DAG4, the
   7final stage of the panel-locked D-dag order (`ReggeTTBlochAssembly →
   8ReggeTTContinuumLimit → ReggeTTAlgebraicCloser → ReggeTTContinuumCloser`).
   9
  10## The verbatim target
  11
  12`ReggeTTSymbolPreflight.ReggeTTContinuumIsotropyTarget` (the named OPEN
  13target of the preflight, status flag `false` there): for every nonzero
  14integer wave vector `m` and every TT polarization `E`
  15(`IsTTPolarization`: symmetric, traceless, transverse, Frobenius-
  16normalized), the continuum TT Bloch symbol of the TRUE nonlinear Regge
  17action exists and equals `reggeTTContinuumCoefficient = -(1/4)`, the
  18linearized Einstein-Hilbert TT coefficient in these conventions.
  19
  20`reggeTTContinuumIsotropyTarget_closed` below proves it.  The witness
  21sequence for `ReggeTTContinuumSymbolIs` is the actual reduced finite
  22symbol `canonicalFiniteH (j+3) E m`:
  23
  24* fixed-`N` symbol existence: `planeWave_TTBlochSymbolIs_reduced` (Gate
  25  A1 + A2(b), the Schläfli-reduced second variation of the true action);
  26* normalized convergence to `-(1/4)`: the algebraic closer's composed
  27  headline `canonicalFiniteH_div_momentumNormSq_tendsto_isotropy`
  28  (P1.1a continuum limit + the C8 closed form
  29  `(1/2)·xᵀ·adj(E)·x` + the TT adjugate step).
  30
  31## Scope disclosures (inherited, binding)
  32
  33* This closes the 3D isotropy target.  It does NOT flip
  34  `gap_action_recovery`: the ledger names the 4D pair
  35  `edge_tt_decomposition` + `S_RS_converges_EH_4d` as that flag's closing
  36  theorems, and neither is proved here.
  37* Aliasing non-repair (inherited from the assembly stage): the finite
  38  assembly identity holds only at non-aliased side lengths and is
  39  consumed in eventual-filter form; no repair at aliased small `N` is
  40  attempted or needed for the limit.
  41
  42No `sorry`, no `admit`, no new axioms, no `native_decide` in this file.
  43No `: True` or `Nonempty`-only headline.
  44
  45## Inherited axiom footprint (disclosure, Elmo receipt 2026-07-17)
  46
  47The convergence side is clean: the algebraic closer's composed headline
  48`canonicalFiniteH_div_momentumNormSq_tendsto_isotropy` and the P1.1a
  49limit carry exactly `[propext, Classical.choice, Quot.sound]`.  The
  50existence side (`planeWave_TTBlochSymbolIs_reduced`, Gate A1 + A2(b))
  51rides the certified periodic angle-sum chain and therefore ALSO carries
  52`Lean.ofReduceBool` and `Lean.trustCompiler` (inherited compiler-trust
  53disclosure, same as `ReggeTTHingeAwareZeroMode`; not new axioms).  All
  54three theorems below inherit that footprint through the existence
  55component.  `#print axioms` receipts at end of file.
  56-/
  57
  58namespace IndisputableMonolith
  59namespace Gravity
  60namespace Analysis
  61namespace ReggeTTContinuumCloser
  62
  63open ReggeTTSymbolPreflight
  64open ReggeTTBlochInterfaceAudit
  65
  66noncomputable section
  67
  68/-- The reduced finite symbol IS a fixed-`N` TT Bloch symbol value: the
  69Gate A1 + A2(b) existence theorem restated on `canonicalFiniteH`. -/
  70theorem canonicalFiniteH_TTBlochSymbolIs (N : ℕ) [NeZero N]
  71    (E : Fin 3 → Fin 3 → ℝ) (m : Fin 3 → ℤ) :
  72    TTBlochSymbolIs N E m (canonicalFiniteH N E m) :=
  73  ReggeTTFlatSecondVariation.planeWave_TTBlochSymbolIs_reduced N E m
  74
  75/-- **THE VERBATIM 3D CLOSER (THEOREM): `ReggeTTContinuumIsotropyTarget`
  76holds.**  For every nonzero integer wave vector and every TT polarization,
  77the continuum TT Bloch symbol of the true Regge action exists and equals
  78`-(1/4)` — the symbol is isotropic with exactly the linearized
  79Einstein-Hilbert TT coefficient.  The preflight's OPEN target is closed;
  80the C10/C8 numerics are hereby superseded by kernel proof at 3D action
  81strength. -/
  82theorem reggeTTContinuumIsotropyTarget_closed :
  83    ReggeTTContinuumIsotropyTarget := by
  84  intro m E hm hTT
  85  have hm' : ∃ i : Fin 3, m i ≠ 0 := Function.ne_iff.mp hm
  86  refine ⟨fun j => @canonicalFiniteH (j + 3) (instNeZeroAddThree j) E m,
  87    fun j => canonicalFiniteH_TTBlochSymbolIs (j + 3) E m, ?_⟩
  88  exact
  89    ReggeTTAlgebraicCloser.canonicalFiniteH_div_momentumNormSq_tendsto_isotropy
  90      m E hm' hTT
  91
  92/-- The closed target instantiated at the preflight's own non-vacuity
  93witnesses (axis wave vector, `+` polarization): the continuum symbol at
  94that concrete instance is `-(1/4)`.  Non-vacuity receipt. -/
  95theorem axis_plus_continuum_symbol :
  96    ReggeTTContinuumSymbolIs axisTTPolarizationPlus axisWaveVector
  97      reggeTTContinuumCoefficient :=
  98  reggeTTContinuumIsotropyTarget_closed axisWaveVector axisTTPolarizationPlus
  99    axisWaveVector_ne_zero axisTTPolarizationPlus_isTT
 100
 101end
 102
 103end ReggeTTContinuumCloser
 104end Analysis
 105end Gravity
 106end IndisputableMonolith
 107
 108#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCloser.canonicalFiniteH_TTBlochSymbolIs
 109#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCloser.reggeTTContinuumIsotropyTarget_closed
 110#print axioms IndisputableMonolith.Gravity.Analysis.ReggeTTContinuumCloser.axis_plus_continuum_symbol
 111