Gravity Analysis Regge Ttcontinuum Closer Axis Plus Continuum Symbol

A concrete check of the continuum limit

In the framework's lattice model of gravity, space is a discrete grid of points, and the action, the quantity whose minimization gives the field equations, is a sum over the grid's edges and hinges. The continuum limit is the idealized limit where the grid spacing shrinks to zero. A central question is whether this discrete action reproduces the standard linearized Einstein-Hilbert action of continuous spacetime in that limit. The theorem axis_plus_continuum_symbol checks one concrete instance of that question.

The specific instance uses a wave vector pointing along a coordinate axis and a polarization state called "plus". For this case, the theorem proves that the continuum symbol, a quantity derived from the discrete action's second variation, equals exactly -(1/4), which is the same coefficient that appears in the linearized Einstein-Hilbert action under the framework's conventions. This is a special case of a broader result, also proved in the same file, that establishes this equality for every nonzero wave vector and every transverse-traceless polarization. The broader result is the target named ReggeTTContinuumIsotropyTarget, and the concrete theorem is its instantiation at the specific axis-plus witness.

The proof is machine-checked: it is a theorem in the framework's library of formal theorems, with no gaps or admitted assumptions. The convergence part of the proof relies only on the standard axioms of the ambient type theory, while the existence part inherits a disclosure about compiler trust, which is not a new axiom. The theorem does not claim that the full nonlinear action converges to the Einstein-Hilbert action in four dimensions. That remains an open target, named gap_action_recovery, and the file explicitly states that this result does not prove it.

What this theorem changes is the status of a specific check: for a single, well-understood case, the discrete lattice model demonstrably matches the continuous theory at the linearized level. This is a necessary step, though not a sufficient one, toward the larger goal of showing that the discrete framework reproduces general relativity in the continuum limit.

/-- The closed target instantiated at the preflight's own non-vacuity
witnesses (axis wave vector, `+` polarization): the continuum symbol at
that concrete instance is `-(1/4)`.  Non-vacuity receipt. -/
theorem axis_plus_continuum_symbol :
    ReggeTTContinuumSymbolIs axisTTPolarizationPlus axisWaveVector
      reggeTTContinuumCoefficient :=
  reggeTTContinuumIsotropyTarget_closed axisWaveVector axisTTPolarizationPlus
    axisWaveVector_ne_zero axisTTPolarizationPlus_isTT

/-- **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 claim that the discrete action converges to the full Einstein-Hilbert action in four dimensions. This does not claim that the existence side of the proof is free of compiler-trust assumptions. This does not claim that the framework reproduces general relativity beyond the linearized 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: