Gravity Analysis Regge Tthinge Aware Zero Mode Canonical Finite H Zero Momentum

The flat zero mode

In Regge calculus, space is chopped into flat tetrahedra, and gravity is described by the lengths of their edges. The question of whether a perturbation of this discrete geometry carries energy is answered by the second variation of the action, a kind of stiffness matrix. A zero mode, a perturbation with zero stiffness, is a flat direction: the lattice can be deformed along it without changing the action to second order, so it costs no energy.

The declaration canonicalFiniteH_zeroMomentum_eq_zero proves that a constant, uniform perturbation of the metric, one that is the same at every lattice site, is exactly such a zero mode. This holds for every lattice size N and for every polarization matrix, meaning the perturbation can be oriented in any direction and the result still holds. The proof works by showing that the assembled constant block of the stiffness matrix is a perfect square, and that the alternating sum of the edge-class coefficients vanishes for every polarization. This is a theorem in the machine-checked library of formal theorems.

The result is stronger than the specific case that motivated it. The original question concerned transverse-traceless perturbations, a particular class of metric deformations. The proof shows the constant block vanishes for every polarization, not just the transverse-traceless ones. The transverse-traceless case is a special instance, and a separate witness-level theorem exhibits the cancellation between the hinge term and the stencil-only residual on a concrete transverse-traceless example.

What the theorem does not claim is also precise. It does not prove that the full Hessian decomposition, splitting the assembled block into hinge and per-tetrahedron terms, holds everywhere; that split is kernel-checked only at the recorded witness. The theorem concerns the assembled object, not the individual pieces. It also does not claim anything about the physical meaning of this zero mode for the full theory of quantum gravity; it is a statement about the second variation of the classical Regge action on a lattice.

/-- **ZERO-MODE SYMBOL COROLLARY (THEOREM): the fixed-`N` TT Bloch symbol
of the TRUE nonlinear Regge action at ZERO wave vector exists and equals
`0`, for every `N` and every polarization matrix.**  This is the lattice
flat zero mode as a statement about the actual second variation, through
the Gate A1 existence chain and the Gate A2 reduction.  AXIOM
DISCLOSURE: this corollary (alone in this file) rides the certified
flat-deficit chain and therefore inherits `Lean.ofReduceBool` /
`Lean.trustCompiler` in addition to the standard trio. -/
theorem zeroMomentum_symbol_is_zero (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) :
    TTBlochSymbolIs N E (fun _ => (0 : ℤ)) 0 := by
  have h := ReggeTTFlatSecondVariation.planeWave_TTBlochSymbolIs_reduced
    N E (fun _ => (0 : ℤ))
  have hval : canonicalFiniteH N E (fun _ => (0 : ℤ)) =
      (2 / (N : ℝ) ^ (3 : ℕ)) *
        (-∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
          ReggeTTFlatSecondVariation.flatSlotSqrtDeriv N E
              (commensurateMomentum N (fun _ => (0 : ℤ))) τ f *
            ReggeTTFlatSecondVariation.flatSlotAngleDeriv N E
              (commensurateMomentum N (fun _ => (0 : ℤ))) τ f) := rfl
  rw [← hval, canonicalFiniteH_zeroMomentum_eq_zero N E] at h
  exact h

/-- **ZERO-MODE SYMBOL COROLLARY (THEOREM): the fixed-`N` TT Bloch symbol
of the TRUE nonlinear Regge action at ZERO wave vector exists and equals
`0`, for every `N` and every polarization matrix.**  This is the lattice
flat zero mode as a statement about the actual second variation, through
the Gate A1 existence chain and the Gate A2 reduction.  AXIOM
DISCLOSURE: this corollary (alone in this file) rides the certified
flat-deficit chain and therefore inherits `Lean.ofReduceBool` /
`Lean.trustCompiler` in addition to the standard trio. -/
theorem zeroMomentum_symbol_is_zero (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) :
    TTBlochSymbolIs N E (fun _ => (0 : ℤ)) 0 := by
  have h := ReggeTTFlatSecondVariation.planeWave_TTBlochSymbolIs_reduced
    N E (fun _ => (0 : ℤ))
  have hval : canonicalFiniteH N E (fun _ => (0 : ℤ)) =
      (2 / (N : ℝ) ^ (3 : ℕ)) *
        (-∑ τ : PeriodicTet N N N, ∑ f : Fin 6,
          ReggeTTFlatSecondVariation.flatSlotSqrtDeriv N E
              (commensurateMomentum N (fun _ => (0 : ℤ))) τ f *
            ReggeTTFlatSecondVariation.flatSlotAngleDeriv N E
              (commensurateMomentum N (fun _ => (0 : ℤ))) τ f) := rfl
  rw [← hval, canonicalFiniteH_zeroMomentum_eq_zero N E] at h
  exact h

/-- The reported witness IS a TT polarization for `k = e_z`: symmetric,
traceless, transverse, Frobenius-normalized.  This grounds the phrase
"the reported TT witness" of the recorded residual. -/
theorem ttWitness_isTT :
    IsTTPolarization ttWitnessWaveVector ttWitnessPolarization := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · intro i j
    fin_cases i <;> fin_cases j <;> simp only [ttWitnessPolarization]
  · simp only [Fin.sum_univ_three, ttWitnessPolarization]
    ring
  · intro j
    fin_cases j <;>
      · simp only [Fin.sum_univ_three, ttWitnessPolarization,
          ttWitnessWaveVector]
        push_cast
        ring
  · simp only [Fin.sum_univ_three, ttWitnessPolarization]
    linear_combination 2 * inv_sqrt2_mul_self

What this page does not claim

The theorem does not prove the full Hessian decomposition assembled = hinge - sum G c c holds everywhere; that split is kernel-checked only at the recorded witness. The theorem does not claim any physical consequence for the full theory of quantum gravity. The theorem does not prove that the stencil-only constant block vanishes; it proves that the assembled block, with the hinge term, vanishes.

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