Gravity Analysis Regge Ttsymbol Preflight Plane Wave Edge Field Zero Amplitude

The plane wave at zero amplitude

Regge calculus is a discrete approximation to general relativity in which spacetime is built from flat tetrahedra glued along their faces. The geometry is encoded entirely in the squared lengths of the edges, and the gravitational action is a sum over edges of the deficit angle, the angle by which the tetrahedra around an edge fail to close flat. A plane wave perturbation is a specific way of wiggling those edge lengths with a cosine profile, controlled by an amplitude parameter t and a wave vector k.

The theorem planeWaveEdgeField_zero_amplitude states that when the amplitude t is set to zero, the perturbed edge-length field is exactly the flat field, the one with all squared lengths equal to their flat-space values. This is a sanity condition: a zero-amplitude wave is no wave at all. The proof is a direct calculation from the definitions, and the same result implies that the action evaluated on the zero-amplitude wave is zero, because the flat configuration has vanishing deficit angles everywhere.

This fact is the starting point for studying how the true nonlinear Regge action responds to small plane wave perturbations. The second difference of the action with respect to the amplitude, normalized per unit cell, is the object that would reveal the effective propagation properties of gravitational waves on this discrete lattice. The zero-amplitude theorem ensures that this second difference is well-defined around the flat background, and it is the first step toward asking whether the continuum limit of that object is isotropic, as general relativity would suggest.

In Recognition Science, this theorem is part of a larger program to derive gravitational structure from a discrete ledger of recognition events. The framework models spacetime as a periodic lattice and studies the true nonlinear action rather than a linearized approximation. The theorem itself is a modest but necessary piece: it establishes the baseline from which all perturbation analysis proceeds.

What the theorem does not claim is just as important. It does not establish that the second difference converges to any particular value, nor that the continuum limit is isotropic. Those are open targets, and the numerical evidence suggesting a value of -1/4 remains numerical evidence, not a proof. The theorem only pins down the zero-amplitude point, a small but solid anchor for the larger investigation.

/-- At amplitude `0` the plane-wave family sits at the flat field. -/
theorem planeWaveEdgeField_zero_amplitude (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) :
    planeWaveEdgeField N E k 0 = flatEdgeField N := by
  funext e
  simp only [planeWaveEdgeField, flatEdgeField, zero_mul, add_zero]

/-- The action profile vanishes at amplitude `0` (flat point of the
family). -/
theorem planeWaveActionProfile_zero (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) :
    planeWaveActionProfile N E k 0 = 0 := by
  unfold planeWaveActionProfile
  rw [planeWaveEdgeField_zero_amplitude, trueReggeAction_flatEdgeField]

/-- 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]

What this page does not claim

The theorem does not prove the existence or value of any continuum limit for the TT Bloch symbol. The theorem does not establish that the true Regge action is isotropic in the continuum limit. The theorem does not claim that the frozen graph-Laplacian model is the correct quadratic approximation for plane wave 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/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: