e_212201
plain-language theorem explainer
Pointwise check that the folded Regge midpoint numerator m2Num at the Fin-4 sextuple (2,1,2,2,0,1) equals eight times the explicit integer table explicitZ at those indices. Gravity analysts cite it as one of 256 kernel decides that assemble the universal identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,2,2,0,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(2,1,2,2,0,1)=8\,Z(2,1,2,2,0,1)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on sextuples of $\mathrm{Fin},4$ indices are compared. The numerator $N=\mathrm{m2Num}$ is obtained by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib},t,a,b,c,d,i,j$. The comparison target $Z=\mathrm{explicitZ}$ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and defaults).
The local module is chunk 9 of a 256-way partition of the kernel: each chunk discharges a batch of concrete sextuples so that a later assembly theorem can recombine them. The ambient claim is the pointwise identity $N=8Z$ on all of $(\mathrm{Fin},4)^6$, which certifies that the folded midpoint mass-squared numerator collapses to an eightfold multiple of the closed form.
proof idea
One-line computational proof: by decide. Both sides are closed integer terms once the six indices are fixed literals, so Lean’s decision procedure evaluates the fold that defines the numerator and the pattern match that defines the explicit table, then checks equality of the resulting Int values. No lemmas beyond the two definitions are required.
why it matters
This declaration is one atomic brick in the exhaustive proof that the Regge midpoint numerator equals eight times the explicit kernel on every Fin-4 sextuple. The parent theorem m2Num_eq_eight_explicitZ introduces all six indices and runs fin_cases on each; the chunk theorems such as this one supply (or are the residual of) those concrete cases.
In the Recognition gravity stack, the identity is bookkeeping infrastructure for the 4D midpoint TT analysis: once $N=8Z$ is certified, downstream curvature and mass-squared identities can quote the cheap closed form instead of re-folding the coupling list. It does not itself invoke the forcing chain (T0–T8), $\varphi$, or the eight-tick octave; it is pure discrete kernel arithmetic supporting the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.