Encyclopedia Gravity Gravity Analysis Regge Ttlocal Symbol Existence Tet Dihedral Angle Plane Wave Co

ARTICLE 4 claims 3 theorems 1 model

Gravity Analysis Regge Ttlocal Symbol Existence Tet Dihedral Angle Plane Wave Co

A theorem in the Recognition Science library proves that the dihedral angles of a tetrahedron respond smoothly to a plane-wave disturbance, a key step toward defining a quantum gravity symbol.

Verify this page

Smoothness at the flat tetrahedron

A dihedral angle is the angle between two faces of a tetrahedron, the three-dimensional analog of the corner angle of a polygon. The declaration tetDihedralAngle_planeWave_contDiffAt concerns a specific family of tetrahedra: those obtained by displacing the vertices of a regular, flat tetrahedron with a plane-wave pattern of small amplitudes. The theorem states that, for any finite order of differentiability, each dihedral angle of such a tetrahedron is a smooth function of the wave amplitude at the point where the amplitude is zero. In plainer terms, as you turn on the wave, the angles change without any kinks or jumps, to any degree of precision you care to check.

This smoothness is not automatic. The angle between two faces is computed from the squared edge lengths of the tetrahedron, and those edge lengths are smooth functions of the amplitude because they are affine, meaning they change linearly. The key step is that the flat tetrahedron is nondegenerate: all six edges have positive length and all six dihedral angles lie strictly between zero and 180 degrees, so the formula for an angle from edge lengths is itself smooth there. Composing the smooth angle formula with the affine edge-length path yields the theorem.

The result is a technical lemma inside a larger program to construct a specific object in quantum gravity, the Regge TT Bloch symbol, which is meant to encode how a gravitational wave propagates on a discrete spacetime lattice. The theorem is one of several that together prove the symbol exists for any lattice size, polarization, and wave vector. The existence proof relies on this smoothness to take a second derivative of the action, the quantity whose variation gives the equations of motion.

In Recognition Science, this is a proved theorem in the machine-checked library of formal theorems, with no unproved assumptions beyond the standard logical axioms. The declaration itself does not compute the value of any angle, nor does it say anything about the value of the Bloch symbol. It only guarantees that the angles are well-behaved enough for the derivative to be taken. The actual numerical value of the symbol, and its behavior as the lattice spacing goes to zero, remain open targets.

MODEL tetDihedralAngle_planeWave_contDiffAt · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
tetDihedralAngle_planeWave_contDiffAt · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:153 
/-- (b) THEOREM: each local dihedral angle along the plane-wave family is
`ContDiffAt` at amplitude `0` of every finite order.  The flat point is the
nondegenerate Freudenthal tetrahedron (`cm3 = 8 > 0`, cosines
`√2/2, 0, 1/2` strictly inside `(-1,1)` — `ReggeTTDerivativeGate`
`flatCos_ne_endpoints`), so the angle map is `ContDiffAt` in the 6-tuple
there; composition with the affine path gives the amplitude smoothness. -/
theorem tetDihedralAngle_planeWave_contDiffAt (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (cellTet : PeriodicTet N N N) (f : Fin 6) (n : ℕ∞) :
    ContDiffAt ℝ n
      (fun t : ℝ => tetDihedralAngleOfField N (planeWaveEdgeField N E k t) cellTet f)
      0 := by
  have hangle : ContDiffAt ℝ n (fun a : SqEdges => dihedralAngle3Sq a f)
      freudenthalTetSqEdges :=
    Geometry.ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
      freudenthalTet f n (ReggeTTDerivativeGate.flatCos_ne_endpoints f)
  have hpath : ContDiffAt ℝ n
      (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet) 0 :=
    (planeWaveTetSqEdges_contDiff N E k cellTet n).contDiffAt
  have hangle' : ContDiffAt ℝ n (fun a : SqEdges => dihedralAngle3Sq a f)
      (tetSqEdgesOfField N (planeWaveEdgeField N E k 0) cellTet) := by
    rw [planeWaveTetSqEdges_zero]
    exact hangle
  have hcomp := ContDiffAt.comp (x := (0 : ℝ)) hangle' hpath
  exact hcomp.congr_of_eventuallyEq (by
    filter_upwards with t
    rfl)
THEOREM tetDihedralAngle_planeWave_contDiffAt · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
tetDihedralAngle_planeWave_contDiffAt · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:153 
/-- (b) THEOREM: each local dihedral angle along the plane-wave family is
`ContDiffAt` at amplitude `0` of every finite order.  The flat point is the
nondegenerate Freudenthal tetrahedron (`cm3 = 8 > 0`, cosines
`√2/2, 0, 1/2` strictly inside `(-1,1)` — `ReggeTTDerivativeGate`
`flatCos_ne_endpoints`), so the angle map is `ContDiffAt` in the 6-tuple
there; composition with the affine path gives the amplitude smoothness. -/
theorem tetDihedralAngle_planeWave_contDiffAt (E : Fin 3 → Fin 3 → ℝ)
    (k : Fin 3 → ℝ) (cellTet : PeriodicTet N N N) (f : Fin 6) (n : ℕ∞) :
    ContDiffAt ℝ n
      (fun t : ℝ => tetDihedralAngleOfField N (planeWaveEdgeField N E k t) cellTet f)
      0 := by
  have hangle : ContDiffAt ℝ n (fun a : SqEdges => dihedralAngle3Sq a f)
      freudenthalTetSqEdges :=
    Geometry.ReggeActionFirstVariation.dihedralAngle3Sq_contDiffAt_nonDegenerate
      freudenthalTet f n (ReggeTTDerivativeGate.flatCos_ne_endpoints f)
  have hpath : ContDiffAt ℝ n
      (fun t : ℝ => tetSqEdgesOfField N (planeWaveEdgeField N E k t) cellTet) 0 :=
    (planeWaveTetSqEdges_contDiff N E k cellTet n).contDiffAt
  have hangle' : ContDiffAt ℝ n (fun a : SqEdges => dihedralAngle3Sq a f)
      (tetSqEdgesOfField N (planeWaveEdgeField N E k 0) cellTet) := by
    rw [planeWaveTetSqEdges_zero]
    exact hangle
  have hcomp := ContDiffAt.comp (x := (0 : ℝ)) hangle' hpath
  exact hcomp.congr_of_eventuallyEq (by
    filter_upwards with t
    rfl)
THEOREM planeWaveTetSqEdges_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
planeWaveTetSqEdges_zero · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:115 
/-- At `t = 0` the local tuple is exactly the flat Freudenthal tuple. -/
theorem planeWaveTetSqEdges_zero (E : Fin 3 → Fin 3 → ℝ) (k : Fin 3 → ℝ)
    (cellTet : PeriodicTet N N N) :
    tetSqEdgesOfField N (planeWaveEdgeField N E k 0) cellTet =
      freudenthalTetSqEdges := by
  funext f
  rw [planeWaveTetSqEdges_apply, zero_mul, add_zero]
THEOREM planeWave_TTBlochSymbol_exists · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean
planeWave_TTBlochSymbol_exists · IndisputableMonolith/Gravity/Analysis/ReggeTTLocalSymbolExistence.lean:404 
/-- 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⟩

What this page does not claim

The theorem does not compute the value of any dihedral angle. The theorem does not evaluate the Regge TT Bloch symbol. The theorem does not establish the continuum limit of the symbol.

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