Pith. sign in
module module moderate

IndisputableMonolith.Gravity.Analysis.RecognitionMeshExactJBridge4D

show as:
view Lean formalization →

Bridge layer equating the exact J-cost action on the canonical 4D Recognition Freudenthal mesh with the true Regge quadratic Hessian at zero momentum. Gravity analysts closing weak-field Einstein-Hilbert recovery from discrete data cite the named mesh-action identities. Structure is definitional carriers plus equality lemmas assembled from preflight, Bloch symbols, and exact flat Hessian imports.

claimOn the canonical 4D Recognition Freudenthal mesh, the exact $J$-action on mesh waves equals the true Regge quadratic Hessian at zero momentum. Preflight $4\times 4$ matrix and wave-norm squared identities match the frozen continuum target; mesh side length and wave data are the committed carriers for the torus continuum dictionary.

background

The 4D continuum closure campaign recovers the weak-field Einstein-Hilbert quadratic action from discrete Regge/Recognition data. Upstream preflight freezes the continuum target, canonical mesh carrier, normalized transverse-traceless (TT) data, pure-gauge family, and honesty decoys before any recovery proof. Nothing in preflight proves continuum limits.

Edge TT decomposition supplies the linear-algebra split of symmetric real $4\times 4$ matrices against a nonzero Euclidean wave covector on $\mathrm{Fin},4$. Parallel Bloch modules give the all-orbit factorized and transported folds over the six $S_4$ hinge types, and name the Stage-1 unit-cell exact flat Hessian as a finite trig polynomial (1208 couplings) with centered two-jet Tendsto.

This module sits between those spectral/assembly layers and the torus action$\leftrightarrow$symbol dictionary: it introduces the Recognition Freudenthal mesh, canonical mesh side, mesh waves, mesh true-Regge quadratic Hessian, and the exact $J$-action evaluated on that mesh.

proof idea

Definition-and-bridge module, not a single deep proof. It aliases preflight matrix and wave types to avoid clashes with transported abbrevs, then defines the Recognition Freudenthal mesh carrier, canonical mesh, mesh wave, and exact $J$-action on the mesh.

Identity lemmas equate preflight Frobenius and wave-norm squares to the committed continuum normalizations, and equate the exact mesh $J$-action to the true Regge zero-momentum Hessian. Those equalities specialize imported exact flat Hessian Bloch symbol, torus bridge, midpoint $m^2$ TT identity, and edge TT decomposition facts rather than re-deriving the trig-polynomial or orbit folds.

why it matters in Recognition Science

Feeds the ledger-facing export SRSConvergesEH4D, whose doc states it is the sole place that may later inhabit the preflight Props for weak-field quadratic action recovery (named closers for edge TT decomposition and $S_{RS}\to EH$ in 4D). Without a named mesh-level exact $J$ bridge, the torus continuum limit and Bloch symbol dictionary have no Recognition-native action to match against the frozen EH target.

In the broader RS gravity path this is the 4D analogue of the closed 3D Regge TT assembly$\to$continuum route: discrete $J$-cost on the Freudenthal mesh is the candidate whose quadratic Hessian must reproduce the continuum EH symbol after TT projection. It does not itself flip the ledger; it supplies the mesh-action equalities the closer will cite.

scope and limits

used by (1)

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