Encyclopedia Gravity Gravity Analysis Regge Tthinge Aware Zero Mode Raw Cell Stencil Zero Momentum

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Tthinge Aware Zero Mode Raw Cell Stencil Zero Momentum

In a discrete lattice model of gravity, a flat, unchanging metric perturbation is a direction of zero energy cost, and a machine-checked proof now pins down that fact.

Verify this page

The flat zero mode

In the Regge calculus approach to gravity, spacetime is chopped into flat tetrahedral pieces, and the metric is described by the edge lengths of this lattice. A natural question is whether a small, uniform change to those lengths, a constant perturbation that does not vary from cell to cell, costs any energy at all. The declaration rawCellStencil_zeroMomentum answers this for a specific, carefully assembled object: it proves that the raw cell stencil, the per-cell contribution to the second variation of the Regge action, evaluated at zero wave vector, is exactly twice the assembled constant block. This is a stepping stone, not the final statement.

The final statement is the zero-mode headline. The assembled constant block, which combines the hinge and Hessian contributions, vanishes identically for every polarization matrix. This means that a constant, uniform perturbation of the lattice metric is an exact flat direction: it costs no energy at all, in the second variation of the true nonlinear Regge action. The proof is a clean algebraic identity. The raw-table contraction over the six tetrahedron types is a perfect square, and the alternating class sum vanishes for every polarization. The result is stronger than the campaign asked for: it does not require the trans-traceless (TT) gauge condition that was originally part of the hypothesis. The TT condition is a special case, not a necessary one.

In Recognition Science, this is a theorem about the framework's model of gravity on a lattice. The framework's library, a machine-checked collection of formal theorems, proves that at zero momentum the Bloch symbol, the Fourier-transformed version of the stencil, is zero for every lattice size and every polarization. This is the lattice flat zero mode, a statement about the second variation of the Regge action. It is a precise, formal result, not a numerical approximation.

What the declaration does not claim is just as important. It does not prove that the full Hessian decomposition, the split into hinge and per-tetrahedron contributions, holds everywhere. That split is only kernel-checked at a specific recorded witness, the concrete TT example the diagnostic found. Everywhere else, it lives at the level of a symbolic computation diagnostic, not a formal proof. The theorem also does not require the TT condition, so it is not a statement about TT perturbations specifically. It is a statement about all constant perturbations.

The practical consequence is a clean, checkable fact about the lattice theory: constant metric perturbations are exact flat directions. This is a necessary consistency condition for any discrete gravity model that hopes to recover general relativity in the continuum limit. The proof removes a potential obstruction and pins down the sign convention in the assembly of the stencil, so no silent sign error can hide in the construction.

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 w00 · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean
w00 · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean:228 
private theorem w00 : rawJacobianCoefficient 0 0 = (0 : ℝ) := by
  rw [rawJacobianCoefficient_eval 0 0]; norm_num [ReggeTTBucketAggregation.rationalStencilWeight]
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

The full Hessian decomposition is not proved in Lean for all configurations, only at a specific witness. The theorem does not require the TT gauge condition, so it is not a statement about TT perturbations only. The result does not establish that the Regge action itself is zero, only its second variation at zero momentum.

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