exactFlatCrossTermSlot_smul
plain-language theorem explainer
The exact flat Regge cross-term slot is homogeneous of degree two in the strain matrix: scaling H by c multiplies the slot by c². Gravity analysts assembling the continuum Hessian symbol on the Freudenthal torus cite this when factoring amplitudes out of plane-wave class strains. The proof unfolds the slot definition, splits on the orbit membership guard, and multiplies the two linear factors via the phased-class-dot and deficit-dot scaling lemmas.
Claim. For every real scalar $c$, hinge-orbit type $\mathrm{ty}$, $4\times 4$ real strain matrix $H$, wavevector $m\in\mathbb{R}^4$, and indices $s\in\{0,\ldots,23\}$, $t\in\{0,\ldots,9\}$, the exact flat cross-term slot satisfies $$\mathrm{slot}(\mathrm{ty},\,cH,\,m,\,s,\,t)=c^{2}\,\mathrm{slot}(\mathrm{ty},\,H,\,m,\,s,\,t).$$
background
This module builds the exact flat cross-term continuum symbol for 4D Regge calculus on the Freudenthal torus. At a flat background, hinge deficits vanish, so the Schläfli identity reduces the second variation of the action to the pure cross term $S''=\sum_h (dA_h)(d\delta_h)$. The binding object is that Hessian evaluated on plane-wave class strains with position-resolved deficit phasing.
A slot is the local contribution at one hinge index pair: if $(s,t)$ lies in the given orbit type, it is the product of a phased class-area covector dotted into the strain against a resolved deficit derivative; otherwise it is zero. Mat4 is a $4\times 4$ real matrix (metric/strain perturbation); Wave4 is a 4-component real wavevector. Hinge orbit types (t11, t12, t21, t13, t31) classify lattice hinges under coordinate permutation.
Upstream, phasedClassDot_smul states that the phased class-area pairing is linear in the strain, and exactDeficitDot_smul states that the resolved deficit derivative is likewise linear in $H$. Their product therefore scales by $c^{2}$.
proof idea
Unfold the slot definition. Case-split on the orbit-membership guard isOrbit ty s t.
On the true branch the slot is a product of phasedClassDot and exactDeficitDot. Rewrite by phasedClassDot_smul (linear in $H$) and exactDeficitDot_smul (also linear in $H$), then ring yields the $c^{2}$ factor.
On the false branch both sides are zero; ring closes immediately.
why it matters
Homogeneity of degree two is the structural fact that lets amplitudes factor cleanly out of the discrete Hessian before continuum limits are taken. The immediate parent is exactFlatCrossTermFold_smul, which lifts the same $c^{2}$ law from a single slot to the full orbit-weighted fold by summing over orbit types and hinge indices.
In the module's tiering this is a THEOREM-tagged structural lemma under the MODEL object exactFlatCrossTermFold / finiteExactReggeSymbol. It supports the oracle claim that the true flat Hessian annihilates vertex-gauge modes and sends normalized TT polarizations on axisTTPlus / symbolDir to $-1/4$. It does not itself close the open continuum Tendsto goals (FoldAlongM2Tendsto, geometric ContinuumSymbolIs) or the ledger $S_{RS}$ inhabit questions, but it is the algebraic bookkeeping step those limits rely on when strains are scaled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.