e_203332
plain-language theorem explainer
For the six-index slot (2,0,3,3,3,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these per-slot identities when assembling the global Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2,b=0,c=3,d=3,i=3,j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification. The local goal, stated in the module header, is to prove $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ on a block of the $4^6$ index space by kernel decides (256 decides per chunk).
$\mathrm{m2Num}(a,b,c,d,i,j)$ is the integer obtained by folding $\mathrm{couplingZList}$ and summing the contribution of each coupling term at those six $\mathrm{Fin},4$ indices. $\mathrm{explicitZ}$ is the closed-form lookup table on the same six indices, returning small integers such as $4$, $-2$, and so on on the matched patterns.
The ambient setting is discrete gravity analysis: verifying that a numerator built from Regge-style couplings collapses exactly to eight times a sparse explicit kernel, which is the algebraic content needed for the midpoint M2TT identity in 4D.
proof idea
One-line proof by decide. Both sides are closed integer expressions once the six concrete $\mathrm{Fin},4$ arguments are substituted: the left-hand side evaluates the fold that defines $\mathrm{m2Num}$, the right-hand side multiplies the pattern-matched $\mathrm{explicitZ}$ value by 8. Lean’s kernel decision procedure checks integer equality; no lemmas are invoked beyond the definitions of $\mathrm{m2Num}$ and $\mathrm{explicitZ}$.
why it matters
This is one atomic slot in the exhaustive case split that builds $\mathrm{m2Num_eq_eight_explicitZ}$, the parent theorem in the assemble module. That parent states $\forall a,b,c,d,i,j:\mathrm{Fin},4,;\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ and discharges the quantifiers by nested $\mathrm{fin_cases}$, each leaf pointing at a chunk identity such as this one.
In the Recognition gravity stack these identities underwrite the exact algebraic midpoint form of the 4D M2TT relation used in Regge-style curvature bookkeeping. They do not themselves invoke the forcing chain (T5–T8) or the J-cost; they sit downstream as certified discrete-geometry arithmetic that later continuum or continuum-limit arguments can quote without re-checking the fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.