finiteTransportedSymbolSequence
plain-language theorem explainer
Packages the legacy distinct-hinge transported Bloch fold into a side-indexed sequence of real symbols for a fixed integer mode and polarization matrix. Gravity analysts cite it only for regression against the frozen continuum binder. The body is the pointwise map sending mesh index j to the finite-N fold on torus side j+3.
Claim. For an integer wave mode $m\in\mathbb{Z}^4$ and a real $4\times 4$ polarization $E$, the legacy transported-symbol sequence is the map $j\mapsto S^{\mathrm{leg}}_j(m,E)\in\mathbb{R}$, where each value is the distinct-hinge Bloch fold of $E$ at the real wave covector $k=2\pi m/N$ on the periodic 4-torus of side $N=j+3$. This is a named $\mathbb{N}\to\mathbb{R}$ family, not the continuum exact-action binder.
background
This module is the first binding increment of the 4D Regge continuum closure plan. It freezes the independent weak-field Einstein-Hilbert quadratic target, the canonical periodic Freudenthal 4-torus mesh of side $N\ge 3$, normalized TT data, pure-gauge families, and honesty decoys before any continuum recovery claim. Nothing in the module proves continuum Tendsto statements.
FiniteSymbolSequence is simply $\mathbb{N}\to\mathbb{R}$: a named family of finite-$N$ symbol values. The continuum Prop is required to use a concrete exact-action sequence, not an arbitrary inhabitant. The side length is $N=j+3$ via torusSide, so the family starts at $N=3$. Integer modes IntMode4 are commensurate wave vectors $m:\mathrm{Fin},4\to\mathbb{Z}$; the real covector is $k=2\pi m/N$. Polarizations are real $4\times 4$ matrices.
The pointwise values come from the legacy finite-$N$ distinct-hinge transported Bloch fold, definitionally the all-distinct-hinge fold of $E$ at that real mode. After oracle H_fold, that fold is retained only for comparison: it mis-transports on $t_{12}/t_{13}$ gauge and is explicitly not the continuum object.
proof idea
Definitional one-liner: the sequence is the function $j\mapsto$ the legacy finite transported symbol at index $j$, mode $m$, and matrix $E$. No lemmas or tactics; pure eta-expansion of the pointwise legacy fold over the continuum-family index.
why it matters
In the preflight contract the continuum target is the exact flat cross-term symbol (from the exact-action fold), $|k|^2$-normalized, matching the independently frozen EH coefficient on TT and vanishing on pure gauge. The legacy distinct-hinge transported fold and this sequence wrapper are kept only as regression decoys so later algebraic closers cannot silently swap binders.
Module OPEN items remain: continuum Tendsto Props for EH recovery and gauge-zero are uninhabited; gap-action recovery is false. This definition does not feed those Props. With no recorded downstream uses, it is archival scaffolding inside the gravity analysis stack, marking what must not be mistaken for the continuum symbol in the QG full-theory campaign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.