Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.ReggeTTLocalSymbolExistence

show as:
view Lean formalization →

Gate A1 in the Regge TT continuum-symbol program: local C^infty existence of the plane-wave action profile and its geometric ingredients (edge lengths, dihedral angles, deficits) at the flat background. Gravity analysts cite it before any second-variation or symbol-extraction step. The module assembles positivity of squared edge displacements with a chain of contDiffAt lemmas along the frozen TT plane-wave family.

claimAlong the frozen transverse-traceless plane-wave deformation of a Euclidean tetrahedron, the squared edge lengths, square-root edge map, dihedral angles, angle contributions, deficit angles, and Regge action profile are $C^\infty$ at the flat point; squared displacement class values are strictly positive ($1,1,1,2,2,2,3$).

background

This module sits in the QG full-theory campaign under ReggeTTContinuumSymbol. Stage 1 (ReggeTTSymbolPreflight) fixed the true nonlinear Regge action, its flat point, the frozen-model identification, and the TT Bloch symbol object. Stage 2 Gate 0 / Lane A (ReggeTTDerivativeGate) already controls first-derivative structure at flat and is imported, never re-proved.

The local objects are plane-wave tetrahedron kinematics: squared edge displacements by lattice class, edge values and their square roots, tetrahedral dihedral angles, edge-angle contributions, and the deficit that enters the Regge action. The plane-wave action profile is the scalar obtained by evaluating that action on the frozen TT deformation. Continuous differentiability is taken in the Mathlib ContDiffAt sense at the zero-amplitude (flat) point.

Downstream Gate A2 treats the Schläfli-reduced flat second variation; that gate explicitly lists this module as Gate A1 of the panel-locked "Normalization-Gated Schläfli Two-Jet" protocol.

proof idea

Not a single theorem: a lemma stack. Positivity of periodic squared-displacement class values (the constants 1,1,1,2,2,2,3) opens the square-root edge map. Plane-wave squared edges are identified, shown to vanish at zero amplitude, and proved $C^\infty$. ContDiffAt is then pushed through edge values, dihedral angles, edge-angle contributions, deficits, and square-root edges, culminating in contDiffAt of the plane-wave action profile at flat. A slope-average identity closes the local linear response used by later gates. Imports supply the preflight action and the derivative gate; no second-variation work is done here.

why it matters in Recognition Science

Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol. Without local smooth existence of the action profile and its geometric factors at flat, the continuum TT symbol cannot be extracted from a second jet. The sole recorded consumer is ReggeTTFlatSecondVariation (Gate A2, Crux-1(c) lane), whose module doc states that Gate A1 is this file and that first-derivative structure is reused from ReggeTTDerivativeGate. In the broader Recognition gravity stack this is the analytic license to pass from discrete Regge data on a tetrahedral complex to a local continuum symbol for the TT sector, after Stage-1 preflight and before Schläfli-reduced second variation.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (15)