e_202203
plain-language theorem explainer
For the six Fin-4 indices (2,0,2,2,0,3), the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic cell in the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=0$, $c=2$, $d=2$, $i=0$, $j=3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $\mathrm{m2Num}$ is the fold of a fixed coupling list: it sums a local contribution at each coupling triple. The comparison target $\mathrm{explicitZ}$ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and defaults).
The module is chunk 8 of a 256-cell kernel certification that $\mathrm{m2Num}=8\cdot\mathrm{explicitZ}$ pointwise. Each cell fixes one concrete 6-tuple and discharges the equality by computation rather than by a symbolic identity on the fold.
Upstream, both maps live in the kernel certificate module; the present theorem only evaluates them at $(2,0,2,2,0,3)$.
proof idea
One-line proof by decide. Lean reduces both sides at the concrete Fin-4 indices to closed integers and checks equality in the kernel. No lemmas beyond the definitions of $\mathrm{m2Num}$ and $\mathrm{explicitZ}$ are invoked.
why it matters
The parent theorem $\mathrm{m2Num_eq_eight_explicitZ}$ assembles all 256 index cells by nested fin_cases and quotes each chunk theorem such as this one. That universal equality is the algebraic backbone of the exact midpoint $M_2$ identity in the 4D Regge gravity analysis.
Within Recognition Science gravity work, the identity supports discrete curvature bookkeeping on the eight-tick / $D=3$ side of the forcing chain by certifying that the folded coupling numerator is exactly eight copies of the sparse kernel table. Closing every chunk removes scaffolding from the midpoint certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.