edge_tt_decomposition_holds
plain-language theorem explainer
The named preflight proposition for edgewise transverse-traceless (TT) decomposition of the true-weight Hessian holds in four-dimensional Regge calculus. Continuum-limit and discrete-gravity workers cite it when discharging the algebraic-plus-attachment ledger gate before Einstein-Hilbert recovery. The proof is a one-line term that re-exports the sibling constructive closer.
Claim. The packaged continuum-preflight proposition holds: for every nonzero four-wave $m$ and every symmetric $4\times 4$ Hessian $H$, one has the algebraic split $H = \mathrm{TT}(m,H) + \mathrm{gauge}(m,H) + \mathrm{trace\,residual}(m,H)\,P_\perp(m)$ with $\mathrm{TT}(m,H)$ transverse-traceless, together with Frobenius-normalized plus/cross TT witnesses, a pure-gauge non-transverse decoy, and plane-wave attachment on all fifteen Regge edge classes.
background
In the four-dimensional Regge continuum preflight, the true-weight Hessian of the discrete action is a symmetric $4\times 4$ matrix $H$ on wave covectors $m$. The preflight packages a single named proposition requiring an algebraic transverse-traceless split of every such $H$ at nonzero wave norm, two independent Frobenius-normalized TT polarizations (plus and cross), annihilation of pure-gauge and trace decoys, and attachment of that split to all fifteen Regge edge classes via the already-proved plane-wave edge stencil.
The module is the named closer for that proposition. It sits strictly at the ledger algebraic-plus-attachment layer: multi-orbit true-weight continuum recovery is deferred to the separate gate $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$. Upstream, the constructive sibling builds the four conjuncts by refining an existential package and invoking the edge-attachment theorems from the Regge edge TT attachment development.
proof idea
One-line term proof. The declaration simply applies the sibling constructive theorem edge_tt_decomposition in the same module, which already inhabits the preflight proposition by refining a four-conjunct package (algebraic TT split for every nonzero wave and symmetric Hessian, plus/cross Frobenius witnesses, pure-gauge non-transverse decoy, and plane-wave edge attachment). No extra tactics or rewriting occur here.
why it matters
Recognition Science gravity recovers continuum Einstein-Hilbert dynamics from a discrete recognition ledger. This declaration seals the named edge-TT decomposition closer required by the four-dimensional continuum preflight, so downstream continuum-limit arguments can treat the algebraic TT split, gauge/trace annihilation, and edge attachment as discharged facts rather than open obligations.
The module doc is explicit that full multi-orbit true-weight continuum recovery remains the $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ gate; this closer only finishes the algebraic-plus-attachment layer. No further used-by edges are recorded yet, so its immediate role is to provide a stable, citable name for that preflight Prop inside the gravity analysis stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.