e_220120
plain-language theorem explainer
For the multi-index (2,2,0,1,2,0) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one cell in the exhaustive check that the Regge midpoint M2TT numerator matches the closed-form Z table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=2$, $c=0$, $d=1$, $i=2$, $j=0$ in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis for the M2TT identity. The numerator m2Num is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The comparison target explicitZ is a closed-form integer table on six Fin 4 indices (sample entries include 4 on diagonal-type pairs and -2 on mixed pairs).
The local claim of the file is the pointwise identity m2Num = 8·explicitZ, discharged in chunks of kernel decides rather than one giant proof. Chunk 10 holds the present sextuple among its 256 decides.
Upstream, only the two definitions matter: the fold that builds the numerator and the pattern-matched explicit table. No analytic lemma is required beyond evaluating those defs at a concrete point.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete indices (2,2,0,1,2,0) to integers and checks equality. No rewrite lemmas or induction; the kernel evaluates the fold for m2Num and the matching clause (or default) for explicitZ, then confirms the factor-of-eight relation.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in Fin 4 by exhaustive fin_cases. That global equality is the certified bridge between the summed coupling numerator and the explicit Z kernel used in the 4D Regge midpoint M2TT analysis.
In the Recognition gravity stack this is bookkeeping, not a new physical law: it locks the discrete curvature/numerator algebra so later continuum or continuum-limit arguments can quote a single closed form. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi ladder; those enter only if the M2TT identity is later tied to the broader RS gravity derivation.
Sibling chunk theorems cover the other index cells; together they close the 4^6 case split without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.