TorusC2DensityExtensionOpen
plain-language theorem explainer
Names the open continuum-limit obligation on the 4D torus Regge mesh: every nonzero integer mode with a Frobenius-normalized TT polarization admits some finite limit of the normalized midpoint Bloch symbol as mesh side tends to infinity. Analysts closing the 4D action–symbol dictionary would cite this proposition. It is a bare Prop definition (the quantified statement itself), not a proved theorem.
Claim. For every nonzero integer wave mode $m\in\mathbb{Z}^4$ and every $4\times 4$ matrix $E$ that is a continuum transverse-traceless polarization of the real covector of $m$ with Frobenius norm one, there exists $\Lambda\in\mathbb{R}$ such that the normalized Option-C midpoint Bloch mesh symbol of $(m,E)$ tends to $\Lambda$ as the torus side length tends to infinity.
background
The module treats the 4D torus continuum limit of a finite periodic Freudenthal action sequence on side $N=j+3$, with $N^4$ sites and density weight $N^{-4}$ (frozen against the wrong-power decoy). The target bookkeeping is the 4D analogue of the closed 3D cancellation: $(2/N^4)\cdot(N^4/2)=1$, so the canonical finite Hamiltonian matches the distinct-hinge Bloch fold once Schläfli elevation and the 4D cell-sum identity are closed.
An integer mode is a commensurate wave vector $\mathrm{Fin},4\to\mathbb{Z}$ on the side-$N$ torus; the associated real covector is $k=2\pi m/N$. Continuum TT polarization means algebraic transverse-traceless conditions plus Frobenius normalization to one (without the pin a fixed continuum coefficient is ill-posed). The normalized torus Tendsto packages convergence, along the mesh family at infinity, of the Option-C midpoint Bloch symbol divided by momentum-norm squared, matching the continuum symbol target used elsewhere in the preflight.
proof idea
No proof body: the declaration is a def of a Prop whose right-hand side is the open statement. It quantifies over nonzero integer modes and TT-normalized polarizations and asserts existence of a real continuum value for the normalized midpoint Bloch Tendsto. Per the doc-comment it is deliberately an equality-style obligation, not a : True shell. Discharging it is future work: a C²/smooth density extension from finite Fourier sums that makes the normalized mesh sequence converge.
why it matters
Module status flags this as OPEN (named, non-tautological): C²/smooth density extension from finite Fourier sums, needed for the continuum Tendsto side of the 4D action↔symbol dictionary. The parallel 3D path (Bloch assembly to continuum limit) is already closed; here the algebraic density-weight identities and decoy discrimination are theorems, while this Prop stands for the analytic extension step. Closing it would let the surviving dictionary factor equal 1 bind to an actual limit value for every nonzero TT mode. It does not flip gap_action_recovery. No downstream users yet; it is the named target rather than a lemma already in a forcing chain (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.