Gravity Analysis Regge Ttlocal Symbol Existence Deficit Plane Wave Cont Diff At

The local smoothness guarantee

In the Recognition Science framework's research program on quantum gravity, one line of attack studies how a discrete geometric structure called a Regge spacetime responds to a small disturbance. A Regge spacetime is built from flat tetrahedra glued together, and the disturbance in question is a plane wave, a simple periodic ripple in the shape of the tetrahedra. The declaration deficit_planeWave_contDiffAt concerns the angle deficit, which is the amount by which the angles around an edge fail to add up to a full circle, a measure of curvature in this discrete setting. The theorem proves that, for any single edge, this angle deficit varies smoothly as the plane wave's amplitude is varied near zero. More precisely, the function mapping the amplitude to the deficit is continuously differentiable of every finite order at the point where the wave is turned off. This is a local statement: it holds at the flat, undisturbed configuration, not globally across all possible amplitudes.

The proof rests on a chain of smoothness results. First, the squared lengths of the edges of any tetrahedron change in a simple affine way, meaning they are a constant plus a term proportional to the amplitude, so they are smooth. Because the flat configuration is nondegenerate, with all edge lengths positive and all angles strictly between zero and a straight angle, the formulas for the dihedral angles are smooth functions of these edge lengths. The angle deficit is built from these angles, and the theorem assembles the pieces to show the whole deficit is smooth. The result is a stepping stone toward a larger goal: defining a Bloch symbol, a quantity that encodes how the Regge action, the discrete analogue of the Einstein-Hilbert action, responds to a plane wave. The existence of this symbol at a fixed lattice size is the first existence theorem of the program, and the smoothness of the deficit is a necessary ingredient for that existence proof.

What the declaration does not claim is just as important as what it proves. It does not compute the value of the Bloch symbol; it only establishes that the symbol exists and identifies it as a second derivative of the action profile. The specific continuum value that the program ultimately targets remains an open problem. The theorem is also fixed at a single lattice size, meaning it says nothing about what happens as the lattice becomes infinitely fine, the continuum limit. The smoothness is local, at the flat point, and does not assert smoothness for large amplitudes. Finally, the theorem concerns the angle deficit of a single edge in a single tetrahedron; it is a local geometric fact, not a statement about the global behavior of the entire spacetime.

/-- Each edge deficit along the plane-wave family is `ContDiffAt` at `0`
(constant `2π` minus a finite sum of smooth contributions). -/
theorem deficit_planeWave_contDiffAt (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
    (e : PeriodicEdge N N N) (n : ℕ∞) :
    ContDiffAt ℝ n
      (fun t : ℝ => deficitOfField N (planeWaveEdgeField N E k t) e) 0 := by
  unfold deficitOfField
  refine ContDiffAt.sub contDiffAt_const ?_
  exact ContDiffAt.sum fun cellTet _ =>
    edgeAngleContribution_planeWave_contDiffAt N E k e cellTet n

/-- (a) THEOREM, affine coordinates: along the plane-wave family every
local squared-edge coordinate is `flat + t · velocity`, with the flat value
the canonical Freudenthal tuple. -/
theorem planeWaveTetSqEdges_apply (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
    (cellTet : PeriodicTet N N N) (t : ℝ) (f : Fin 6) :
    tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet f =
      freudenthalTetSqEdges f + t * planeWaveTetVelocity N E k cellTet f := by
  simp only [tetSqEdgesOfField, planeWaveEdgeField, planeWaveTetVelocity]
  rw [show freudenthalTetSqEdges f =
      periodicDispSqEdge ((localEdgeOf cellTet.1 cellTet.2 f).disp) from
    freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf cellTet.1 cellTet.2 f]
  ring

/-- (a) THEOREM, smoothness: the local squared-edge path is `C^n` in the
amplitude for every order (it is affine). -/
theorem planeWaveTetSqEdges_contDiff (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
    (cellTet : PeriodicTet N N N) (n : ℕ∞) :
    ContDiff ℝ n
      (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet) := by
  have h : (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet) =
      fun t : ℝ => fun f : Fin 6 =>
        freudenthalTetSqEdges f + t * planeWaveTetVelocity N E k cellTet f := by
    funext t f
    exact planeWaveTetSqEdges_apply N E k cellTet t f
  rw [h]
  refine contDiff_pi.mpr fun f => ?_
  exact contDiff_const.add (contDiff_id.mul contDiff_const)

/-- (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 declaration does not compute the value of the Bloch symbol, only its existence and identification as a second derivative. The theorem does not address the continuum limit as the lattice size grows. The smoothness is local at the flat point and does not extend to large wave amplitudes.

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: