e_223333
plain-language theorem explainer
Finite-case certificate that the 4D midpoint Regge numerator equals eight times the explicit integer kernel at multi-index (2,2,3,3,3,3). Gravity analysts assembling the full m2Num = 8·Z identity cite this chunk. Proof is a single kernel decide on concrete integer arithmetic.
Claim. At the multi-index $(2,2,3,3,3,3)\in(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit kernel value: $N(2,2,3,3,3,3)=8\,Z(2,2,3,3,3,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six indices in $\mathbb{F}_4$ are compared. The numerator $N=\mathrm{m2Num}$ is the fold of a fixed coupling list: each term contributes an integer $\mathrm{contrib}$ and the accumulator starts at 0. The comparison target $Z=\mathrm{explicitZ}$ is a closed pattern-match table on the same six indices (sample entries include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local module is chunk 10 of the kernel-decide campaign that checks $N=8Z$ pointwise. The ambient goal is the exact midpoint M2/TT identity in four dimensions; this file only discharges one concrete sextuple among the $4^6$ cases.
proof idea
One-line tactic proof: decide. Both sides reduce to closed integers once the six Fin 4 arguments are literals, so the kernel evaluates the fold defining $N$ and the match defining $Z$ and checks equality with the factor 8. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}_4,; N(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ and is proved by exhaustive fin_cases on the six indices. Each chunk theorem such as this one supplies one decided cell so the universal identity is a pure case split rather than a fresh algebraic derivation.
In the broader Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge calculus comparison (M2 versus TT) in $D=4$. It does not itself touch the forcing chain (T0–T8), the J-cost, or the $\varphi$-ladder; it is infrastructure that keeps the discrete curvature numerics certificate-complete.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.