finiteTransportedSymbol
plain-language theorem explainer
Legacy finite-N distinct-hinge transported Bloch fold of a 4×4 polarization against a commensurate torus mode. Gravity continuum-limit authors cite it only for regression against the exact-action continuum symbol; after the H_fold oracle it is not the continuum binder (mis-transport on t12/t13 gauge). One-line definitional wrapper of the distinct-hinge orbit fold at k = 2π m / N with N = j+3.
Claim. For mesh index $j\in\mathbb{N}$, integer mode $m\in\mathbb{Z}^4$, and polarization $E\in M_4(\mathbb{R})$, set $N=j+3$ and $k_i=2\pi m_i/N$. The finite transported symbol is the distinct-hinge Bloch fold of $E$ at covector $k$: $\sum_{\tau} r_\tau^{-1}\,\mathrm{blochFoldOrbit}_\tau(E,k)$.
background
Module freezes the independent continuum EH target, canonical Freudenthal 4-torus mesh, normalized TT data, and honesty decoys before any continuum recovery proof. Nothing here proves Tendsto to Einstein-Hilbert.
Side length is $N=j+3$ (so $N\ge 3$). An integer mode $m:\mathrm{Fin},4\to\mathbb{Z}$ becomes the real wave covector $k=2\pi m/N$. Polarizations are real $4\times 4$ matrices. The upstream distinct-hinge fold sums over hinge orbit types with weight $1/r_\tau$ times the orbit Bloch fold: true hinge sum wants distinct hinges with full-star deficit, not bare blochFoldAll and not a fitted $2/r$.
After oracle H_fold the continuum object is the exact flat cross-term symbol (normalized by $|k|^2$), equal to the EH coefficient on TT and zero on pure gauge. This legacy fold is retained only for comparison.
proof idea
Definitional one-liner: expand to the distinct-hinge Bloch fold of polarization $E$ evaluated at the real mode on side $N=j+3$. No tactics; the companion equality theorem is rfl.
why it matters
Named mesh-side entry point for the legacy transported fold inside the 4D continuum preflight and torus-limit stack. Downstream equalities identify it with the canonical finite Hessian, the finite torus Hessian, and several algebraic closer aliases (orbit sum, blochFoldAllDistinctHinge). The sequence form packages it as a FiniteSymbolSequence for regression.
Module doc is explicit: after H_fold this is not the continuum binder (mis-transport on t12/t13 gauge). Continuum recovery, gauge-zero Tendsto, and $S_{RS}\to\mathrm{EH}$ remain OPEN; the frozen EH quadratic is independent of lattice weights. Landmark context is the QG full-theory 4D continuum closure plan, not the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.