e_320331
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at multi-index (3,2,0,3,3,1) equals eight times the explicit integer table entry. Gravity analysts assembling the 4D Regge exact midpoint M2TT kernel cite this chunk among the 256 kernel decides. Proof is a single computational `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,3,3,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit table value: $N(3,2,0,3,3,1)=8\,Z(3,2,0,3,3,1)$.
background
This module is chunk 14 of the 256 kernel decides establishing $N=8Z$ pointwise for the 4D Regge exact midpoint M2TT identity. Indices run over $\mathrm{Fin},4$ (four discrete directions).
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at the six-index slot. The closed form $Z=\mathrm{explicitZ}$ is an integer-valued lookup table on $(\mathrm{Fin},4)^6$, with sparse nonzero entries such as $4$ on matched pairs and $-2$ on crossed pairs.
The parent assembly theorem states $\forall a,b,c,d,i,j,, N=8Z$, proved by exhaustive fin_cases that invoke these pointwise chunks.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(3,2,0,3,3,1)$. The left side reduces the fold of couplingZList through contrib; the right side multiplies the table entry of explicitZ by 8. Equality of the resulting integers is discharged by the kernel decision procedure. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts the identity for every six-index in $(\mathrm{Fin},4)^6$ by casing on each coordinate and calling the matching chunk. That global equality is the certified numerator side of the Regge exact midpoint M2TT identity in 4D gravity analysis.
Within Recognition Science gravity work, these kernel certificates lock the discrete curvature/midpoint algebra before continuum or phenomenological limits are taken. The chunking (256 decides) keeps each goal inside the decision kernel and makes the full cover auditable. No open scaffold remains on this slot: the equality is fully decided.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.