phasedDeficitDotCollapsed
plain-language theorem explainer
Defines the collapsed (legacy) deficit-side contraction for the exact flat Regge cross-term: a single full-star kernel dotted against plane-wave class strains, indexed by hinge orbit type, strain matrix, wave and position, and slot/tetrahedron indices. Gravity analysts cite it as the fallback when cube-offset tables are unavailable. The body is a one-line wrapper around the phased class dot with the transported slot-orbit deficit kernel.
Claim. For a hinge orbit type $\mathrm{ty}$, a $4\times 4$ real strain matrix $H$, wave and position vectors $m,x\in\mathbb{R}^4$, slot index $s\in\{0,\ldots,23\}$ and tetrahedron index $t\in\{0,\ldots,9\}$, the collapsed deficit contraction is the real number obtained by pairing the transported slot-orbit deficit kernel of $(\mathrm{ty},s,t)$ with the plane-wave class perturbation of $H$ at $(m,x)$.
background
This module builds the exact flat cross-term continuum symbol for the 4D Regge action Hessian on the Freudenthal torus. At flat background, deficits vanish, so Schläfli reduces the second variation to $S''=\sum_h (dA_h)(d\delta_h)$. The binding objects keep position-resolved deficit phasing: type-$(1,1)$ orbits use star-member cube offsets; other orbits use per-edge transported origins.
Mat4 is a $4\times 4$ real matrix (class strain); Wave4 is a map $\mathrm{Fin},4\to\mathbb{R}$ (Bloch wave / lattice position). HingeOrbitType enumerates the six lattice orbits under coordinate permutation ($t11,t12,t21,t13,t31,\ldots$). Upstream, slotOrbitDeficitKer pushes the assembly deficit covector through the orbit covering permutation, and phasedClassDot contracts a 15-component class vector against plane-wave class perturbations of $H$.
The doc-comment marks this definition as the collapsed legacy path: one hinge base for the full-star kernel, used only when cube-offset tables are missing in Lean.
proof idea
Pure definitional wrapper. The body applies phasedClassDot to the 15-vector slotOrbitDeficitKer ty s t and the strain/wave data $(H,m,x)$. No tactics, no algebraic reduction beyond that single application. Homogeneity in $H$ is proved downstream by unfolding and rewriting with phasedClassDot_smul.
why it matters
Supplies the deficit half of the exact flat cross-term slot when the preferred position-resolved paths (phasedDeficitDotResolvedT11 / T12) are not available. The immediate consumer is the private homogeneity lemma phasedDeficitDotCollapsed_smul, which feeds structural bookkeeping (scalar homogeneity of the fold) in the same module.
In the broader RS gravity stack this sits under the MODEL tier objects exactFlatCrossTermFold / finiteExactReggeSymbol: geometry-derived flat cross-terms, not yet Schläfli-elevated from the nonlinear action for every orbit. It does not close the open continuum questions (FoldAlongM2Tendsto, ledger $S_{RS}$, e0 isotropy). Oracle target remains $H_{\mathrm{fold}}$ sending normalized TT on axisTTPlus/symbolDir to $-1/4$ while annihilating vertex-gauge modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.