canonicalRecognitionMesh
plain-language theorem explainer
Packages each continuum index j as the canonical Recognition-native Freudenthal 4-torus mesh carrier (side j+3). Gravity continuum-closure proofs cite it as the fixed mesh on which exact-J amplitude Hessians and true-weight Regge Hessians are compared. The body is the one-field structure constructor.
Claim. For each natural number $j$, the canonical Recognition mesh is the Recognition-native Freudenthal 4-torus mesh whose continuum index equals $j$ (equivalently, torus side length $j+3$).
background
This module is the Recognition gate of the 4D continuum-closure campaign: it builds a canonical mesh carrier on the periodic Freudenthal 4-torus and attaches a value-level action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol on that torus family.
RecognitionFreudenthalMesh4D is the thin carrier: a single continuum index $j$, with side length defined as the torus side of that index (namely $j+3$) and a forgetful map to the canonical Freudenthal 4-torus. The exact flat cross-term Hessian on this carrier is the concrete edge-class geometry used downstream.
Preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$. The module treats the exact-J action as the midpoint Bloch symbol at amplitude $\varepsilon$ (MODEL identification); elevating that Hessian to the literal nonlinear Regge action via Schläfli remains open.
proof idea
Definitional one-liner: the structure RecognitionFreudenthalMesh4D has a single field continuumIndex, so the canonical mesh at $j$ is the anonymous constructor $\langle j\rangle$. No lemmas or tactics.
why it matters
This is the mesh family every Recognition-gate statement quantifies over. Downstream, canonicalRecognitionMesh_side records side $= j+3$ by rfl. ExactJEqualsTrueReggeHessian and its proof exactJEqualsTrueReggeHessian_holds identify the exact-J amplitude Hessian with the mesh true-Regge quadratic Hessian on canonicalRecognitionMesh j by construction.
The iterated continuum target RecognitionExactJConvergesEH (closed by recognitionExactJConvergesEH_closed, and via the normalized-mesh reduction) takes amplitude Hessians on this family then sends side $N\to\infty$ to the scale-explicit Option-C EH face. Gauge-zero variants use the same carrier. In the broader RS gravity stack this is the discrete mesh step before continuum EH recovery; it does not flip gap_action_recovery or inhabit S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.