Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloser

show as:
view Lean formalization →

Algebraic closure layer for the transported all-orbit 4D Regge continuum symbol: equates the finite transported symbol to the distinct-hinge Bloch fold, packages T11 ray evaluations, and pins uniqueness of the continuum limit. Gravity analysts cite it when wiring the transported m² quadratic form into the tensor closer or flat second-variation path. Argument is mostly transport-and-fold equalities plus tendsto closures already proved on axis TT and pure gauge.

claimOn the 4D Regge mesh with transported all-orbit Bloch data, the finite transported symbol equals the distinct-hinge Bloch fold (and the full orbit sum). The continuum symbol is the unique limit of that sequence along the frozen weak-field directions; the $(1,1)$ T11 contribution admits closed $m^2$ ray evaluations on axis TT-plus and pure-gauge decoys.

background

This sits in the QG full-theory 4D continuum campaign. Upstream, EdgeTTDecomposition4D supplies the linear-algebra transverse-traceless split of symmetric $4\times 4$ matrices against a nonzero Euclidean wave covector. Regge4DContinuumPreflight freezes the independent continuum target, mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before any recovery claim.

The Bloch stack builds the phase-decorated fold of the true-weight flat Hessian for type-$(1,1)$ hinges (ReggeBlochFold4D), its small-momentum $m^2$ symbol (ReggeBlochM2Symbol4D), and punctured Tendsto along the symbol direction for axis TT and pure gauge (ReggeBlochM2Tendsto4D). ReggeBlochTransportedAllOrbit4D extends to a continuum-facing multi-orbit fold: each slot transports its seed area covector and star deficit kernel by the orbit-covering $S_4$ permutation (not the factorized transport used only for $(1,1)$).

The module doc frames the continuum sequence as a compatibility alias of the distinct-hinge fold, so downstream code can quote one name for the transported algebraic object.

proof idea

Definition-and-equality module, not a single deep theorem. It introduces Mat4 and the finite transported symbol, then proves it equals the distinct-hinge Bloch fold and the full orbit sum by unwinding the transported fold against the hinge-orbit classification and edge stencil. Scalar-multiplication and zero cases are direct. T11 specializations reduce to the already-closed $m^2$ symbol and the cosine two-jet tendsto lemmas on axis TT-plus and decoy gauge. Continuum uniqueness is the standard unique-limit argument once the fold sequence is identified and the punctured tendsto is in hand.

why it matters in Recognition Science

Feeds three parents. Regge4DTensorAlgebraicCloser banks the transported distinct-hinge $m^2$ as a quadratic form in $(E,\mathrm{dir})$ on the TT variety; this module is the algebraic identification that makes those ray evaluations speak about one continuum symbol. Regge4DFlatSecondVariation mirrors the 3D Schläfli-elevated edge Hessian contract and needs a closed continuum-facing second-variation symbol on the flat seed. The audit module checks the axiom footprint stays at propext, Classical.choice, and Quot.sound.

In the campaign ladder this is the transported counterpart of the 3D algebraic closer: it does not yet claim a universal adjugate-style tensor identity (that remains open in the tensor closer), but it removes naming and fold-vs-transport ambiguity so later gates can cite a single continuum sequence.

scope and limits

used by (3)

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

depends on (8)

Lean names referenced from this declaration's body.

declarations in this module (31)