e_211301
plain-language theorem explainer
Pointwise identity: the Regge midpoint m₂ numerator at multi-index (2,1,1,3,0,1) equals eight times the explicit Z-table entry there. Gravity analysts cite it as one of 256 kernel cells feeding the global m₂Num = 8·explicitZ theorem. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,1,3,0,1)$ in $(\mathrm{Fin}\,4)^6$, the integer midpoint $m_2$ numerator equals $8$ times the explicit coupling table value $Z$ at those same indices.
background
This module is chunk 9 of a 256-cell kernel certifying that the 4D Regge midpoint $m_2$ numerator matches eight times a closed-form integer table. The ambient setting is exact midpoint identities for the TT sector of discrete gravity on a 4-simplex skeleton.
The numerator m2Num is defined by folding a fixed coupling list: it sums contribution terms contrib t a b c d i j over that list, yielding an Int. The comparison table explicitZ is a six-argument function on Fin 4 with finitely many nonzero integer clauses (e.g. value 4 or −2 on selected index patterns) and implicit zero elsewhere.
Both objects live in the kernel-cert module imported here. The present declaration fixes one concrete six-tuple and asserts numerical equality after the factor of eight.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete Fin 4 arguments (2,1,1,3,0,1) to closed integers and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal claim $\forall a,b,c,d,i,j,; m_2\mathrm{Num}=8\cdot Z$. Its proof exhausts all $4^6$ index tuples; this chunk cell is one of those cases (module doc: "m2Num = 8·explicitZ, chunk 9 (256 kernel decides)").
In the Recognition gravity stack, the identity underwrites exact midpoint Regge calculus in 4D (consistent with the T8 forcing of three spatial dimensions plus time). It is bookkeeping infrastructure rather than a new physical law: once every cell is decided, the assembled equality licenses replacing the folded numerator by the sparse explicit table in downstream curvature and mass-gap arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.