recognitionMeshExactJBridge4DStatus
plain-language theorem explainer
Status record for the 4D Recognition-mesh exact-J bridge on the periodic Freudenthal torus. It marks the mesh carrier as defined, closes the amplitude Hessian and iterated Einstein-Hilbert continuum faces, records exact-J equal to the true-Regge Hessian by model identification, leaves gap-action recovery unclaimed, and keeps Schläfli elevation open. Downstream flag lemmas cite it by `decide`. Pure structure inhabitant, no proof work.
Claim. The status bundle for the 4D Recognition-mesh exact-$J$ bridge asserts: mesh carrier defined; amplitude Hessian closed (equals the mesh true-Regge Hessian); iterated Einstein-Hilbert Tendsto closed at the scale-explicit Option-C face; exact-$J$ equals true Regge Hessian closed by model identification; gap-action recovery not claimed; Schläfli elevation of the model action still open.
background
This module is the Recognition gate of the 4D continuum-closure campaign. It builds a canonical Recognition 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.
Preferred limit shape is amplitude Hessian at fixed mesh, then $N\to\infty$. The model identification sets the exact-$J$ action on the mesh equal to the exact midpoint Bloch symbol on edge classes at amplitude $\varepsilon$. Elevating that Hessian to the literal nonlinear Regge action via Schläfli is deliberately left open. Arbitrary test-variation pullbacks are excluded by the preflight decoy.
The status structure packages six Boolean honesty flags: carrier defined, amplitude-Hessian open, iterated-EH open, equals-true-Regge open, gap-action recovery, and Schläfli-elevation open. Doc-comments on the structure mark the first four continuum faces as closed and Schläfli as the remaining honesty gap.
proof idea
Definitional inhabitant of the status structure. Each field is a literal Boolean: carrier true; amplitude Hessian, iterated EH, equals-true-Regge, and gap-action-recovery all false (closed or unclaimed); Schläfli elevation true (still open). No tactics, no lemmas, no computation beyond structure construction.
why it matters
Ledger entry for the Recognition half of the 4D continuum bridge. Downstream, recognitionMeshExactJBridge4DStatus_flags reifies all six bits as a single conjunction, and recognition_iterated_eh_closed records that iterated EH is closed without flipping gap-action recovery. Module theorems already close amplitude Hessian equals mesh true-Regge Hessian and the iterated $N\to\infty$ Tendsto at the scale-explicit Option-C face by composing the discrete torus bridge with exact midpoint $m^2$ TT and gauge faces. The record does not inhabit full $S_{\mathrm{RS}}\to\mathrm{EH}$ convergence in 4D and does not claim Schläfli elevation of the model action to nonlinear Regge. In the broader RS gravity stack this is bookkeeping for the Option-C midpoint Bloch route, not a new dynamical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.