Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.Regge4DExactActionSymbol

show as:
view Lean formalization →

Exact 4D Regge action symbol assembled from lattice star-cube translates, transport offsets, and phased deficit pairings on the (1,1) and (1,2) orbits. Continuum-closure and EH-normalization work cite it as the discrete quadratic face before dictionary comparison. The module packages offsets, star membership, and collapsed phased dots on top of the imported multi-orbit Bloch transport stack.

claimPackage the exact 4D Regge action symbol: lattice translates of type-$(1,1)$ and type-$(1,2)$ star cubes, transport offsets on the covering permutations, and phased deficit pairings that collapse the multi-orbit Bloch fold into a continuum-facing quadratic form on strain and wave data in four dimensions.

background

Four-dimensional Regge calculus expands the action to second order on a Freudenthal triangulation of flat space. Edges carry length strains; hinges carry deficit angles. The flat Hessian is assembled orbit-wise under the $S_4$ action on coordinate axes, with six hinge types grouped into four orbits: $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$.

Upstream modules supply the committed pieces. The flat Hessian assembly pairs Heron area covectors with per-orbit star deficit kernels. Orbit covering permutations transport each seed kernel by the first $S_4$ cover sending the orbit representative to the slot's difference masks. Position-resolved star edge origins repair the fold phase for non-$(1,1)$ orbits. The transported all-orbit fold is the continuum-facing consumer of those covers; the factorized all-orbit symbol tracks the $m^2$ moment.

This module sits on that stack and introduces the lattice geometry of star cubes (type $(1,1)$ and $(1,2)$), their membership tests, transport offsets (including the zero-offset identity), and the resolved then collapsed phased deficit dots that turn the symbolic fold into an exact action symbol.

proof idea

Definition and assembly module, not a single theorem proof. It wires imported orbit transport, star-edge origins, hinge kernels, and flat Hessian weights into concrete objects: strain and wave carriers, cube offsets for the $(1,1)$ and $(1,2)$ stars, star-membership predicates, transport offsets, and phased deficit pairings. Resolved dots for the two orbit types are then collapsed into the exact symbol face used downstream. No independent analytic argument lives here beyond packaging and the zero-offset identity.

why it matters in Recognition Science

Supplies the discrete exact-symbol face that continuum-closure modules compare to Einstein-Hilbert. Downstream, the geometric-fold-versus-dictionary module uses it when separating the hinge fold from the banked dictionary and pinning the factor-of-two gap after $\rho=1/2$ normalization. The continuum preflight freezes weak-field EH targets against this symbol. The exact flat-Hessian normalization gate checks honesty of the $-1/8$ per unit Frobenius $m^2$ face versus decoy $-1/4$ scalings. The named closer module for $S_{RS}\to\mathrm{EH}$ in 4D imports it as ledger-facing quadratic input.

In the broader RS gravity campaign this is the exact discrete quadratic before continuum recovery claims, parallel to the 3D TT edge-class packaging but fully multi-orbit and transport-corrected in 4D.

scope and limits

used by (4)

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 (43)