m2SlotCertZ
plain-language theorem explainer
Integer per-slot certificate for the (1,1)-orbit contribution to the small-momentum m² symbol of the 4D Regge Bloch fold. On T11 hinges it is minus the product of the integer area pairing and the squared-phase kernel weight; elsewhere it is zero. Downstream closed-form m² evaluations on TT and gauge modes cite it via the real coefficient identity. The body is a single conditional product of two integer slot sums.
Claim. Given integer class coefficients $c_z:\{0,\ldots,14\}\to\mathbb{Z}$, a star index $s\in\{0,\ldots,23\}$, and a triangle index $t\in\{0,\ldots,9\}$, the certified $m^2$ slot value equals $-A_0(c_z,s,t)\,K''(c_z,s,t)$ when $(s,t)$ is a $(1,1)$-orbit hinge, and equals $0$ otherwise. Here $A_0$ is the integer area-covector pairing and $K''$ is the integer squared-phase kernel weight along the slot transport.
background
The module isolates the $(1,1)$-orbit piece of the small-momentum symbol of blochFold11 in 4D Regge calculus. Along the momentum ray $\mu\cdot(1,1,0,0)$, one studies the even fold $\mu\mapsto\mathrm{blochFold}_{11}(H,\mu\cdot v)$ and its putative quadratic coefficient $m^2(H)$. Only hinge pairs of orbit type T11 contribute; the predicate isT11 is the decidable equality of the hinge orbit classifier with that type.
Two integer slot functionals feed the certificate. The area pairing $A_0(c_z,s,t)$ is the sum over the fifteen edge classes of the integer area-covariance stencil times $c_z$. The kernel weight $K''(c_z,s,t)$ sums, over classes, the $(1,1)$-kernel sign times the transported coefficient times the square of the integer phase index along the slot transport permutation. Both are pure $\mathbb{Z}$-valued, so the product is an exact certificate before any real cast.
The local setting is deliberately narrow: Hessian, kernels, and stencil are imported from the fold module and never redefined; the full Einstein-Hilbert recovery and gap-action statements remain out of scope.
proof idea
Pure definition, not a proof. The body is one conditional: if the hinge pair $(s,t)$ has orbit type T11, return the negation of the product of the integer area pairing and the squared-phase kernel weight; otherwise return zero. No lemmas are applied; decidability of the orbit test is inherited from the hinge-orbit classifier.
why it matters
This certificate is the integer backbone of the closed-form $m^2$ symbol on the $(1,1)$ orbit. The identity m2SlotCoeff_eq_cert casts it to $\mathbb{R}$ and divides by $32$, equating the real slot coefficient to the certificate. Finite double sums of the certificate then evaluate by decide to $-96$ on the axis TT mode and $0$ on the decoy gauge mode, which (after the $/32$ factor and the outer sum structure) yield the landed claims $m^2=!-3$ (TT, nonzero) and $m^2=0$ (gauge).
The same pattern is reused for further gauge probes (e.g. $m=(1,1,0,0)$, $v=e_2$) and for counterexample/sum lemmas in the star-edge and transported-orbit evaluation modules. It therefore underwrites the module's main landed facts while leaving the open punctured-limit glue FoldAlongM2Tendsto untouched. In the broader RS gravity stack this is bookkeeping for the continuum symbol of the discrete action, not a forcing-chain step (T0-T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.