e_302312
plain-language theorem explainer
For the concrete multi-index (3,0,2,3,1,2) on Fin 4, the folded coupling numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of the 256 decided cells. The proof is a single kernel decide on the two integer sides.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(3,0,2,3,1,2)$. The summed coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 12 of a 256-cell kernel certification that the 4D Regge exact-midpoint M2 numerator equals eight times an explicit integer table. Indices run over Fin 4 (four discrete directions).
The numerator m2Num folds a fixed coupling list: it sums contrib terms over that list for the six indices. The companion explicitZ is a pattern-matched Int table on the same six Fin 4 arguments (sample entries include 4, -2, and so on for particular index patterns).
Local goal, per the module doc: prove m2Num = 8·explicitZ cell by cell so a later fin_cases sweep can reassemble the universal identity.
proof idea
One-line computational proof: decide. Both sides are closed Int expressions once the six concrete Fin 4 values are substituted (m2Num reduces by folding the coupling list; explicitZ by pattern match). The kernel evaluates the integers and accepts equality. No lemmas beyond the two defs are invoked.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states ∀ six Fin 4 indices, m2Num = 8·explicitZ, proved by exhaustive fin_cases that discharge each cell (including this e_302312). That identity is the numerical spine of the Regge exact-midpoint M2–TT certification in 4D gravity analysis inside the monolith. It does not itself touch T0–T8 or the RCL; it is infrastructure for the discrete curvature/coupling bookkeeping those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.