e_320320
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at indices (3,2,0,3,2,0) equals eight times the explicit Z-table entry there. Gravity analysts cite it as one of the 256 kernel cells that assemble the full m2Num = 8·explicitZ statement on (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For the six-tuple of indices $(3,2,0,3,2,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer table value at those same indices.
background
This module is chunk 14 of a 256-cell kernel certification that the folded midpoint numerator agrees with eight times an explicit integer table on every six-tuple of indices in $\mathrm{Fin},4$. The setting is 4D Regge-style midpoint analysis for the TT identity in the gravity stack.
The numerator is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry at the six indices. The explicit table is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite case split (sample values include $4$, $-2$, and so on). The claim is the numerical equality of those two integers at one fixed cell.
Upstream, both sides are pure definitions in the kernel certificate module; no analytic lemma is required beyond evaluating the fold and the table.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete integers (the fold over the coupling list versus eight times the matching table clause), so the equality is discharged by the decidable integer instance with no further lemmas.
why it matters
Parent theorem is the universal assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,;\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ and proves it by exhaustive fin_cases on all six indices. Each chunk cell such as this one supplies one concrete branch of that case tree.
In the Recognition gravity analysis, the identity certifies that the midpoint numerator used in the 4D TT/Regge exact-midpoint bookkeeping is exactly eight times a sparse explicit integer kernel. That closes a computational gap between the folded coupling definition and the closed-form table needed downstream. It is pure finite verification, not a continuum GR derivation; framework landmarks (T0–T8, RCL, $\phi$-ladder) are not invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.