Gravity Analysis Regge Ttcontinuum Closer Regge Ttcontinuum Isotropy Target Clos

The closed isotropy target

The declaration reggeTTContinuumIsotropyTarget_closed is a formal theorem in the machine-checked library of the Recognition Science framework. It proves a specific claim about a lattice model of gravity: for every nonzero wave vector and every transverse-traceless polarization, the continuum limit of the model's wave symbol exists and equals -(1/4). That number is exactly the coefficient that appears in the linearized Einstein-Hilbert action for gravitational waves in three dimensions. In plain terms, the discrete model, when refined to a continuum, reproduces the same wave-propagation behavior as Einstein's theory, at least at the level of the transverse-traceless sector.

The proof is not a numerical approximation or a simulation. It is a theorem in the framework's formal library, checked by the Lean kernel. The theorem closes a target that was previously listed as open: the preflight document had named ReggeTTContinuumIsotropyTarget as an unproved statement. The new declaration proves it for all nonzero wave vectors and all TT polarizations. The witness sequence is explicit: it constructs a reduced finite symbol for each lattice size and shows that the normalized sequence converges to -(1/4). The convergence component carries only the standard axiom footprint [propext, Classical.choice, Quot.sound]. The existence component inherits a compiler-trust disclosure, which is not a new axiom.

What the declaration does not claim is as important as what it proves. It does not close the four-dimensional gap-action recovery target. The framework's ledger names two other theorems, edge_tt_decomposition and S_RS_converges_EH_4d, as the closing theorems for that flag; neither is proved in this file. The result also does not address aliasing at small lattice sizes. The finite assembly identity holds only at non-aliased side lengths, and no repair is attempted at aliased small N. The theorem is specifically about the three-dimensional transverse-traceless sector, not about the full nonlinear action or about four dimensions.

The practical consequence is that a previously open target in the framework's gravity program is now settled by kernel proof. The C10/C8 numerics that had been used as evidence are superseded by a formal derivation. The result strengthens the framework's claim that its discrete model converges to general relativity in the appropriate limit, at least for the TT sector in three dimensions. It does not, by itself, prove the full theory or the four-dimensional recovery; those remain separate targets.

/-- **THE VERBATIM 3D CLOSER (THEOREM): `ReggeTTContinuumIsotropyTarget`
holds.**  For every nonzero integer wave vector and every TT polarization,
the continuum TT Bloch symbol of the true Regge action exists and equals
`-(1/4)` — the symbol is isotropic with exactly the linearized
Einstein-Hilbert TT coefficient.  The preflight's OPEN target is closed;
the C10/C8 numerics are hereby superseded by kernel proof at 3D action
strength. -/
theorem reggeTTContinuumIsotropyTarget_closed :
    ReggeTTContinuumIsotropyTarget := by
  intro m E hm hTT
  have hm' : ∃ i : Fin 3, m i ≠ 0 := Function.ne_iff.mp hm
  refine ⟨fun j => @canonicalFiniteH (j + 3) (instNeZeroAddThree j) E m,
    fun j => canonicalFiniteH_TTBlochSymbolIs (j + 3) E m, ?_⟩
  exact
    ReggeTTAlgebraicCloser.canonicalFiniteH_div_momentumNormSq_tendsto_isotropy
      m E hm' hTT

/-- **THE VERBATIM 3D CLOSER (THEOREM): `ReggeTTContinuumIsotropyTarget`
holds.**  For every nonzero integer wave vector and every TT polarization,
the continuum TT Bloch symbol of the true Regge action exists and equals
`-(1/4)` — the symbol is isotropic with exactly the linearized
Einstein-Hilbert TT coefficient.  The preflight's OPEN target is closed;
the C10/C8 numerics are hereby superseded by kernel proof at 3D action
strength. -/
theorem reggeTTContinuumIsotropyTarget_closed :
    ReggeTTContinuumIsotropyTarget := by
  intro m E hm hTT
  have hm' : ∃ i : Fin 3, m i ≠ 0 := Function.ne_iff.mp hm
  refine ⟨fun j => @canonicalFiniteH (j + 3) (instNeZeroAddThree j) E m,
    fun j => canonicalFiniteH_TTBlochSymbolIs (j + 3) E m, ?_⟩
  exact
    ReggeTTAlgebraicCloser.canonicalFiniteH_div_momentumNormSq_tendsto_isotropy
      m E hm' hTT

/-- **THE VERBATIM 3D CLOSER (THEOREM): `ReggeTTContinuumIsotropyTarget`
holds.**  For every nonzero integer wave vector and every TT polarization,
the continuum TT Bloch symbol of the true Regge action exists and equals
`-(1/4)` — the symbol is isotropic with exactly the linearized
Einstein-Hilbert TT coefficient.  The preflight's OPEN target is closed;
the C10/C8 numerics are hereby superseded by kernel proof at 3D action
strength. -/
theorem reggeTTContinuumIsotropyTarget_closed :
    ReggeTTContinuumIsotropyTarget := by
  intro m E hm hTT
  have hm' : ∃ i : Fin 3, m i ≠ 0 := Function.ne_iff.mp hm
  refine ⟨fun j => @canonicalFiniteH (j + 3) (instNeZeroAddThree j) E m,
    fun j => canonicalFiniteH_TTBlochSymbolIs (j + 3) E m, ?_⟩
  exact
    ReggeTTAlgebraicCloser.canonicalFiniteH_div_momentumNormSq_tendsto_isotropy
      m E hm' hTT

What this page does not claim

This does not prove four-dimensional gap-action recovery. This does not address aliasing at small lattice sizes. This does not cover the full nonlinear action beyond the transverse-traceless sector.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/Analysis/ReggeTTContinuumCloser.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: