Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.Regge4DFlatSecondVariation

show as:
view Lean formalization →

Assembles the flat-background second variation of 4D Regge calculus on the Freudenthal lattice: Schläfli identities, zero-momentum candidates, and vanishing on TT and pure-gauge modes. Gravity analysts in the Regge-to-EH continuum campaign cite it for the algebraic Hessian layer. Content is identity packaging, candidate definitions, and evaluations against preflight decoys rather than a single deep proof.

claimModule collecting flat Freudenthal 4-simplex Schläfli identities and the associated second-variation candidates on the 4D Regge lattice, including vanishing of the Schläfli candidate on transverse-traceless and pure-gauge modes at zero momentum, with local matrix type $4\times 4$ inherited from continuum preflight.

background

Recognition Science's quantum-gravity lane treats 4D Regge calculus on a periodic Freudenthal triangulation as the discrete precursor of weak-field Einstein-Hilbert. Continuum recovery is staged: freeze targets and decoys first, then close algebraic identities, then pass to Bloch symbols and the torus limit.

Upstream, Regge4DContinuumPreflight freezes the weak-field EH target, canonical mesh, normalized TT data, pure-gauge family, and honesty decoys before any continuum claim. EdgeTTDecomposition4D supplies the linear-algebra transverse-traceless split of symmetric $4\times 4$ matrices against a nonzero Euclidean wave covector. Regge4DSchlaefliPathwise mirrors the 3D six-edge closed-form Schläfli identity at the 4-simplex ($n_H = n_E = 10$), flat and directional. The dimension-parametric Schläfli interface in SchlaefliN states the finite-index $n$-dimensional identity that 3D and 4D instantiate.

Related closers bank transported distinct-hinge $m^2$ as a quadratic form on the TT variety (Regge4DTensorAlgebraicCloser) and the finite periodic action sequence with density $N^{-4}$ (Regge4DTorusContinuumLimit). This module sits at the flat second-variation seam between those layers.

proof idea

Definition-and-identity module, not a single theorem proof. It aliases the preflight $4\times 4$ matrix type, records presence and closed-form statements of the flat and directional Freudenthal Schläfli identities, and packages seed-angle differentiability. Zero-momentum and fold Schläfli candidates are defined and equated to their explicit forms, then shown to vanish on the axis TT+ sector and on the pure-gauge decoy family. Downstream Hessian and Bloch assembly import these vanishings rather than re-deriving them.

why it matters in Recognition Science

Second variation on a flat background is the discrete stand-in for the linearized EH kinetic term. Without controlled vanishing of the Schläfli candidate on TT physical modes and on pure gauge, the continuum symbol cannot match the frozen weak-field target from preflight. The module therefore supplies the algebraic hinge between pathwise Schläfli (Regge4DSchlaefliPathwise), TT decomposition, and the torus continuum dictionary (Regge4DTorusContinuumLimit). No downstream consumers are wired yet in the graph; the intended parents are the 4D Bloch/Hessian assembly and continuum-limit theorems in the same Gravity.Analysis lane. It does not itself claim continuum recovery of Einstein-Hilbert.

scope and limits

depends on (11)

Lean names referenced from this declaration's body.

declarations in this module (30)