e_320202
plain-language theorem explainer
For multi-index (3,2,0,2,0,2) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one decided cell in chunk 14 of the 256-kernel case split. The proof is a single decide on concrete integer arithmetic after unfolding the fold.
Claim. For indices $a=3$, $b=2$, $c=0$, $d=2$, $i=0$, $j=2$ in $\mathrm{Fin}\,4$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the explicit kernel entry $Z(a,b,c,d,i,j)$.
background
This module sits in the Gravity analysis stack for the exact midpoint M2TT identity in 4D Regge calculus. The local setting is the chunked verification that the folded numerator equals eight times an explicit integer kernel on every multi-index in $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling triple at the six Fin-4 slots. The explicit kernel $Z$ is a pattern-matched integer table on those same six indices (sample entries include $4$, $-2$, and further signed values on other patterns).
Chunk 14 is one block of the 256 kernel decides that discharge individual cells before the global assembler runs.
proof idea
One-line computational proof: decide. Lean unfolds m2Num (the fold over couplingZList with contrib) and explicitZ at the concrete indices $(3,2,0,2,0,2)$, reduces both sides to closed integers, and checks equality by the decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
This cell is one of the concrete witnesses consumed by the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by exhaustive fin_cases on all six Fin-4 arguments. Without the chunk theorems, that universal identity does not close.
In the broader Recognition gravity stack, the factor-of-eight match between the folded coupling numerator and the explicit kernel is the algebraic backbone of the 4D Regge midpoint M2TT identity. It is infrastructure for the discrete curvature side of the RS gravity analysis, not a forcing-chain (T0–T8) step, but it is required before continuum or continuum-limit claims that quote the midpoint identity can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.