edge_tt_decomposition
plain-language theorem explainer
Local alias for the packaged edge transverse-traceless decomposition proposition used by the weak-field SRS-to-Einstein-Hilbert ledger. Gravity analysts cite it when wiring the algebraic TT split of the true-weight Regge Hessian into the continuum preflight. The body is a one-line re-export of the preflight Prop name after multi-module opens.
Claim. The proposition that every symmetric $4\times 4$ matrix $H$ at nonzero wavevector $m$ splits as $H = H^{\mathrm{TT}} + \mathrm{gauge}(m,H) + \mathrm{trace\, residual}\cdot P_\perp(m)$, with $H^{\mathrm{TT}}$ transverse-traceless at $m$, together with the packaged independent TT polarizations and gauge/trace annihilation clauses attached to all fifteen Regge edge classes of the true-weight Hessian.
background
In the weak-field Regge analysis, the continuum limit of the discrete quadratic action is controlled by the true-weight Hessian on edge lengths. That Hessian must be split into a transverse-traceless (TT) radiative piece, a pure-gauge piece, and a residual trace piece along the transverse projector. The preflight packages this split, plus two independent TT polarizations and gauge/trace annihilation on all fifteen edge classes, as a single named Prop.
This module is the ledger-facing export for quadratic action recovery of the Einstein-Hilbert term in 4D. After opening several analysis modules that share short names, local abbreviations disambiguate Mat4, Wave4, and the edge TT Prop so downstream ledger closers refer to one stable name.
Upstream, the preflight defines the Prop; the algebraic closer module supplies the theorem that inhabits it by refining the four conjuncts (decomposition identity, TT projection, polarizations, annihilation).
proof idea
One-line abbreviation: the local name is definitionally equal to Regge4DContinuumPreflight.edge_tt_decomposition. No proof obligations are discharged here; the inhabitant lives in the EdgeTTDecompositionCloser4D theorem of the same name, which refines the four packaged conjuncts and reduces wave-norm nonvanishing to momentum-square nonvanishing.
why it matters
This alias is the stable ledger handle for the edge TT closer inside the SRS-converges-to-EH campaign. Downstream it is consumed by edge_tt_decomposition_closed, the audit package, Lorentzian TT projection lemmas, and the dual-gate requirement that both named closers be inhabited before gap_action_recovery may flip.
In Recognition Science gravity, recovering the Einstein-Hilbert quadratic action from the recognition mesh is the continuum bridge for the weak-field sector. The module scope is deliberately narrow: weak-field quadratic convergence only, not sourced Einstein equations, horizons, or full nonlinear wick continuation. Banking this named Prop (and its closed inhabitant) is a required ledger step on that path; it does not by itself claim continuum Ricci or arbitrary-curvature GR.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.