e_211302
plain-language theorem explainer
Kernel certificate: the discrete numerator coupling at multi-index (2,1,1,3,0,2) equals eight times the explicit integer kernel Z at that same index. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite it as one of the 256 decide-chunks. The proof is a single closed decision-procedure check on concrete Fin-4 data.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,1,3,0,2)$ with each coordinate in $\mathbb{F}_4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge-calculus analysis of the exact midpoint M2–TT identity. The numerator side is the integer-valued map $m_2^{\mathrm{num}}$ obtained by folding a fixed coupling list: each term contributes an integer contrib at a six-index in $(\mathbb{F}_4)^6$, and the fold starts from zero. The comparison object is the sparse explicit kernel $Z$, a total function $(\mathbb{F}_4)^6\to\mathbb{Z}$ defined by a finite pattern match (nonzero only on a short list of index patterns, with values such as $\pm 2,\pm 4$).
The local claim of the file is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on the whole $4^6$ grid, discharged in decide-sized chunks rather than one giant proof. Chunk 9 supplies one concrete cell of that grid. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ are pure definitions in the kernel-certificate module; no analytic hypotheses are carried.
proof idea
One-line closed proof: decide. Lean evaluates both sides on the concrete six-tuple of Fin 4 values, reduces the fold that defines the numerator and the pattern match that defines $Z$, and checks integer equality. No lemmas are invoked beyond the decidable equality instance on Int.
why it matters
Parent theorem is the assembled identity m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}_4,; m_2^{\mathrm{num}}=8\cdot Z$ and is proved by exhaustive fin_cases over the six indices. Each chunk such as this one supplies (or is regenerated as) a single cell of that case tree, so the full algebraic certificate of the 4D midpoint M2–TT numerator identity rests on these decide atoms.
In the Recognition gravity stack this identity is bookkeeping infrastructure: it certifies that the discrete curvature/coupling numerator matches the closed-form kernel used downstream in Regge-exact midpoint analysis. It does not itself invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder; it is a pure integer identity on the 4D combinatorial kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.