e_302200
plain-language theorem explainer
For the multi-index (3,0,2,2,0,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integer arithmetic.
Claim. For indices $a{=}3$, $b{=}0$, $c{=}2$, $d{=}2$, $i{=}0$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel integer: $\mathrm{m2Num}(3,0,2,2,0,0)=8\cdot\mathrm{explicitZ}(3,0,2,2,0,0)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local goal, stated in the module header, is to discharge $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ on a block of the $4^6=4096$ index tuples by kernel decides (here chunk 12, 256 decides).
$\mathrm{m2Num}(a,b,c,d,i,j)$ is the integer obtained by folding a fixed coupling list: start at $0$ and add each term's contribution at those six indices. $\mathrm{explicitZ}$ is the closed-form integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on the listed patterns).
The identity equates the folded numerator to eight times that table entry, index by index. Upstream definitions live in the KernelCert module; this file only specializes them.
proof idea
One-line kernel proof: by decide. Both sides are closed integer expressions once the six concrete $\mathrm{Fin},4$ indices are substituted into $\mathrm{m2Num}$ (a fold of contributions) and $\mathrm{explicitZ}$ (a pattern-matched constant). Lean’s decision procedure evaluates the equality and closes the goal with no lemmas or case splits in this declaration.
why it matters
Feeds the assembler theorem $\mathrm{m2Num_eq_eight_explicitZ}$, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ by exhaustive fin_cases and invokes each chunk equality such as this one. That global identity is part of the Regge exact-midpoint $M_2$ TT analysis in the Gravity domain: it certifies that the folded coupling numerator matches the explicit kernel table up to the universal factor $8$.
In the broader Recognition Science gravity stack, such kernel certificates underwrite discrete curvature / Regge-calculus identities used when matching continuum limits and mass-ladder phenomenology. This declaration is pure bookkeeping: one of 256 decides in chunk 12, not a new physical law, but required so the assembler has a complete, sorry-free case cover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.