e_100011
plain-language theorem explainer
Pointwise identity: the Regge midpoint numerator m2Num at multi-index (1,0,0,0,1,1) equals eight times the explicit kernel value explicitZ there. Gravity analysts cite it as one of the 256 kernel decides that assemble the full m2Num = 8·explicitZ identity on (Fin 4)^6. The proof is a single decide on closed integer arithmetic.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,0,0,0,1,1)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(1,0,0,0,1,1)$ equals $8\,Z(1,0,0,0,1,1)$, where $Z$ is the explicit integer kernel table.
background
In the 4D Regge midpoint M2–TT analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator m2Num folds a fixed coupling list, summing a local contribution at each table entry for the given multi-index. The comparison target explicitZ is a sparse pattern-matched table of small integers (entries such as 4, −2, and defaults) that records the closed-form kernel.
The local module is chunk 4 of a 256-way case split: every sextuple in (Fin 4)^6 is checked separately so that the global identity can be reassembled by exhaustive fin_cases. The setting is pure integer equality of discrete curvature couplings, not continuum GR.
proof idea
One-line computational proof: decide evaluates both sides as concrete Int expressions (the fold that defines m2Num at (1,0,0,0,1,1) versus 8 times the matching explicitZ clause) and discharges the equality by kernel decision procedure. No lemmas beyond the two defining defs are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states ∀ (a b c d i j : Fin 4), m2Num a b c d i j = 8 * explicitZ a b c d i j and proves it by nested fin_cases over all six indices. Each chunk theorem such as this one closes one concrete cell of that 4^6 grid.
In the Recognition gravity stack this identity certifies that the midpoint M2 numerator agrees with the explicit kernel used in the 4D TT analysis, so later continuum or continuum-limit arguments can quote the closed form rather than the fold. It is bookkeeping infrastructure inside the Gravity.Analysis Regge exact-midpoint line, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.