e_323010
plain-language theorem explainer
For the six-index slot (3,2,3,0,1,0) in the 4D Regge midpoint kernel, the folded numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts assembling the full m2Num = 8·explicitZ identity cite this as one of the 256 decided cells. The proof is a single kernel `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,3,0,1,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(3,2,3,0,1,0)=8\,Z_{\mathrm{explicit}}(3,2,3,0,1,0)$.
background
This module is chunk 14 of a 256-cell kernel certification that the 4D Regge-exact midpoint numerator equals eight times a closed integer table. The ambient setting is discrete gravity analysis: six indices in $\mathrm{Fin},4$ label the tensor slots of a midpoint contribution.
Upstream, m2Num is the fold of a coupling list: it accumulates contrib t a b c d i j over couplingZList, yielding an Int. The companion explicitZ is a pattern-matched integer table on the same six indices (sample clauses give values such as $4$, $-2$, etc.). The claim under audit is one concrete equality between those two functions at a fixed multi-index.
The parent assembly theorem will range over all $4^6$ slots by fin_cases; each chunk supplies a block of decided equalities so the exhaustive case split stays modular.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the decision procedure discharges the equality with no lemmas or rewriting. No upstream theorem is applied beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and proves it by six nested fin_cases over Fin 4. Each leaf of that case tree is one of these chunk theorems (here e_323010 for slot 3,2,3,0,1,0).
In the Recognition gravity stack this identity is bookkeeping for the Regge midpoint kernel: once numerator and explicit table match everywhere, later curvature and mass-ladder arguments can quote the closed form instead of the fold. It does not itself touch T0–T8 or the RCL; it is infrastructure inside the 4D discrete-gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.