Encyclopedia Gravity Gravity Analysis Regge Ttlocal Symbol Existence Plane Wave Ttbloch Symbol Is Sec

ARTICLE 3 claims 3 theorems

Gravity Analysis Regge Ttlocal Symbol Existence Plane Wave Ttbloch Symbol Is Sec

A machine-checked proof establishes that a well-defined quantity, the Bloch symbol, exists for every plane-wave state in a discrete model of gravity, without yet computing its value.

Verify this page

The fixed-N Bloch symbol

In solid-state physics, a Bloch symbol is a function that describes how a wave behaves as it moves through a periodic structure, such as a crystal lattice. The declaration planeWave_TTBlochSymbolIs_secondVariation is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It proves that for a discrete model of gravity built from tetrahedra, a specific quantity, the fixed-N TT Bloch symbol, exists for every possible plane-wave state. The proof is a chain of logical steps verified by a computer, with no unproven assumptions beyond the standard axioms of the underlying type theory.

The theorem identifies this symbol with the second derivative of the action, a measure of how the system's energy changes as the wave's amplitude varies. Specifically, the symbol equals (2/N³) times the second derivative of the action profile at zero amplitude, where N is the lattice size. This is an identification of the limit, not a calculation of its value. The proof works by showing that the action profile is smooth at the flat, regular tetrahedral configuration, and then using a general result about centered second differences to connect the discrete definition to the continuous second derivative.

This is the first existence theorem of its kind in the program. It establishes that the object the framework set out to study is well-defined and non-vacuous. The theorem does not, however, provide a numerical value for the symbol. The target value of -1/4 in the continuum limit, where the lattice spacing goes to zero, remains an open problem. The proof is also limited to a fixed lattice size N; it does not establish anything about the limit as N grows large. The numerical evidence for the continuum value comes from separate computations and is not part of this theorem.

For a reader, the practical consequence is a firm foundation: the framework can now ask questions about the value of this symbol, knowing that the object itself exists. This is a necessary first step before any attempt to connect the discrete model to continuous physics, such as the propagation of gravitational waves. The existence result is a milestone, but the journey from this formal existence to a physical prediction is still ahead.

THEOREM planeWave_TTBlochSymbolIs_secondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
planeWave_TTBlochSymbolIs_secondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:379 
/-- (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]
THEOREM planeWave_TTBlochSymbolIs_secondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
planeWave_TTBlochSymbolIs_secondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:379 
/-- (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]
THEOREM planeWave_TTBlochSymbolIs_secondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
planeWave_TTBlochSymbolIs_secondVariation · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:379 
/-- (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 provide a numerical value for the Bloch symbol. The theorem does not establish anything about the continuum limit as N grows large. The theorem does not prove that the continuum target value of -1/4 is correct.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND