e_322123
plain-language theorem explainer
For the six Fin-4 indices (3,2,2,1,2,3), the summed Regge coupling numerator m2Num equals eight times the explicit integer kernel explicitZ at that multi-index. Gravity analysts cite it as one atomic case in the 4D midpoint M2 TT identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(3,2,2,1,2,3)$. The folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
This module is chunk 14 of a case split proving $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ on all $4^6$ multi-indices in the 4D Regge exact-midpoint M2 TT identity kernel.
$\mathrm{m2Num}(a,b,c,d,i,j)$ is the integer obtained by folding $\mathrm{couplingZList}$ and summing each term's contribution at those six Fin-4 slots. $\mathrm{explicitZ}$ is the closed-form piecewise integer table on the same six indices (sample entries include $4$, $-2$, and so on for the listed patterns).
The local goal is purely algebraic bookkeeping: show the fold equals eight times the table entry, index by index, so a later assembler can reassemble the universal identity.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(3,2,2,1,2,3)$ and checks integer equality. No lemmas are invoked beyond the definitions of $\mathrm{m2Num}$ and $\mathrm{explicitZ}$.
why it matters
Feeds the parent theorem $\mathrm{m2Num_eq_eight_explicitZ}$, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,;\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ and discharges the claim by exhaustive fin_cases over the six indices. Each chunk theorem such as this one is one decided leaf of that $256$-style kernel split (module doc: "m2Num = 8·explicitZ, chunk 14").
In the broader gravity analysis, the identity certifies that the midpoint M2 TT numerator matches the explicit Z kernel used in the Regge calculus side of the Recognition Science gravity stack. It is pure discrete linear algebra on Fin 4, not a continuum GR statement, but it is a required exact certificate before continuum or continuum-limit claims can be attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.