Encyclopedia Gravity Gravity Analysis Regge Tthinge Aware Zero Mode Zero Mode Free Coefficients

ARTICLE 4 claims 4 theorems

Gravity Analysis Regge Tthinge Aware Zero Mode Zero Mode Free Coefficients

A machine-checked proof shows that a lattice version of gravity has a flat direction: constant distortions cost no energy, for any polarization.

Verify this page

The flat zero mode

In the Recognition Science framework, where reality keeps a discrete ledger of events, gravity is studied on a lattice of tetrahedra. A key question is whether certain distortions of this lattice cost energy. The declaration zeroMode_free_coefficients establishes an identity: the energy contribution from a constant distortion, computed from a sum over the six tetrahedron types, is the perfect square (c0 + c1 + c2 - c3 - c4 - c5 + c6)^2 / 2, an identity in seven free coefficients.

This identity is the core of a theorem: the assembled constant block vanishes identically, for every polarization matrix. In plain terms, a uniform, constant distortion of the lattice is an exact flat direction of the action. This means it costs no energy to shift the entire lattice uniformly. This result is stronger than what was asked for: it holds for all polarizations, not just the transverse-traceless (TT) ones that the diagnostic originally targeted. The TT case is a special instance of this more general result.

The proof also pins down the assembly sign convention. A separate diagnostic found that the hinge term and the stencil-only residual both equal -pi*(sqrt 2 + 4)/8 at a specific test point. The kernel-checked theorem assembled_witness_split shows the assembled block is the hinge term minus the stencil residual, which is zero, confirming the relative minus sign. This is a concrete check that the cancellation is real, not a sign error.

What the declaration does not claim is also precise. The full decomposition of the assembled block into a hinge part and a sum over per-tetrahedron Hessians is not re-proved in the machine-checked library. The split is verified only at the recorded test witness. The vanishing of the constant block is a statement about the true nonlinear Regge action's second variation at zero wave vector, not a statement about the full Hessian decomposition. The result is pure algebra, relying only on the standard axiom trio, with no new axioms introduced.

This flat zero mode is a structural fact about the lattice theory. It tells us that the lattice action has a continuous family of minima, all related by constant shifts. This is a property that must be handled carefully in any quantization or perturbation scheme, because it signals a gauge-like freedom. The proof shows this freedom is exact, not an artifact of a particular approximation.

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 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 ttWitnessWaveVector · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean
ttWitnessWaveVector · IndisputableMonolith/Gravity/Analysis/ReggeTTHingeAwareZeroMode.lean:130 
/-- The witness wave vector `k = e_z` (integer form `m = (0,0,1)`). -/
def ttWitnessWaveVector : Fin 3 → ℤ
  | 0 => 0
  | 1 => 0
  | 2 => 1
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 decomposition of the assembled block into hinge and per-tetrahedron Hessian parts is not proved for all configurations. The result does not imply that all constant distortions are physically unobservable in the full theory. The proof does not use or require the transverse-traceless condition for the vanishing of the constant block.

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