e_320303
plain-language theorem explainer
Pointwise identity: the midpoint M2 numerator at multi-index (3,2,0,3,0,3) equals eight times the explicit Z-coupling at those indices. Gravity analysts cite it as one kernel cell in the Regge exact midpoint TT identity. The proof is a single `decide` on closed integer arithmetic.
Claim. For the six indices $(a,b,c,d,i,j)=(3,2,0,3,0,3)$ in $\mathrm{Fin}\,4$, the midpoint mass-squared numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer coupling $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint TT kernel certification. The local claim is the scalar identity $m_2^{\mathrm{num}}=8\cdot Z$ evaluated at concrete multi-indices in $(\mathrm{Fin},4)^6$, discharged by kernel decision procedures.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer contrib and the fold starts at $0$. The comparison target explicitZ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by an exhaustive pattern table (sample entries include $4$ on diagonal-like pairs such as $(0,0,1,1,2,2)$ and $-2$ on mixed pairs such as $(0,0,1,2,1,2)$).
The ambient setting is discrete Regge-style gravity analysis inside Recognition Science: certifying that a midpoint mass-squared numerator factors as eight times a sparse explicit coupling table before assembly into a quantified identity.
proof idea
One-line computational proof: by decide. Both sides are closed integer expressions once the six Fin 4 arguments are literals, so the kernel reduces the fold that defines the numerator and the pattern match that defines explicit $Z$, then checks numerical equality. No lemmas are invoked beyond the decidable equality of Int.
why it matters
This cell is one of the chunked pointwise facts that feed the assembly theorem m2Num_eq_eight_explicitZ, which states
$\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$
and is proved by exhaustive fin_cases on the six indices. Without the chunk identities, the quantified midpoint TT kernel identity does not close.
In the broader gravity stack this is bookkeeping infrastructure for the Regge exact-midpoint analysis, not a forcing-chain landmark (T5–T8) or an RCL step. It exists so the numerator/coupling relation is machine-checked at every multi-index before higher geometric claims rely on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.