finiteTransportedSymbol_eq
plain-language theorem explainer
Definitional identity: the legacy finite-N transported Bloch symbol on a side-(j+3) torus equals the distinct-hinge fold of the real mode k=2πm/N against polarization E. Gravity analysts cite it when routing the preflight binder into algebraic closers. Proof is pure rfl from the definition.
Claim. For every mesh index $j\in\mathbb{N}$, integer mode $m\in\mathbb{Z}^4$, and real $4\times 4$ polarization $E$, the legacy finite transported symbol at $(j,m,E)$ equals the distinct-hinge Bloch fold of $E$ on the real covector $k=2\pi m/N$ with $N=j+3$.
background
Module Regge4DContinuumPreflight freezes the independent continuum target, canonical mesh, TT data, and honesty decoys before any continuum recovery proof. Nothing here claims Tendsto to Einstein-Hilbert; the OPEN continuum binder is the exact flat cross-term symbol, not this legacy fold.
torusSide j := j+3 is the periodic Freudenthal 4-torus side ($N\ge 3$). IntMode4 is an integer wave vector on that torus; realMode N m builds the commensurate covector $k_i=2\pi m_i/N$. Mat4 is a real $4\times 4$ matrix (polarization).
finiteTransportedSymbol is documented as LEGACY: definitionally the distinct-hinge transported Bloch fold blochFoldAllDistinctHinge E (realMode (torusSide j) m). After oracle H_fold it is not the continuum object (mis-transport on t12/t13 gauge) and is retained only for comparison and regression.
proof idea
One-line rfl. The left-hand side is defined to be exactly the right-hand side, so definitional reduction closes the equality with no lemmas or rewriting.
why it matters
Gives a named, stable interface for the legacy distinct-hinge fold so downstream algebraic closers can cite the binder without unfolding the def. The sole recorded consumer is finiteTransportedSymbol_eq_blochFoldAllDistinctHinge in Regge4DTransportedAlgebraicCloser, a thin re-export of this identity.
In the QG full-theory campaign this sits in the preflight tier: THEOREM-tagged bookkeeping and symbol uniqueness, not continuum recovery. Module policy is explicit that the continuum target is finiteExactReggeSymbol (exact flat cross-term fold), while this legacy path and bare blochFoldAll / fitted $2/r$ remain excluded. It does not advance T0-T8 forcing, RCL, or the EH Tendsto Props; it only pins the comparison face so later closers cannot silently redefine the fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.