IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk05
Fifth chunk of precomputed integer certificates for the 4D Regge midpoint m² TT numerator identity. Each entry is a kernel-decidable equality on a scale-32 table cell for a fixed multi-index. Gravity analysts assembling the full 4096-tuple m2Num sum cite this block. Content is generated fold data, not a hand proof.
claimFor multi-indices in chunk 05 of the $4$D midpoint Regge $m^2$ TT table (scale-$32$ integer lattice), the certified cell values $e_{\sigma}$ equal the corresponding kernel evaluations, so they may be folded into $m_2^{\mathrm{Num}} = 8\sum Z(\sigma)$ over all $4096$ index tuples.
background
Recognition Science gravity work formalizes discrete Regge calculus identities that underwrite continuum limits and mass-ladder consistency. The midpoint $m^2$ TT identity in four dimensions is checked on a finite integer table (scale 32) rather than by symbolic expansion of every curvature term.
Upstream, the kernel-certificate module supplies the decide-only infrastructure: Int lists folded with scale-32 tables, no native_decide. This chunk module holds one contiguous block of those cells (siblings e_110000–e_110023 and kin), each a closed Prop that a single table entry matches the kernel.
The global count is $4096$ index tuples; chunks partition that range so Lean can typecheck certificates without a monolithic file.
proof idea
Definition-and-certificate module, not a narrative proof. Each sibling is a generated kernel certificate: an equality or decidable predicate on one multi-index cell, discharged by decide against the fold/scale-32 tables from the kernel-cert import. No tactic script beyond kernel decision; the script regge_4d_m2_kernel_certs_20260721.py emits the chunk.
why it matters in Recognition Science
Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, which builds $m_2^{\mathrm{Num}} = 8\cdot\mathrm{explicit}Z$ over all $4096$ tuples. Without every chunk, the assemble step cannot close the exact midpoint identity used in the 4D Regge gravity analysis stack. Sits in the Gravity domain as machine-checked numerics supporting discrete curvature identities tied to the broader RS forcing and continuum-limit story, not as a T0–T8 landmark itself.
scope and limits
- Does not prove the continuum Regge or Einstein equations, only finite table cells.
- Does not cover all 4096 tuples; only chunk 05 of the partition.
- Does not use native_decide; certificates are kernel decide on Int folds.
- Does not state physical units or phi-ladder mass formulae.
- Does not assemble m2Num; that is the downstream assemble module.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_110000 -
theorem
e_110001 -
theorem
e_110002 -
theorem
e_110003 -
theorem
e_110010 -
theorem
e_110011 -
theorem
e_110012 -
theorem
e_110013 -
theorem
e_110020 -
theorem
e_110021 -
theorem
e_110022 -
theorem
e_110023 -
theorem
e_110030 -
theorem
e_110031 -
theorem
e_110032 -
theorem
e_110033 -
theorem
e_110100 -
theorem
e_110101 -
theorem
e_110102 -
theorem
e_110103 -
theorem
e_110110 -
theorem
e_110111 -
theorem
e_110112 -
theorem
e_110113 -
theorem
e_110120 -
theorem
e_110121 -
theorem
e_110122 -
theorem
e_110123 -
theorem
e_110130 -
theorem
e_110131 -
theorem
e_110132 -
theorem
e_110133 -
theorem
e_110200 -
theorem
e_110201 -
theorem
e_110202 -
theorem
e_110203 -
theorem
e_110210 -
theorem
e_110211 -
theorem
e_110212 -
theorem
e_110213 -
theorem
e_110220 -
theorem
e_110221 -
theorem
e_110222 -
theorem
e_110223 -
theorem
e_110230 -
theorem
e_110231 -
theorem
e_110232 -
theorem
e_110233 -
theorem
e_110300 -
theorem
e_110301 -
theorem
e_110302 -
theorem
e_110303 -
theorem
e_110310 -
theorem
e_110311 -
theorem
e_110312 -
theorem
e_110313 -
theorem
e_110320 -
theorem
e_110321 -
theorem
e_110322 -
theorem
e_110323 -
theorem
e_110330 -
theorem
e_110331 -
theorem
e_110332 -
theorem
e_110333 -
theorem
e_111000 -
theorem
e_111001 -
theorem
e_111002 -
theorem
e_111003 -
theorem
e_111010 -
theorem
e_111011 -
theorem
e_111012 -
theorem
e_111013 -
theorem
e_111020 -
theorem
e_111021 -
theorem
e_111022 -
theorem
e_111023 -
theorem
e_111030 -
theorem
e_111031 -
theorem
e_111032 -
theorem
e_111033