e_000101
plain-language theorem explainer
Kernel certificate for one Fin-4 sextuple: the midpoint M2 numerator equals eight times the explicit Z table at indices (0,0,0,1,0,1). Gravity analysts cite it only as a brick in the 256-case exhaustion of the 4D Regge midpoint identity. The proof is a single native decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,0,1,0,1)$ in $(\mathbb{F}_4)^6$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 0 of a 256-way kernel split proving $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathbb{F}_4)^6$. The ambient setting is the exact midpoint analysis of the 4D Regge M2/TT identity in the Gravity.Analysis stack.
Upstream, $m_2^{\mathrm{num}}$ is the integer obtained by folding couplingZList and summing each term's contribution at the six indices. The comparison table $Z$ is an explicit pattern-matched function $\mathbb{F}_4^6\to\mathbb{Z}$ (nonzero only on a sparse set of index patterns, e.g. values $\pm 2,4$).
The full quantified statement is assembled downstream by exhausting all six fin_cases; each concrete sextuple is discharged by one of these chunk theorems.
proof idea
One-line computational proof: by decide. Both sides reduce to closed integer expressions once the six Fin 4 arguments are literals, so the kernel decision procedure checks equality with no lemmas or rewriting.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and closes by six nested fin_cases over $\mathbb{F}_4$. Without the 256 pointwise certificates the assembly cannot finish.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge kernel in 4D (spatial $D=3$ plus time), not a forcing-chain step (T5–T8) or an RCL identity. It is pure finite enumeration supporting the continuum/discrete match claimed by the broader M2/TT analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.