Gravity Analysis Regge Ttlocal Symbol Existence Plane Wave Ttbloch Symbol Exists

The existence theorem

In the study of quantum gravity, one often wants to know how a theory behaves when space is gently shaken by a wave. The Recognition Science framework analyzes this through a discrete model of spacetime built from tetrahedra, the simplest three-dimensional shapes. A plane wave, a disturbance that oscillates smoothly as it travels, is imposed on this tetrahedral grid. The question is whether a particular quantity, called the TT Bloch symbol, can be defined at all in this setting. The declaration planeWave_TTBlochSymbol_exists answers that question in the affirmative.

The theorem proves that for every side length N, every polarization matrix, and every integer wave vector, there exists a real number H such that the TT Bloch symbol equals H. The proof constructs H explicitly as a second derivative of the action profile, the function that measures the total energy of the configuration. Specifically, H equals (2/N³) times the second derivative of the action at zero amplitude. This is a statement about existence and identification of the limit, not about its numerical value.

The proof works by showing that the action profile is smooth at the flat configuration, where all tetrahedra are regular. It then uses a general lemma about centered second differences: if a function is twice differentiable at a point, the symmetric difference quotient converges to the second derivative there. This local argument avoids a global smoothness assumption that would fail for this family of waves. The result is the first existence theorem of its kind in the program.

What the theorem does not do is evaluate the symbol. The value of H is not computed; the continuum target of -1/4 remains an open problem. The result also holds only at fixed N, with no limit taken as the grid becomes infinitely fine. Numerical evidence suggests the continuum value, but that evidence is not a proof. The theorem establishes that the symbol is well-defined, which is a necessary first step, but it leaves the quantitative question for future work.

/-- Companion existence form: there IS a real number `H` with
`TTBlochSymbolIs N E m H` — the fixed-`N` symbol object is non-vacuous for
every polarization and wave vector. -/
theorem planeWave_TTBlochSymbol_exists (E : Fin 3 → Fin 3 → ℝ)
    (m : Fin 3 → ℤ) :
    ∃ H : ℝ, TTBlochSymbolIs N E m H :=
  ⟨_, planeWave_TTBlochSymbolIs_secondVariation N E m⟩

/-- (e) HEADLINE THEOREM (first existence theorem of the program): for
every side `N`, every polarization matrix `E`, and every integer wave
vector `m`, the fixed-`N` TT Bloch symbol EXISTS and equals
`(2/N³) · S''(0)` where `S` is the plane-wave action profile of the TRUE
nonlinear Regge action.  Exact bookkeeping: the preflight's
`ttSecondDifference` is `(2/N³) · [(S(t) − 2S(0) + S(−t))/t²]` and the
bracket converges to `iteratedDeriv 2 S 0` by the local bridge (d) — no
stray `1/2` anywhere.  NOTE: this identifies the LIMIT, not its value; the
continuum `-(1/4)` target remains OPEN. -/
theorem planeWave_TTBlochSymbolIs_secondVariation (E : Fin 3 → Fin 3 → ℝ)
    (m : Fin 3 → ℤ) :
    TTBlochSymbolIs N E m
      ((2 / (N : ℝ) ^ (3 : ℕ)) *
        iteratedDeriv 2 (planeWaveActionProfile N E (commensurateMomentum N m)) 0) := by
  set k : Fin 3 → ℝ := commensurateMomentum N m with hk
  set S : ℝ → ℝ := planeWaveActionProfile N E k with hS
  have hC2 : ContDiffAt ℝ 2 S 0 := planeWaveActionProfile_contDiffAt N E k 2
  have hbridge := tendsto_centeredSecondDifference_of_contDiffAt S hC2
  unfold TTBlochSymbolIs
  have hconst := hbridge.const_mul (2 / (N : ℝ) ^ (3 : ℕ))
  refine hconst.congr' ?_
  filter_upwards with t
  unfold ttSecondDifference
  rw [← hk, ← hS, mul_div_assoc]

/-- (e) HEADLINE THEOREM (first existence theorem of the program): for
every side `N`, every polarization matrix `E`, and every integer wave
vector `m`, the fixed-`N` TT Bloch symbol EXISTS and equals
`(2/N³) · S''(0)` where `S` is the plane-wave action profile of the TRUE
nonlinear Regge action.  Exact bookkeeping: the preflight's
`ttSecondDifference` is `(2/N³) · [(S(t) − 2S(0) + S(−t))/t²]` and the
bracket converges to `iteratedDeriv 2 S 0` by the local bridge (d) — no
stray `1/2` anywhere.  NOTE: this identifies the LIMIT, not its value; the
continuum `-(1/4)` target remains OPEN. -/
theorem planeWave_TTBlochSymbolIs_secondVariation (E : Fin 3 → Fin 3 → ℝ)
    (m : Fin 3 → ℤ) :
    TTBlochSymbolIs N E m
      ((2 / (N : ℝ) ^ (3 : ℕ)) *
        iteratedDeriv 2 (planeWaveActionProfile N E (commensurateMomentum N m)) 0) := by
  set k : Fin 3 → ℝ := commensurateMomentum N m with hk
  set S : ℝ → ℝ := planeWaveActionProfile N E k with hS
  have hC2 : ContDiffAt ℝ 2 S 0 := planeWaveActionProfile_contDiffAt N E k 2
  have hbridge := tendsto_centeredSecondDifference_of_contDiffAt S hC2
  unfold TTBlochSymbolIs
  have hconst := hbridge.const_mul (2 / (N : ℝ) ^ (3 : ℕ))
  refine hconst.congr' ?_
  filter_upwards with t
  unfold ttSecondDifference
  rw [← hk, ← hS, mul_div_assoc]

What this page does not claim

The theorem does not evaluate the symbol numerically. The theorem does not establish the continuum limit as N approaches infinity. The theorem does not prove the continuum target value of -1/4.

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