Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D

show as:
view Lean formalization →

Assembles the transported all-orbit 4D Regge Bloch fold: seed star deficit kernels per S4 hinge orbit, pushforward by covering permutations, and the summed phase-decorated fold over all six hinge types. Gravity analysts cite it when building the finite-momentum Hessian symbol on the Freudenthal 4-torus. Structure is definitional assembly plus transport identities linking orbit seeds to the flat Hessian commitment.

claimFor each S4 hinge orbit type $\mathrm{ty}$ among $\{(1,1),(1,2),(2,1),(1,3),(3,1),(2,2)\}$, fix a seed star deficit kernel and Heron area covector; transport them by the covering coordinate permutation of each hinge slot to obtain slot kernels and covectors; form the phase-decorated Bloch fold of each orbit and sum to the all-orbit fold $F_{\mathrm{all}}(E,k)$ on edge data $E$ at Bloch momentum $k$.

background

In the 4D Regge campaign on the periodic Freudenthal triangulation, the flat second variation of the action is assembled from star deficit kernels and Heron area gradients at triangle hinges. Hinges fall into six combinatorial types under $S_4$ (four orbits once complements are identified). The zero-momentum true-weight assembly lives in the flat Hessian assembly module; the $(1,1)$ orbit already has an exact midpoint plane-wave Bloch fold and its small-momentum $m^2$ symbol.

Orbit transport supplies, for each hinge slot $(s,t)$ of type $\mathrm{ty}$, the first coordinate permutation $p\in\mathrm{Fin},24$ sending the orbit representative to the slot's difference masks. This module commits the per-orbit seed kernels (matching the assembly) and pushes them forward under those permutations, so every orbit reuses the same geometric weights without redefining the stencil or dihedral calculus.

The local setting is finite-momentum Bloch analysis on one Kuhn cell, preparatory to continuum recovery of the Einstein-Hilbert weak-field symbol on the 4-torus.

proof idea

Definition-heavy module. Seed kernels are declared equal to the committed assembly kernels per orbit type. Transport maps apply the covering permutation of each slot to deficit kernels and area covectors (class pushforward on $4\times 4$ matrices). Per-slot terms pair transported deficit against transported area with the midpoint phase factor; orbit folds sum slots; the all-orbit fold sums the six types. Equalities such as seed-kernel-equals-assembly are short rewriting lemmas. No independent analytic closed form is proved here; the content is the transported assembly interface.

why it matters in Recognition Science

This is the all-orbit finite-momentum carrier that later continuum and Recognition-bridge modules import. Downstream, the exact action symbol and torus continuum limit treat the transported fold as the geometric Hessian input (with the caveat that a distinct-hinge variant can leave gauge residue and is not the continuum object). The Recognition mesh exact-$J$ bridge attaches a value-level action whose amplitude Hessian is the Option-C midpoint Bloch symbol on the same torus family. Tensor algebraic closer and flat second-variation status modules consume the transported $m^2$ and fold data when elevating Schläfli-reduced edge Hessians and banking TT quadratic forms. In the broader RS gravity stack it sits between hinge star kernels / flat assembly and the 4D continuum preflight target (weak-field EH, pure gauge, honesty decoys).

scope and limits

used by (11)

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

depends on (9)

Lean names referenced from this declaration's body.

declarations in this module (65)