e_303301
plain-language theorem explainer
For the six Fin-4 indices (3,0,3,3,0,1), the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel cells that assemble the global identity m2Num = 8·explicitZ. The proof is a pure decide on concrete integers.
Claim. For indices $a=3$, $b=0$, $c=3$, $d=3$, $i=0$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 12 of a 256-cell kernel certification that the Regge midpoint numerator equals eight times an explicit integer table. The ambient setting is 4D discrete gravity analysis: six indices in $\mathrm{Fin},4$ label a contribution to a midpoint mass-squared style numerator.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six indices (sample values include $4$, $-2$, and other small integers on the listed patterns).
The global claim is $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$. Because both sides are computable on a finite domain, the proof is split into decide-able cells; this declaration is the cell for $(3,0,3,3,0,1)$.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the equality on the concrete Fin-4 sextuple to integers and checks equality by the kernel decision procedure. No algebraic lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (list fold of contributions) and $\mathrm{explicitZ}$ (pattern table).
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every cell by nested fin_cases on the six indices; this cell is one of those branches. Closing all 256 decides discharges the exact midpoint identity $m_2^{\mathrm{num}}=8,Z$ used in the Regge 4D analysis stack.
In the broader Recognition gravity line, such exact discrete identities pin the midpoint/TT kernel before continuum or continuum-limit statements. The module header states the goal directly: "$m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$, chunk 12 (256 kernel decides)." No open scaffolding remains on this cell once decide succeeds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.