e_030203
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at indices (0,3,0,2,0,3) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full 4D Regge midpoint M2–TT numerator identity over Fin 4. The proof is a single kernel decide on two concrete integers.
Claim. For indices $a=0$, $b=3$, $c=0$, $d=2$, $i=0$, $j=3$ in $\mathrm{Fin}\,4$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, the numerator of the M2–TT identity is written two ways. One is m2Num: fold contrib over a fixed coupling list, yielding an integer for each six-tuple of face/edge indices in $\mathrm{Fin},4$. The other is explicitZ: a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on).
The module certifies the relation $m_2^{\mathrm{num}}=8\cdot Z$ by splitting the $4^6=4096$ domain into chunks of kernel decides. This file is chunk 3. The local claim is only the single six-tuple $(0,3,0,2,0,3)$.
proof idea
One-line decide. Both sides reduce to concrete Int values: the left by evaluating the fold that defines the numerator, the right by looking up the explicit table and multiplying by eight. No lemmas are invoked beyond kernel computation of those integers.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $\mathrm{Fin},4$ and discharges the goal by exhaustive fin_cases on the six indices. Each chunk lemma such as this one supplies one concrete cell of that case split.
In the broader gravity stack this closes a numerator identity used in the Regge midpoint M2–TT analysis in four dimensions. It is bookkeeping, not a new physical law: once every cell matches, the folded coupling form may be replaced by the closed table times eight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.