IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk06
Chunk 06 of the generated midpoint m² TT numerator certificates for 4D Regge calculus. It packages a block of scale-32 integer table entries (the e_1200** family) that the kernel can decide without native evaluation. Downstream assembly folds these chunks into the global m2Num = 8·explicitZ identity over all 4096 index tuples. Citation target for anyone auditing the split of the 4D midpoint TT numerator proof.
claimA finite block of certified integer table values $e_{1200ij}$ (scale-32) contributing to the 4D Regge midpoint $m^2$ transverse-traceless numerator identity, to be assembled into $m_2^{\mathrm{Num}} = 8\,Z_{\mathrm{explicit}}$ over the full $4096$-tuple index set.
background
Recognition Science gravity work formalizes discrete Regge calculus identities in Lean. The midpoint $m^2$ TT identity in 4D is a large finite check: for every multi-index in a $4096$-element set one must verify a numerator relation built from explicit integer combinations $Z$.
The upstream kernel-certificate module supplies the decision infrastructure: Int List.foldl over scale-32 tables, with proofs discharged by decide only (no native_decide). That keeps the kernel small and reproducible from the generator script regge_4d_m2_kernel_certs_20260721.py.
This module is one numbered chunk of those tables. Sibling declarations e_120000–e_120023 are the local certificate atoms; they are not physics postulates, only verified table rows for the numerator assembly.
proof idea
Definition-and-certificate module, not a discursive proof. Each e_1200** entry is a closed integer certificate over the scale-32 table, proved by kernel decide via the imported KernelCert infrastructure. No algebraic rewriting of continuum curvature appears here; the argument is exhaustive finite verification of precomputed table cells. The chunk boundary is purely organizational so that assembly can import manageable pieces.
why it matters in Recognition Science
Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, which "Assemble[s] m2Num = 8·explicitZ over all 4096 index tuples." Without the chunked numerator certificates the global 4D midpoint TT identity cannot be closed in-kernel. In the broader RS gravity stack this is scaffolding for discrete curvature / graviton-sector identities on the eight-tick, $D=3$ spatial backbone, not a new continuum force law. It closes a generated obligation rather than a named T0–T8 forcing step.
scope and limits
- Does not state the full 4096-tuple m2Num identity; only one certificate chunk.
- Does not prove continuum GR field equations or Einstein tensor identities.
- Does not introduce new physical constants or phi-ladder mass formulae.
- Does not use native_decide; relies on kernel decide over scale-32 Int tables.
- Does not cover other chunks or the final assembly theorem itself.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_120000 -
theorem
e_120001 -
theorem
e_120002 -
theorem
e_120003 -
theorem
e_120010 -
theorem
e_120011 -
theorem
e_120012 -
theorem
e_120013 -
theorem
e_120020 -
theorem
e_120021 -
theorem
e_120022 -
theorem
e_120023 -
theorem
e_120030 -
theorem
e_120031 -
theorem
e_120032 -
theorem
e_120033 -
theorem
e_120100 -
theorem
e_120101 -
theorem
e_120102 -
theorem
e_120103 -
theorem
e_120110 -
theorem
e_120111 -
theorem
e_120112 -
theorem
e_120113 -
theorem
e_120120 -
theorem
e_120121 -
theorem
e_120122 -
theorem
e_120123 -
theorem
e_120130 -
theorem
e_120131 -
theorem
e_120132 -
theorem
e_120133 -
theorem
e_120200 -
theorem
e_120201 -
theorem
e_120202 -
theorem
e_120203 -
theorem
e_120210 -
theorem
e_120211 -
theorem
e_120212 -
theorem
e_120213 -
theorem
e_120220 -
theorem
e_120221 -
theorem
e_120222 -
theorem
e_120223 -
theorem
e_120230 -
theorem
e_120231 -
theorem
e_120232 -
theorem
e_120233 -
theorem
e_120300 -
theorem
e_120301 -
theorem
e_120302 -
theorem
e_120303 -
theorem
e_120310 -
theorem
e_120311 -
theorem
e_120312 -
theorem
e_120313 -
theorem
e_120320 -
theorem
e_120321 -
theorem
e_120322 -
theorem
e_120323 -
theorem
e_120330 -
theorem
e_120331 -
theorem
e_120332 -
theorem
e_120333 -
theorem
e_121000 -
theorem
e_121001 -
theorem
e_121002 -
theorem
e_121003 -
theorem
e_121010 -
theorem
e_121011 -
theorem
e_121012 -
theorem
e_121013 -
theorem
e_121020 -
theorem
e_121021 -
theorem
e_121022 -
theorem
e_121023 -
theorem
e_121030 -
theorem
e_121031 -
theorem
e_121032 -
theorem
e_121033