IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk08
Chunk 08 of the generated numerical certificates for the 4D Regge midpoint m² TT identity. It packages a block of kernel-decidable equalities (the e_2000xx family) that feed the global m2Num assembly. Gravity analysts checking the discrete TT sector cite it when auditing the fold over index tuples. The content is script-generated scale-32 table lookup discharged by kernel decide.
claimA finite block of certified integer identities for the midpoint $m^2$ transverse-traceless sector in 4D Regge calculus: each entry equates a scaled discrete curvature/mass contribution to its tabulated value under the scale-32 encoding, as one chunk of the full $m_2^{\mathrm{Num}}$ sum over index tuples.
background
Recognition Science gravity work formalizes Regge calculus identities in Lean so that continuum TT (transverse-traceless) constraints have exact discrete counterparts. The midpoint $m^2$ TT identity is one such target: a numerical identity on lattice edge data that must hold before continuum limits or continuum matching arguments are trusted.
This module sits under Gravity.Analysis and imports the kernel-certificate layer (ReggeExactMidpointM2TTIdentity4DKernelCert). That upstream layer is generated by scripts/qg/regge_4d_m2_kernel_certs_20260721.py and uses Int List.foldl with scale-32 tables, discharging equalities by kernel decide only (no native_decide).
Chunk 08 is one slice of the enumerated certificate family (siblings e_200000–e_200023 and kin). The full index space is large (assembly later folds 4096 tuples), so certificates are split across chunk modules for compile-time and reviewability.
proof idea
Definition-and-certificate module, not a single prose theorem. Each local lemma is a closed integer equality produced by the generator: evaluate the scaled midpoint $m^2$ contribution on a fixed multi-index, compare to the precomputed table entry, and finish with kernel decide on the folded Int expression. No analytic continuum argument lives here; the structure is batch verification of table rows. Import surface is only Mathlib plus the shared kernel-cert module.
why it matters in Recognition Science
Downstream, ReggeExactMidpointM2TTIdentity4DM2NumAssemble imports this chunk to assemble $m_2^{\mathrm{Num}} = 8\cdot\mathrm{explicitZ}$ over all 4096 index tuples. Without the chunk certificates, the global numerical identity cannot be closed in-kernel. In the broader RS gravity stack, these Regge midpoint identities support discrete control of the TT sector before continuum or phenomenological gravity claims. The module is pure scaffolding of verified numerics: it does not itself state a continuum theorem, but it is a required brick in the exact discrete identity chain.
scope and limits
- Does not prove the continuum TT identity; only discrete scaled integer certificates.
- Does not cover the full 4096-tuple fold; only chunk 08 of m2Num certificates.
- Does not use native_decide; relies on kernel decide and generated tables.
- Does not define physical constants, phi-ladder masses, or Einstein-equation solutions.
- Does not argue convergence rates or continuum limits of the Regge complex.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_200000 -
theorem
e_200001 -
theorem
e_200002 -
theorem
e_200003 -
theorem
e_200010 -
theorem
e_200011 -
theorem
e_200012 -
theorem
e_200013 -
theorem
e_200020 -
theorem
e_200021 -
theorem
e_200022 -
theorem
e_200023 -
theorem
e_200030 -
theorem
e_200031 -
theorem
e_200032 -
theorem
e_200033 -
theorem
e_200100 -
theorem
e_200101 -
theorem
e_200102 -
theorem
e_200103 -
theorem
e_200110 -
theorem
e_200111 -
theorem
e_200112 -
theorem
e_200113 -
theorem
e_200120 -
theorem
e_200121 -
theorem
e_200122 -
theorem
e_200123 -
theorem
e_200130 -
theorem
e_200131 -
theorem
e_200132 -
theorem
e_200133 -
theorem
e_200200 -
theorem
e_200201 -
theorem
e_200202 -
theorem
e_200203 -
theorem
e_200210 -
theorem
e_200211 -
theorem
e_200212 -
theorem
e_200213 -
theorem
e_200220 -
theorem
e_200221 -
theorem
e_200222 -
theorem
e_200223 -
theorem
e_200230 -
theorem
e_200231 -
theorem
e_200232 -
theorem
e_200233 -
theorem
e_200300 -
theorem
e_200301 -
theorem
e_200302 -
theorem
e_200303 -
theorem
e_200310 -
theorem
e_200311 -
theorem
e_200312 -
theorem
e_200313 -
theorem
e_200320 -
theorem
e_200321 -
theorem
e_200322 -
theorem
e_200323 -
theorem
e_200330 -
theorem
e_200331 -
theorem
e_200332 -
theorem
e_200333 -
theorem
e_201000 -
theorem
e_201001 -
theorem
e_201002 -
theorem
e_201003 -
theorem
e_201010 -
theorem
e_201011 -
theorem
e_201012 -
theorem
e_201013 -
theorem
e_201020 -
theorem
e_201021 -
theorem
e_201022 -
theorem
e_201023 -
theorem
e_201030 -
theorem
e_201031 -
theorem
e_201032 -
theorem
e_201033