e_101303
plain-language theorem explainer
Pointwise kernel identity: for the Fin-4 index sextuple (1,0,1,3,0,3), the discrete numerator m2Num equals eight times the closed-form integer explicitZ. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,0,1,3,0,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 4 of a 256-way kernel certification that the 4D Regge midpoint numerator matches an explicit closed form: $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of indices in $\mathbb{F}_4$.
Upstream, $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: it sums integer contributions contrib over couplingZList at the six indices. The companion explicitZ is a pattern-matched integer table on $\mathrm{Fin},4^6$ (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local setting is pure finite enumeration: no continuum limit, no metric ansatz beyond the discrete midpoint kernel already certified in the imported KernelCert module.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the concrete sextuple $(1,0,1,3,0,3)$—the fold defining $m_2^{\mathrm{num}}$ and the pattern match defining $Z$—and checks integer equality. No lemmas are invoked beyond the decidable equality of Int.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ by exhausting all $4^6$ index tuples. Each chunk theorem such as this one discharges one concrete cell so the global identity is a pure case split rather than a symbolic rewrite.
In the Recognition gravity stack this identity is bookkeeping for the discrete curvature kernel used in Regge-style midpoint analyses in $D=3+1$. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is infrastructure that keeps the 4D kernel certificate fully machine-checked.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.