exactFlatCrossTermFold_smul
plain-language theorem explainer
The exact flat cross-term fold is homogeneous of degree two in the strain matrix: scaling H by a real factor c multiplies the fold by c². Anyone assembling continuum symbols or checking that the discrete Hessian is a quadratic form cites this. The proof unfolds the orbit sum, applies the slot-level smul lemma, and pulls c² through the finite sums.
Claim. For every real scalar $c$, every $4\times 4$ real matrix $H$, and every wave vector $m\in\mathbb{R}^4$, the distinct-hinge weighted exact flat cross-term fold satisfies $\mathrm{Fold}(cH,m)=c^{2}\,\mathrm{Fold}(H,m)$.
background
This module builds the continuum-facing Hessian candidate for 4D Regge calculus on the Freudenthal torus after the oracle verdict $H_{\mathrm{fold}}$. At flat background, deficits vanish, so Schläfli reduces the second variation to the cross term $S''=\sum_h(dA_h)(d\delta_h)$. The fold averages that cross term over hinge orbit types, each weighted by the reciprocal of the orbit star size.
A slot is one (star-member, triangle) contribution: area covector dotted into the class strain, times a position-resolved deficit phasing. Orbit sums run over 24 star members and 10 triangles; the fold then weights by orbit type. Matrices are plain $4\times 4$ reals; waves are $\mathbb{R}^4$ momenta.
The slot-level identity already records that each nonzero slot scales as $c^{2}$ when $H\mapsto cH$, because both the area factor and the deficit factor are linear in $H$. The fold is the weighted sum of those slots.
proof idea
Unfold the fold into a sum over hinge orbit types of $(\mathrm{orbitStarSize},ty)^{-1}$ times the orbit double sum, then unfold each orbit into slots. Rewrite every slot via the slot smul lemma, replacing each summand by $c^{2}$ times the unscaled slot.
For each orbit type, a short local identity pulls $c^{2}$ out of the double sum: Finset.mul_sum followed by ring_nf moves the scalar past the inverse star-size weight. Reassemble with another simp_rw and ← Finset.mul_sum to obtain the global $c^{2}$ factor outside the fold.
why it matters
Quadratic homogeneity is the structural signature that the flat cross-term fold is a true Hessian symbol, not a gauge-contaminated linear residue. Downstream, finiteExactReggeSymbol_smul is a one-line application: the continuum-family symbol at side $N=j+3$ inherits $c^{2}$ scaling by specializing the wave to the family real mode.
In the module's tier tags this sits under THEOREM (structural lemmas: homogeneity, zero-momentum drop, status flags). It supports the MODEL object exactFlatCrossTermFold / finiteExactReggeSymbol that the preflight continuum symbol is meant to match. Open items it does not close remain FoldAlongM2Tendsto, full geometric ContinuumSymbolIs for all modes, and ledger $S_{RS}$ inhabit; those need analytic limits, not algebraic scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.