Encyclopedia Gravity Gravity Analysis Regge Tthinge Aware Zero Mode

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Tthinge Aware Zero Mode

A machine-checked proof that a certain lattice version of gravity has a flat direction: constant distortions cost nothing, a fact that must hold for the theory to make sense.

Verify this page

The lattice flat direction

Regge calculus is a way of doing general relativity without smooth geometry. Instead of a continuous spacetime, you build it from flat four-dimensional blocks, called tetrahedra, glued together along their faces. The geometry lives in the edge lengths: how long each edge is determines the curvature, and the Einstein equations become statements about how the total volume changes when you stretch those edges. It is the standard discrete approach to gravity, introduced by Tullio Regge in 1961.

A key question for any discrete gravity is whether it has the right zero modes. A zero mode is a distortion of the geometry that costs no energy, a direction in which the action does not change to second order. In continuous general relativity, one such mode is obvious: if you rescale the whole spacetime uniformly, nothing physical changes. A discrete theory should reproduce that freedom. The module in question checks a subtler version of this for a specific lattice, a regular grid of tetrahedra, and it does so with a machine-checked proof.

In Recognition Science, the framework models this lattice gravity through a ledger, a discrete record of geometric events, and asks whether its cost function has the required flat directions. The module, called Regge TT hinge-aware zero mode, analyzes the second variation of the Regge action on this lattice. The headline result is a theorem: the assembled constant block, the part of the second variation that responds to distortions that are the same everywhere, vanishes identically for every possible polarization matrix. In plain terms, constant metric perturbations are exact flat directions of the lattice, with no exceptions.

The proof is not a numerical check but an algebraic identity. The raw table of second derivatives, contracted over the six tetrahedron types in the lattice, turns out to be a perfect square: (c0 + c1 + c2 - c3 - c4 - c5 + c6)^2 / 2, where the c's are the edge-class coefficients. The alternating class sum vanishes for every polarization because of a termwise identity in the coefficients themselves. This is the kind of structural cancellation that a symbolic calculation can suggest but only a formal proof can pin down.

The module also records a concrete witness for the transverse-traceless (TT) condition, a specific polarization and wave vector where the cancellation happens. At that witness, the hinge block and the stencil-only residual are equal and opposite, so their sum is zero. The proof fixes the sign convention that makes the cancellation work, so no silent sign error can creep in. The result extends to the full Bloch symbol at zero wave vector: the lattice flat zero mode exists as a statement about the true nonlinear Regge action's second variation, for every lattice size.

What this establishes, in the framework's own terms, is that the discrete gravity it studies has the same flat directions as the continuous theory. That is a necessary consistency check for any discrete approach to gravity, and here it is not assumed but proved, with the proof checked by a machine.

THEOREM ttWitness_isTT · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean
ttWitness_isTT · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean:146 
/-- 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
THEOREM zeroMomentum_symbol_is_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean
zeroMomentum_symbol_is_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean:478 
/-- **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
THEOREM rawCellStencil_zeroMomentum · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean
rawCellStencil_zeroMomentum · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean:405 
/-- The `k = 0` raw cell stencil is `2` times the per-cell assembled
constant block: the cell sum contributes exactly `N ^ 3` identical
copies, and the `2 / N ^ 3` normalization leaves the factor `2`. -/
theorem rawCellStencil_zeroMomentum (N : ℕ) [NeZero N]
    (E : Fin 3 → Fin 3 → ℝ) :
    rawCellStencil N E (fun _ => (0 : ℤ)) = 2 * assembledConstantBlock E := by
  unfold rawCellStencil
  have hterm : ∀ (τ : PeriodicTet N N N) (f g : Fin 6),
      rawCellStencilTerm N E (fun _ => (0 : ℤ)) τ f g =
        rawJacobianCoefficient f g *
          polEdgeCoeff E (slotDispClass τ.2 f) *
          polEdgeCoeff E (slotDispClass τ.2 g) := by
    intro τ f g
    unfold rawCellStencilTerm rawJacobianCoefficient
    rw [commensurateMomentum_zero N,
      planeWaveTetVelocity_zeroMomentum N E τ f,
      planeWaveTetVelocity_zeroMomentum N E τ g]
    ring
  have hsum : (∑ τ : PeriodicTet N N N, ∑ f : Fin 6, ∑ g : Fin 6,
      rawCellStencilTerm N E (fun _ => (0 : ℤ)) τ f g) =
      (N : ℝ) ^ (3 : ℕ) *
        ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
          rawJacobianCoefficient f g *
            polEdgeCoeff E (slotDispClass t f) *
            polEdgeCoeff E (slotDispClass t g) := by
    calc
      (∑ τ : PeriodicTet N N N, ∑ f : Fin 6, ∑ g : Fin 6,
          rawCellStencilTerm N E (fun _ => (0 : ℤ)) τ f g)
          = ∑ cell : Vertex N N N, ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
              rawJacobianCoefficient f g *
                polEdgeCoeff E (slotDispClass t f) *
                polEdgeCoeff E (slotDispClass t g) := by
            rw [Fintype.sum_prod_type]
            refine Finset.sum_congr rfl fun cell _ => ?_
            refine Finset.sum_congr rfl fun t _ => ?_
            refine Finset.sum_congr rfl fun f _ => ?_
            refine Finset.sum_congr rfl fun g _ => ?_
            exact hterm (cell, t) f g
      _ = (Fintype.card (Vertex N N N) : ℝ) *
            ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
              rawJacobianCoefficient f g *
                polEdgeCoeff E (slotDispClass t f) *
                polEdgeCoeff E (slotDispClass t g) := by
            rw [Finset.sum_const, nsmul_eq_mul, Finset.card_univ]
      _ = (N : ℝ) ^ (3 : ℕ) *
            ∑ t : Fin 6, ∑ f : Fin 6, ∑ g : Fin 6,
              rawJacobianCoefficient f g *
                polEdgeCoeff E (slotDispClass t f) *
                polEdgeCoeff E (slotDispClass t g) := by
            congr 1
            rw [show Fintype.card (Vertex N N N) = N * (N * N) by
              simp [Fintype.card_prod]]
            push_cast
            ring
  rw [hsum]
  unfold assembledConstantBlock
  have hN : ((N : ℝ)) ^ (3 : ℕ) ≠ 0 := by
    have hcast : (N : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.pos_of_neZero N).ne'
    positivity
  have hkey : ∀ (A S : ℝ), A ≠ 0 → (2 / A) * -(A * S) = 2 * -S := by
    intro A S hA
    field_simp
  exact hkey _ _ hN
THEOREM zeroMomentum_symbol_is_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean
zeroMomentum_symbol_is_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean:478 
/-- **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

What this page does not claim

This module does not prove the full Hessian decomposition for all configurations, only the assembled block at the recorded witness. It does not claim that all zero modes of the lattice are constant; only that constant ones exist. It does not address the stability of the lattice under non-constant perturbations.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND