RecognitionFreudenthalMesh4D
plain-language theorem explainer
Recognition-native mesh carrier for a continuum index j, with lattice side N = j+3 on the periodic Freudenthal 4-torus. Gravity continuum-closure work cites it as the typed mesh for the Recognition gate. The structure holds only the index; side length and the underlying torus carrier are definitional projections.
Claim. A Recognition Freudenthal mesh in four dimensions is data consisting of a continuum index $j \in \mathbb{N}$. Its lattice side length is $N = j+3$, and it determines the canonical periodic Freudenthal triangulation of the flat 4-torus with the same index.
background
This module is the Recognition gate of the 4D continuum-closure campaign: it builds a mesh carrier on the periodic Freudenthal 4-torus and attaches a value-level exact-J action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol on that torus family.
Upstream, CanonicalFreudenthalTorus4D is the same one-field continuum-index carrier for the side-$N$ periodic Freudenthal triangulation of the flat 4-torus; concrete Kuhn cell data live in star/orbit modules. The side map is torusSide j := j + 3, so the continuum family never uses degenerate small lattices.
The Recognition mesh is the Recognition-native twin of that torus carrier: same index, same side, with an explicit conversion into the preflight torus type so later exact-J and Hessian constructions can sit on a single typed mesh.
proof idea
Definitional structure, not a proved claim. One field: continuum index. Side length is torusSide of that index. Conversion to the canonical Freudenthal torus is the same index wrapped as a torus. Equality of side with the torus side is rfl.
why it matters
This is the typed mesh every Recognition-gate construction in the module consumes. Downstream, the canonical family is just the index wrapper; the exact-J action on the mesh is defined as half epsilon-squared times the mesh true-Regge quadratic Hessian; amplitude-Hessian existence and equality with that mesh Hessian are stated on this carrier; second-difference and Hessian-bridge lemmas take it as the first argument.
In the framework it is the discrete geometry side of the exact-J to Option-C midpoint Bloch bridge at value level. Preferred limit shape is amplitude Hessian at fixed mesh, then N to infinity. Binding honesty from the module: Schläfli elevation of the Hessian to the full nonlinear Regge action remains open; the module does not flip gap action recovery or inhabit the full RS-to-EH 4D convergence statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.