e_021301
plain-language theorem explainer
For the fixed index sextuple (0,2,1,3,0,1) in (Fin 4)^6, the Regge midpoint numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts cite it as one cell of the 4D midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,3,0,1)$ with each index in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel entry $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 identity: the claim that the folded numerator m2Num agrees with eight times a closed-form integer table explicitZ on every sextuple of indices in Fin 4. The module doc states the local goal as "m2Num = 8·explicitZ, chunk 2 (256 kernel decides)."
Upstream, m2Num a b c d i j is defined by folding contrib over couplingZList, starting from 0. The companion table explicitZ is a pattern-matched Int-valued function on six Fin 4 arguments (sample clauses include values 4, −2, and so on). Both live in the kernel-cert module imported here.
The ambient setting is discrete gravity analysis: verifying an algebraic identity that underwrites the midpoint form of the second-moment (M2) TT kernel in four dimensions, index by index.
proof idea
One-line computational proof: by decide. Lean reduces both sides on the concrete sextuple (0,2,1,3,0,1) to integers (the fold defining m2Num versus the pattern match for explicitZ) and checks equality by the kernel decision procedure. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
This cell feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts the identity for every (a,b,c,d,i,j) : Fin 4 by exhaustive fin_cases. Each chunk theorem such as this one discharges one concrete goal in that case split (or an equivalent 256-way kernel partition).
In the Recognition gravity stack, the midpoint M2/TT identity is bookkeeping for the discrete curvature kernel used in Regge-style analyses. Closing the numerator-versus-table match removes a scaffolding obligation on the 4D kernel cert: once every chunk is decided, the universal equality is available downstream without further case work.
It is not itself a forcing-chain (T0–T8) step; it is infrastructure under the gravity analysis layer that those continuum claims eventually rest on when discrete kernels are specialized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.