BlochM2Symbol4DStatus
plain-language theorem explainer
Status record for the (1,1)-orbit small-momentum (m²) symbol of the 4D Regge Bloch fold. Eight boolean flags mark which subclaims are closed: evenness, axis/gauge m² coefficients, axis nonvacuity, axis/gauge Tendsto, full Hessian symbol, EH4d convergence, and gap-action recovery. Gravity analysts cite it as the honest ledger of what the module has proved. It is a pure structure definition; the companion value fills the closed flags.
Claim. A record type with eight boolean fields tracking closure of the (1,1)-orbit $m^2$-symbol analysis for the 4D Bloch fold along the direction $(1,1,0,0)$: evenness of the folded cost; closed-form $m^2$ coefficient on the TT axis and on the decoy gauge mode; nonvacuity of the axis; punctured Tendsto of $\mathrm{fold}/\mu^2$ on axis and gauge; full Hessian symbol; convergence of the RS action to the Einstein–Hilbert 4d action; and gap-action recovery.
background
The module studies the (1,1)-orbit contribution to the small-momentum symbol of blochFold11, imported from the 4D Regge Bloch fold analysis. It never redefines Hessians, kernels, or stencils. The fold along a momentum scale is $\mathrm{foldAlong},H,\mu := \mathrm{blochFold11},H,(\mu\cdot(1,1,0,0))$, with $H$ the shifted recognition cost $H(x)=J(x)+1=\frac12(x+x^{-1})$, under which the Recognition Composition Law becomes the d'Alembert identity $H(xy)+H(x/y)=2H(x)H(y)$.
Landed facts along that ray: the fold is even (so the first derivative at zero vanishes when differentiable); it vanishes at zero on the TT-plus axis and on the decoy gauge mode; and the closed-form $m^2$ coefficient equals $-3$ (TT, nonzero) and $0$ (gauge). The punctured Tendsto glue $\mathrm{foldAlong},H,\mu/\mu^2\to m^2\mathrm{Symbol},H$ is closed on axis/gauge in a sibling module and remains open for general $H$.
Upstream ledger-closure predicates on plaquettes and glued dominos supply the discrete parity language in which the fold is built; they are not re-proved here.
proof idea
No proof body: this is a structure declaration. Each field is a bare Bool flag. The companion value blochM2Symbol4DStatus assigns true to evenness, both $m^2$ coefficients, axis nonvacuity, and axis/gauge Tendsto, leaving fullHessianSymbol, convergesEH4d, and gapActionRecovery unset in the supplied snippet (defaults or explicit false at the use site). Doc-comment on the Tendsto flag points to the sibling Tendsto module for the axis/gauge case and marks general $H$ as open.
why it matters
This is the module's honest progress board for the (1,1) contribution to the 4D Bloch $m^2$ symbol. Downstream, blochM2Symbol4DStatus is the single inhabited instance that records which pieces have closed theorems. Module scope is explicit: it does not claim the full Hessian symbol, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4d, and does not flip gap-action recovery. Those three flags stay false until separate work lands.
In the Recognition gravity stack this sits under the discrete-to-continuum bridge: the eight-tick / plaquette ledger (pixel closure) feeds Regge-type folds whose small-momentum quadratic symbol must match the continuum graviton kinetic term. Closing evenness and the TT coefficient $-3$ is the local evidence that the (1,1) orbit is nondegenerate and gauge-clean; the open Tendsto-for-general-$H$ and full-symbol flags mark the remaining analytic gap before an EH4d convergence theorem can be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.