Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.Regge4DTensorAlgebraicCloser

show as:
view Lean formalization →

Packages the distinct-hinge contribution to the transported small-momentum symbol as an explicit quadratic form on 4D polarization tensors. Continuum-closure work in the Regge gravity lane cites it when converting multi-orbit Bloch folds into continuum face moments. Algebraic identities for hinge-moment forms on TT axes and normalized faces are banked here; full Einstein-Hilbert Tendsto is not claimed.

claimIn 4D Regge calculus, the distinct-hinge transported small-momentum symbol $m^2$ is realized as a quadratic form $Q(h)$ on symmetric polarization tensors $h\in\mathrm{Sym}^2(\mathbb{R}^4)$. The form admits closed evaluations on normalized TT-plus and TT-cross axes and on continuum face directions (including vanishing statements on pure $e_0$ channels).

background

This module sits in the QG full-theory 4D continuum-closure campaign. Upstream, the edge TT decomposition supplies the linear-algebra transverse-traceless split of symmetric $4\times 4$ matrices against a nonzero Euclidean wave covector. The continuum preflight freezes the weak-field Einstein-Hilbert target, canonical mesh carrier, normalized TT data, and honesty decoys before any recovery claim. The torus continuum-limit module supplies the action-symbol dictionary on the finite periodic Freudenthal sequence (side $N=j+3$, density $N^{-4}$).

The transported algebraic closer binds that preflight Prop to the multi-orbit fold and banks identities without inhabiting $S_{RS}\to EH$. The Bloch $m^2$ symbol module isolates the $(1,1)$-orbit small-momentum contribution; the transported all-orbit fold moves each orbit's seed area covector and star-deficit kernel by the $S_4$ covering permutation. Distinct-hinge work here means the hinge contributions that are not absorbed into the single-orbit factorized picture.

proof idea

Definition-and-identity module, not a single end-to-end theorem. It introduces a $4\times 4$ matrix carrier and the distinct-hinge moment form as a quadratic form in the polarization, then records scalar-multiplication and zero lemmas. Axis evaluations pin the form on TT-plus and TT-cross symbol directions and on the $e_0$ channel. Continuum-face normalizations give matching evaluations (plus a vanishing statement for the normalized-plus face along $e_0$). An open closed-form marker records what remains for the distinct-hinge tensor identity. Arguments are algebraic reductions against the imported TT decomposition and transported-orbit $m^2$ evaluations.

why it matters in Recognition Science

Feeds the 4D flat second-variation stack, which mirrors the 3D contract elevating the nonlinear Regge action to a Schläfli-reduced edge Hessian (Gate A2). Downstream audit imports this module to track partial closure of the tensor algebraic layer. In the broader forcing picture this is continuum gravity bookkeeping, not a T0-T8 landmark: it supplies the polarization quadratic form needed before any claim that the transported multi-orbit fold recovers the Einstein-Hilbert second variation on flat seeds. Without the distinct-hinge form, face-moment matching between Bloch symbols and continuum TT data stays informal.

scope and limits

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.

declarations in this module (21)