e_133103
plain-language theorem explainer
Pointwise identity: the midpoint Regge numerator at indices (1,3,3,1,0,3) equals eight times the explicit integer kernel at those same indices. Gravity analysts cite it as one cell of the 256-case kernel that underwrites the global m2Num = 8·explicitZ theorem. The proof is a single decide on concrete integers.
Claim. For the index sextuple $(1,3,3,1,0,3)\in(\mathbb{F}_4)^6$, the midpoint mass-squared numerator equals eight times the explicit integer kernel value: $m_2^{\mathrm{num}}(1,3,3,1,0,3)=8\,Z_{\mathrm{expl}}(1,3,3,1,0,3)$.
background
This module is chunk 7 of a 256-way case split proving that the midpoint Regge numerator equals eight times an explicit integer table on every sextuple of indices in $\mathbb{F}_4$. The ambient setting is 4D Regge calculus at the exact midpoint configuration used to certify a mass-squared / TT identity.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a coupling list and summing local contributions at those six $\mathrm{Fin},4$ indices. The comparison target $Z_{\mathrm{expl}}$ is a closed-form integer function on the same domain, given by a finite pattern of values such as $4$, $-2$, and related entries on distinguished index patterns.
The local claim fixes one concrete sextuple and asserts numerical equality after the factor of eight. Sibling chunks cover the remaining cells; the assembly theorem recombines them by exhaustive fin_cases.
proof idea
One-line computational proof: decide evaluates both sides at the concrete indices $(1,3,3,1,0,3)$. The left side reduces by unfolding the fold over couplingZList and summing contributions; the right side multiplies the table value of explicitZ by eight. Both land on the same integer, so the decision procedure closes the goal with no manual algebra.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and discharges the universal quantifier by six nested fin_cases over the 4-element index set. Each chunk such as this one supplies one of the 256 ground instances the assembler needs.
In the gravity analysis stack, that global identity is the certified numerator form for the exact-midpoint 4D Regge / TT mass-squared relation. Without the pointwise cells, the fold definition of $m_2^{\mathrm{num}}$ would remain only an algorithmic sum, not matched to the explicit kernel used downstream. The module doc frames the whole file as “m2Num = 8·explicitZ, chunk 7 (256 kernel decides),” so this declaration is pure kernel filler, not a new physical hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.