czChunk10
plain-language theorem explainer
Chunk 10 of the machine-generated coupling table for the 4D Regge midpoint m² transverse-traceless kernel identity. Each entry is a rational coefficient (num/den) paired with multi-index defect and dual-defect exponents. Gravity analysts cite it only as a data fragment inside the full coupling list. The body is a literal list literal; no proof work lives here.
Claim. A fixed finite list of coupling records, each record a rational $n/d$ together with integer multi-indices for the defect factors $\mathrm{De}$ and dual-defect factors $\mathrm{Dep}$. This is the tenth contiguous block of the full midpoint $m^2$ TT kernel coupling table in four dimensions.
background
The module holds kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus. Data are produced by an external script that emits scale-32 integer tables; Lean only folds and decides equality, never runs native evaluation.
Each record has type CZ: a numerator, a natural denominator, and integer exponents for the defect monomials and their duals. Sibling chunks czChunk0–czChunk15 partition the same table so that individual list literals stay inside Lean’s practical size limits.
Upstream, the structure CZ is the only dependency. Downstream assembly concatenates every chunk into one master list used by the kernel identity certificates.
proof idea
There is no proof. The declaration is a pure data definition: a concrete List CZ written out as structure literals. Equality of this chunk against the corresponding generated source list is discharged later by a one-line decide bridge theorem.
why it matters
The full coupling table is the algebraic backbone of the midpoint $m^2$ TT kernel identity for 4D Regge gravity. This chunk is one of sixteen slices that couplingZList concatenates; the bridge theorem czChunk10_bridge certifies that the slice matches the script output under toCZ.
Inside Recognition Science the identity sits in the gravity-analysis layer that checks discrete curvature and mass-squared kernels against continuum expectations. It does not itself invoke the forcing chain (T5–T8), the Recognition Composition Law, or the $\phi$-ladder mass formula; it supplies certified combinatorial input those higher arguments may later consume when discrete gravity is tied back to the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.