e_310032
plain-language theorem explainer
For the six-index tuple (3,1,0,0,3,2) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel point checks. The proof is a single decide on concrete integer arithmetic.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(3,1,0,0,3,2)$ equals $8$ times the explicit integer kernel entry at the same indices: $N(3,1,0,0,3,2)=8\,Z(3,1,0,0,3,2)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $N=\mathrm{m2Num}$ is obtained by folding a fixed coupling list and summing local contributions at the given indices. The comparison target $Z=\mathrm{explicitZ}$ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and so on).
The module is chunk 13 of a 256-point kernel certification: each chunk discharges a batch of concrete index sextuples toward the global identity $N=8Z$. The local setting is pure finite enumeration over $\mathrm{Fin},4$, not continuum gravity.
Upstream, both $N$ and $Z$ are defined in the kernel certificate module; this lemma only evaluates them at one fixed point.
proof idea
One-line proof by decide. Lean reduces both sides at the concrete indices $(3,1,0,0,3,2)$ to closed integers (the fold for $N$ and the pattern match for $Z$) and checks equality of $N$ with $8Z$ by computation. No lemmas beyond the definitions of m2Num and explicitZ are invoked.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,,N=8Z$ by exhaustive fin_cases on all six indices. Each chunk lemma such as this one is a leaf in that case tree (or an equivalent decide batch), so the global midpoint M2TT numerator identity rests on these pointwise checks.
Within Recognition gravity, the identity is bookkeeping for the discrete Regge/midpoint kernel in 4D, not a new continuum Einstein equation. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi-ladder mass formula; it is infrastructure under the gravity analysis stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.