e_200102
plain-language theorem explainer
For the six-index slot (2,0,0,1,0,2) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global Regge midpoint M2TT relation. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}0$, $c{=}0$, $d{=}1$, $i{=}0$, $j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling 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 is one chunk of a 256-case kernel certification that the Regge-exact midpoint numerator equals eight times a closed-form integer table. The ambient setting is 4D discrete gravity analysis: six indices each run over $\mathrm{Fin},4$, and equalities are checked pointwise before assembly.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling triple at the given six indices. The comparison target $\mathrm{explicitZ}$ is a sparse pattern-matched integer table on those same six indices (nonzero only on a short list of ordered sextuples, with values such as $4$ or $-2$).
Chunk 8 isolates one concrete sextuple so that the full universal identity can later be rebuilt by exhaustive fin_cases rather than a single giant decide.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side evaluates the fold that defines $m_2^{\mathrm{num}}$ at $(2,0,0,1,0,2)$, the right-hand side multiplies the table lookup $\mathrm{explicitZ}(2,0,0,1,0,2)$ by $8$. Lean’s kernel decision procedure discharges the resulting integer equality with no lemmas or rewriting.
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ for all six $\mathrm{Fin},4$ indices. That assembler runs nested fin_cases and invokes each chunk identity (including this one) at the matching sextuple. Closing every chunk removes scaffolding from the Regge-exact midpoint M2TT 4D kernel certificate used in the gravity analysis stack.
In the broader Recognition Science gravity line, these identities pin the discrete curvature/coupling numerator to an explicit integer kernel before continuum or phenomenological comparisons. They do not themselves invoke the forcing chain (T5–T8) or the Recognition Composition Law; they are pure algebraic bookkeeping inside the 4D Regge midpoint certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.