Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.Regge4DContinuumPreflight

show as:
view Lean formalization →

Preflight infrastructure for the 4D Regge continuum limit on the periodic Freudenthal torus: lattice side length N=j+3, integer and real Bloch modes, wave/momentum norms, and 4×4 matrix carriers. Gravity analysts cite it before any continuum-symbol or second-variation argument. The module is definitional scaffolding plus elementary norm identities, not a deep existence proof.

claimOn the periodic Freudenthal 4-torus of side length $N=j+3$ ($j\ge 0$, hence $N\ge 3$), introduce integer modes $k\in\mathbb{Z}^4$, real wave covectors, squared wave and momentum norms (with $||k||^2$ identified to the momentum square), the canonical torus carrier, Frobenius norm on symmetric $4\times 4$ matrices, and the basic $4\times 4$ / wave-type aliases used by all downstream continuum symbols.

background

Recognition Science gravity analysis elevates discrete Regge calculus on a Freudenthal triangulation of the 4-torus toward a continuum TT symbol. The continuum family is indexed by lattice side length $N=j+3$ with $N\ge 3$, so the torus is large enough for nontrivial Bloch modes and orbit covers.

Upstream modules supply the algebraic ingredients this preflight packages: the linear-algebra transverse-traceless decomposition of symmetric $4\times 4$ matrices against a nonzero Euclidean wave covector; the 4D edge stencil and hinge classes; Bloch folds (including the small-momentum $m^2$ symbol of the $(1,1)$ orbit and the transported all-orbit fold); and the exact flat cross-term continuum symbol (oracle $H_{\mathrm{fold}}$) that annihilates vertex-gauge modes and sends normalized TT on the preferred axes to $-1/4$.

Local objects are deliberately thin: matrix and wave type aliases, integer/real mode maps, wave-norm and momentum-norm squares with their equality lemmas, Frobenius norm squared, and the named canonical torus. No new Hessian or kernel is redefined here.

proof idea

Definition module with elementary supporting lemmas. Side length is introduced as $N=j+3$ with a one-line inequality $N\ge 3$. Mode and norm declarations are pure defs or abbrevs; the nontrivial content is the identification of wave-norm squared with momentum-norm squared and the closed form of the momentum square, proved by direct expansion on $\mathrm{Fin},4$. Frobenius norm and torus carrier are definitional. No continuum limit, Schläfli identity, or TT isotropy is proved in-module.

why it matters in Recognition Science

This module is the frozen continuum preflight target consumed by the 4D algebraic and continuum closers. Downstream, Regge4DAlgebraicCloser banks algebraic witnesses against it and leaves full TT isotropy/gauge/plus-cross agreement OPEN; Regge4DTensorAlgebraicCloser treats the transported distinct-hinge $m^2$ as a quadratic form on the TT variety; Regge4DFlatSecondVariation elevates the true nonlinear Regge action toward a Schläfli-reduced edge Hessian; Regge4DTorusContinuumLimit and the transported/algebraic closers take the torus family and mode/norm package as given.

It also feeds the named closer for edge TT decomposition (algebraic TT split, Frobenius-normalized plus/cross witnesses, plane-wave edge attachment) and the Recognition-mesh exact-$J$ bridge that attaches a value-level action whose amplitude Hessian is the Option-C midpoint Bloch symbol on the same torus family. The companion audit module records the expected axiom footprint. In the QG full-theory campaign this is the 4D analogue of the 3D TT symbol preflight: fix carriers and norms before claiming continuum symbols or second variation.

scope and limits

used by (12)

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

depends on (10)

Lean names referenced from this declaration's body.

declarations in this module (68)