finiteTransportedSymbol_zero
plain-language theorem explainer
The finite transported continuum symbol vanishes on the zero polarization for every torus side and integer mode. Gravity analysts banking 4D Regge Bloch fold identities cite this as the zero case of quadratic homogeneity. Proof is a one-line specialization of the scalar-multiplication identity at coefficient zero.
Claim. For every $j \in \mathbb{N}$ and integer mode $m \in \mathbb{Z}^4$, the finite transported symbol at resolution $j$ and mode $m$ evaluates to zero on the zero $4\times 4$ matrix: $S_j(m,0)=0$.
background
In the transported 4D algebraic-closer module, the concrete continuum sequence is the finite-$N$ distinct-hinge Bloch fold on the torus family. For side index $j$, integer mode $m$, and polarization $E$, the finite transported symbol is defined as the all-distinct-hinge fold of $E$ against the real wave covector $k=2\pi m/N$ on the side-$N$ torus.
The module banks algebraic identities for this sequence without claiming Einstein–Hilbert Tendsto of the normalized fold to $-1/4$ on Frobenius TT, and without inhabiting the continuum EH convergence Prop. Integer modes are maps $\mathrm{Fin},4\to\mathbb{Z}$ (commensurate torus modes).
Upstream, quadratic homogeneity is already proved: scaling the polarization by $c\in\mathbb{R}$ multiplies the symbol by $c^2$. The zero-polarization case is the $c=0$ corner of that identity.
proof idea
One-line specialization of the scalar-multiplication theorem. Instantiate that identity at coefficient $c=0$ and polarization equal to the unit matrix in $\mathrm{Mat}_4$; then $0\bullet I=0$ and $0^2=0$, so the symbol on the zero matrix is zero. simpa closes the equality.
why it matters
Closes the zero case of quadratic homogeneity for the concrete continuum sequence that the module equates with the distinct-hinge multi-orbit fold. The module doc lists quadratic homogeneity of the finite transported symbol among the banked theorems, alongside limit uniqueness, orbit-sum decomposition, and the $(1,1)$-orbit $m^2$ Tendsto witnesses (axis TT to $-3$, decoy gauge to $0$).
No downstream consumers are wired yet; the result is local scaffolding for later continuum-symbol algebra. It does not touch the open EH target (Tendsto to $-1/4$ on Frobenius TT) or the gauge-zero target, and it does not flip gap-action recovery. Expected axiom footprint stays the standard classical trio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.