Gravity Analysis Regge Ttsymbol Preflight

The preflight check

In the framework's account, gravity is built from elementary tetrahedra, the simplest three-dimensional solid. The ledger, a discrete record of geometric states, tracks the squared length of every edge in a periodic lattice called the Freudenthal torus. The cost, the action that measures how far a configuration is from flat, sums a deficit angle around each edge. This preflight check defines the exact objects needed to ask whether this discrete gravity becomes smooth and direction-independent at long wavelengths.

The central object is the TT Bloch symbol, a quantity that measures how the action responds to a small plane-wave perturbation of the edge lengths. A plane wave is a ripple with a definite wavelength and direction; TT stands for transverse-traceless, the two polarizations that gravitational waves possess. The preflight defines the perturbation family, the second difference of the action along it, and the limit that would define the continuum symbol. These are definitions only. The preflight proves the setup is coherent: the perturbation passes through the flat configuration, the second difference is even in the amplitude, and the two explicit TT polarizations for the axis direction are valid. It also proves that the true nonlinear action vanishes at the flat point, and that a previously studied frozen model is exactly the true action restricted to a special conformal family of edge fields.

The preflight does not prove the headline result. The claim that the TT Bloch symbol converges to the isotropic value -1/4, matching the linearized Einstein-Hilbert coefficient, is a named open target, ReggeTTContinuumIsotropyTarget, with status flag false. Numerical evidence from a separate probe supports this value on all 14 preregistered directions, but that evidence is not a proof. The preflight's theorems, such as the flat point and the frozen-model identification, are kernel-checked with no admitted axioms beyond the standard three. The preflight establishes the vocabulary and the non-vacuity of the question, so a later stage can attempt the limit itself.

What this changes is the boundary of what is known. The framework now has a precise, machine-checked statement of what would need to be proved for discrete gravity to recover the familiar continuum behavior. The path is marked, the tools are in place, and the target is named. The proof of isotropy remains open, but the question is no longer vague.

/-- THE TRUE NONLINEAR 3D REGGE ACTION on the side-`N` periodic Freudenthal
torus, as a function of the edge squared-length field:
`S(ℓ) = Σ_e √(ℓ_e) · deficit_e`.  This is the object whose TT Bloch symbol
the C10 probe measured. -/
def trueReggeAction (ℓ : EdgeField N) : ℝ :=
  ∑ e : PeriodicEdge N N N, Real.sqrt (ℓ e) * deficitOfField N ℓ e

/-- FLAT POINT, action form (THEOREM): the true Regge action vanishes at
the flat edge assignment. -/
theorem trueReggeAction_flatEdgeField :
    trueReggeAction N (flatEdgeField N) = 0 := by
  unfold trueReggeAction
  refine Finset.sum_eq_zero fun e _ => ?_
  rw [deficitOfField_flatEdgeField N e, mul_zero]

/-- Definitional transparency of the canonical triangulation's local
tetrahedron (proof is `rfl`). -/
theorem canonical_tet_eq (τ : Fin (canonicalPeriodicTriangulation N N N).nT) :
    (canonicalPeriodicTriangulation N N N).tet τ =
      Geometry.FreudenthalCubeTriangulation.freudenthalTet := rfl

/-- The `+`-witness is a TT polarization for the axis wave vector. -/
theorem axisTTPolarizationPlus_isTT :
    IsTTPolarization axisWaveVector axisTTPolarizationPlus := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · intro i j
    fin_cases i <;> fin_cases j <;>
      simp only [axisTTPolarizationPlus]
  · simp only [Fin.sum_univ_three, axisTTPolarizationPlus]
    ring
  · intro j
    fin_cases j <;>
      · simp only [Fin.sum_univ_three, axisTTPolarizationPlus,
          axisWaveVector]
        push_cast
        ring
  · simp only [Fin.sum_univ_three, axisTTPolarizationPlus]
    linear_combination 2 * inv_sqrt_two_sq

What this page does not claim

The isotropy of the TT Bloch symbol in the continuum limit is not proved here. The numerical value -1/4 is not established as a theorem. The frozen-model identification is a definitional tautology, not a derivation of the graph-Laplacian model.

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/ReggeTTSymbolPreflight.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: