explicitZ
plain-language theorem explainer
Explicit six-index integer table on Fin 4 for the scale-32 kernel of the 4D Regge midpoint m² TT identity. Nonzero entries are only 4, −2, or 1; all other index tuples map to 0. Gravity analysts cite it as the kernel-checkable stand-in for the rational m² coefficient. Pure exhaustive pattern match; no proof content.
Claim. Define an integer-valued map $Z:\{0,1,2,3\}^6\to\mathbb{Z}$ by the listed nonzero assignments (each value in $\{4,-2,1\}$) on ordered sextuples of spacetime indices, and set $Z=0$ on every remaining sextuple.
background
The ambient module holds kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus. Certificates are generated from scale-32 integer fold tables so that Lean’s kernel decide can discharge equalities without native_decide.
The six arguments run over the four discrete directions of a 4-simplex edge/face labeling. Downstream glue casts this table to rationals by dividing by 32, recovering the explicit $m^2$ coefficient used in the flat Hessian / Bloch-data analysis.
Sibling chunk tables and closed-form integer counterparts live in the same certificate layer; the present map is the single exhaustive lookup that those pieces compare against.
proof idea
Definition only: a single large pattern match on six Fin 4 indices. Each listed clause returns a fixed Int literal (4, −2, or 1); the catch-all clause returns 0. No lemmas, tactics, or computation beyond the match.
why it matters
This table is the concrete kernel object that lets the midpoint $m^2$ TT identity be checked by decide. Downstream it is cast to rationals as explicitM2CoeffZ = explicitZ/32, equated pointwise to the closed coefficient via symFullZ_explicit_eq_closed and symFull_explicit_eq_symFull_closed, and related to the numerator assembly by m2Num_eq_eight_explicitZ ($m^2$ numerator equals $8\cdot Z$). Those equalities underwrite the 4D Regge flat-Hessian identities used in the gravity sector of the Recognition stack (discrete curvature / TT projection on the eight-tick lattice with $D=3$ spatial). Without an explicit integer kernel, the rational coefficient identities would not be kernel-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.