IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk12
Chunk 12 of machine-generated kernel certificates for the exact midpoint m² transverse-traceless identity in 4D Regge calculus. Each entry is a decide-closed equality on scaled integer tables. Gravity analysts assembling the global m2Num sum over 4096 index tuples import this block. Proofs are pure kernel decide on foldl-built scale-32 data; no native_decide.
claimA finite family of certified equalities $e_{300000},\ldots$ establishing the midpoint $m^2$ TT kernel identities on the corresponding index blocks, with all arithmetic carried in scale-$32$ integer tables so that each identity reduces to a decidable equality of integers.
background
In the 4D Regge analysis, the midpoint $m^2$ transverse-traceless identity is checked by reducing curvature and edge contributions to explicit integer arithmetic. The upstream kernel-cert module supplies the shared infrastructure: Int List.foldl constructions and scale-32 tables, with every atomic check discharged by decide only (no native_decide).
This module is one numbered chunk of those certificates. The sibling names $e_{300000}$–$e_{300023}$ (and their companions in the file) are the concrete certificate lemmas for a contiguous block of index tuples. They sit between the kernel infrastructure and the global assembly that forms $m_2^{\mathrm{Num}}=8\cdot\mathrm{explicitZ}$ over all $4096$ tuples.
proof idea
Definition-and-certificate module, not a single theorem. Each certificate is a one-line (or short) decide proof that a particular scaled integer identity holds for its index block. The arithmetic is pre-tabulated at scale 32 and folded with List.foldl; the kernel closes the Prop. No analytic rewriting beyond the generated tables.
why it matters in Recognition Science
Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, which assembles $m_2^{\mathrm{Num}}=8\cdot\mathrm{explicitZ}$ over the full $4096$ index space. Without the chunk certificates, the assemble step cannot discharge every tuple. In the broader gravity stack this is bookkeeping for the exact midpoint TT identity that underwrites the discrete curvature side of the Recognition Science gravity analysis, not a new physical law by itself.
scope and limits
- Does not state the global m² TT identity; only one index chunk of kernel equalities.
- Does not perform the 4096-tuple assembly; that lives in the downstream Assemble module.
- Does not introduce new continuum or continuum-limit claims about Regge gravity.
- Does not use native_decide; all checks are kernel decide on scale-32 Int tables.
- Does not define the physical constants or the forcing chain (T0–T8).
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_300000 -
theorem
e_300001 -
theorem
e_300002 -
theorem
e_300003 -
theorem
e_300010 -
theorem
e_300011 -
theorem
e_300012 -
theorem
e_300013 -
theorem
e_300020 -
theorem
e_300021 -
theorem
e_300022 -
theorem
e_300023 -
theorem
e_300030 -
theorem
e_300031 -
theorem
e_300032 -
theorem
e_300033 -
theorem
e_300100 -
theorem
e_300101 -
theorem
e_300102 -
theorem
e_300103 -
theorem
e_300110 -
theorem
e_300111 -
theorem
e_300112 -
theorem
e_300113 -
theorem
e_300120 -
theorem
e_300121 -
theorem
e_300122 -
theorem
e_300123 -
theorem
e_300130 -
theorem
e_300131 -
theorem
e_300132 -
theorem
e_300133 -
theorem
e_300200 -
theorem
e_300201 -
theorem
e_300202 -
theorem
e_300203 -
theorem
e_300210 -
theorem
e_300211 -
theorem
e_300212 -
theorem
e_300213 -
theorem
e_300220 -
theorem
e_300221 -
theorem
e_300222 -
theorem
e_300223 -
theorem
e_300230 -
theorem
e_300231 -
theorem
e_300232 -
theorem
e_300233 -
theorem
e_300300 -
theorem
e_300301 -
theorem
e_300302 -
theorem
e_300303 -
theorem
e_300310 -
theorem
e_300311 -
theorem
e_300312 -
theorem
e_300313 -
theorem
e_300320 -
theorem
e_300321 -
theorem
e_300322 -
theorem
e_300323 -
theorem
e_300330 -
theorem
e_300331 -
theorem
e_300332 -
theorem
e_300333 -
theorem
e_301000 -
theorem
e_301001 -
theorem
e_301002 -
theorem
e_301003 -
theorem
e_301010 -
theorem
e_301011 -
theorem
e_301012 -
theorem
e_301013 -
theorem
e_301020 -
theorem
e_301021 -
theorem
e_301022 -
theorem
e_301023 -
theorem
e_301030 -
theorem
e_301031 -
theorem
e_301032 -
theorem
e_301033