e_110010
plain-language theorem explainer
For the six-index slot (1,1,0,0,1,0) in the 4D Regge midpoint kernel, the folded coupling numerator equals eight times the explicit integer table value. Gravity analysts assembling the global m2Num = 8·explicitZ identity cite this as one of the 256 kernel cases. Proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,1,0,0,1,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-case kernel that certifies the exact midpoint identity for the 4D Regge $M_2$ TT sector: every multi-index value of the folded numerator equals eight times a closed-form integer table.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list, accumulating integer contributions at each six-tuple of $\mathrm{Fin},4$ indices. The companion table $\mathrm{explicitZ}$ is a pattern-matched integer function on the same six indices (typical nonzero values $\pm 2,,4$). Both live in the kernel certificate module imported here.
The local setting is pure finite enumeration: six indices each in ${0,1,2,3}$ give 4096 formal slots, reduced by symmetry and chunking to 256 decide goals of which this file holds one block.
proof idea
One-line kernel proof: by decide. Lean reduces both sides on the concrete six-tuple $(1,1,0,0,1,0)$ to integers (left via the fold definition of the numerator, right via the pattern match on the explicit table) and checks equality by computation. No lemmas are invoked beyond the two definitions.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by exhaustive fin_cases and dispatches each leaf to a chunk theorem of this form. That global equality is the algebraic content of the Regge exact-midpoint $M_2$ TT identity in 4D inside the Gravity analysis stack.
Within Recognition Science this sits in the gravity sector that must eventually match the forced $D=3$ spatial geometry (T8) and the eight-tick octave structure; the factor of 8 in the identity is the same combinatorial 8 that appears throughout the octave bookkeeping. The chunk is scaffolding closure for the kernel, not an open physics claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.