exactFlatCrossTermFold
plain-language theorem explainer
Local alias of the distinct-hinge weighted exact flat cross-term fold: a real-valued quadratic form on a 4×4 strain matrix and a 4-wavevector. Gravity analysts cite it as the continuum-facing Hessian candidate after the fold map. The body is a one-line re-export of the exact-action symbol definition.
Claim. For a $4\times 4$ real matrix $H$ and wavevector $m\in\mathbb{R}^4$, the exact flat cross-term fold is $\sum_{\mathrm{ty}} (\mathrm{orbitStarSize}(\mathrm{ty}))^{-1}\, C_{\mathrm{ty}}(H,m)$, the orbit-size-weighted sum of exact flat cross-terms over distinct hinge orbit types.
background
This module is the ledger-facing export for the weak-field quadratic action recovery campaign in 4D Regge gravity. It only hosts named closers for edge TT decomposition and $S_{\mathrm{RS}}\to\mathrm{EH}$ convergence; the Props stay uninhabited until both gates close under audit.
The underlying object lives in the exact-action symbol layer. There the fold is defined as a sum over hinge orbit types of the exact flat cross-term on each orbit, weighted by the reciprocal star size of the orbit. Upstream doc calls it the continuum-facing Hessian candidate after the fold map $H_{\mathrm{fold}}$.
Matrices are $4\times 4$ strain data; waves are $\mathbb{R}^4$ modes. Continuum preflight rebinds the same name and proves the finite exact Regge symbol equals this fold evaluated at the real mode of the torus side.
proof idea
Pure abbreviation: one-line alias of Regge4DExactActionSymbol.exactFlatCrossTermFold. No tactics, no lemmas, no computation. The mathematical content is entirely in the target definition (orbit-weighted sum of exact flat cross-term orbits).
why it matters
Gives the SRS-converges-EH export module a stable local name for the continuum Hessian face used throughout the 4D Regge symbol pipeline. Downstream, continuum preflight equates the finite exact Regge symbol to this fold at the torus real mode (definitional equality). The exact-action layer uses it to build the bare continuum symbol sequence, prove quadratic scaling under scalar multiplication, and mark the fold as retained legacy structure.
In the broader campaign it sits under the weak-field quadratic recovery path toward $S_{\mathrm{RS}}\to\mathrm{EH}$ in 4D. Module scope is explicit: not sourced Einstein, not full nonlinear wick continuation, and gap action recovery flips only when both named closers are inhabited with focused audits. Geometric residual bookkeeping also references the export surface that carries this name.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.