e_330102
plain-language theorem explainer
For the six-index slot (3,3,0,1,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the summed coupling numerator at $(a,b,c,d,i,j)=(3,3,0,1,0,2)$ equals $8$ times the explicit integer kernel at those same indices: $N(3,3,0,1,0,2)=8\,Z(3,3,0,1,0,2)$.
background
This module is one of the finite case-chunks that discharge the identity $N=8Z$ pointwise on $(\mathrm{Fin},4)^6$. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and summing a local contribution at each six-tuple of indices. The closed form $Z=\mathrm{explicitZ}$ is an integer-valued pattern match on those same six indices (typical values $\pm 2,,4$, and zero off the listed patterns).
The ambient setting is the 4D Regge midpoint analysis of the M2TT identity in the Gravity.Analysis stack: one must check that the assembled discrete numerator matches eight times the explicit kernel everywhere on the finite index cube. Chunk 15 packages 256 such kernel decides; this declaration is the single point $(3,3,0,1,0,2)$.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left by evaluating the fold that defines the numerator, the right by evaluating the pattern-match definition of the explicit kernel and multiplying by 8. No lemmas are invoked beyond definitional computation on Fin 4 literals.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and proves it by exhaustive fin_cases on all six indices, dispatching each leaf to a chunk equality of this form. Without the pointwise facts, the global numerator-kernel identity for the 4D Regge midpoint M2TT analysis does not close.
In the Recognition gravity stack this is bookkeeping infrastructure rather than a new physical law: it certifies that the discrete coupling sum agrees with the explicit integer kernel used downstream in curvature and mass-side identities. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those enter only if later gravity theorems quote the assembled identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.