IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk10
Chunk 10 of the generated midpoint m-squared TT identity certificates for 4D Regge calculus. It packages a contiguous block of kernel-decided edge lemmas (the e_2200xx family) that feed the global numerical assembly of m2Num. Gravity analysts reconstructing the exact discrete identity cite this file as one of the fold-table shards. Content is pure certificate data discharged by kernel decide on scale-32 integer tables.
claimA finite block of kernel certificates establishing the midpoint $m^2$ transverse-traceless identity contributions for a contiguous range of 4D Regge edge index tuples, written as scale-32 integer fold equalities ready for assembly into $m_2^{\mathrm{Num}} = 8 \cdot Z_{\mathrm{explicit}}$ over all $4096$ tuples.
background
Recognition Science gravity work includes an exact discrete identity for the midpoint $m^2$ transverse-traceless sector of 4D Regge calculus. The identity is certified by reducing contributions to integer tables at a fixed scale factor of 32, then discharging equalities with Lean's kernel decide (no native_decide).
The upstream kernel-certificate module supplies the shared fold and table infrastructure generated by scripts/qg/regge_4d_m2_kernel_certs_20260721.py. Individual chunks hold only a slice of the enumerated edge lemmas so that the library stays modular and checkable.
This chunk exposes the sibling family e_220000 through e_220023: named certificate lemmas for successive index tuples in that numbering band.
proof idea
Definition-and-certificate module, not a single prose theorem. Each edge lemma is a closed kernel goal: an Int fold over a scale-32 table equals the predicted midpoint contribution for that index tuple. Proofs are uniform decide discharges against the imported kernel-cert infrastructure; there is no analytic rewriting inside the chunk itself.
why it matters in Recognition Science
The downstream assemble module imports this chunk (with its siblings) to build $m_2^{\mathrm{Num}} = 8 \cdot Z_{\mathrm{explicit}}$ over the full $4096$ index tuples. Without every chunk's certificates, the global numerical identity cannot be closed in-kernel. In the gravity analysis stack this is bookkeeping infrastructure for the exact Regge midpoint TT identity, not a new physical law; it exists so the assembled identity is machine-checked rather than trusted from external numerics.
scope and limits
- Does not state the full 4096-tuple identity; only one numbered certificate slice.
- Does not prove continuum GR limits or continuum TT gauge fixing.
- Does not introduce new physical constants or RS forcing-chain steps (T0–T8).
- Does not use native_decide; certificates are kernel decide on integer tables only.
- Does not assemble m2Num; that is the downstream assemble module's job.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_220000 -
theorem
e_220001 -
theorem
e_220002 -
theorem
e_220003 -
theorem
e_220010 -
theorem
e_220011 -
theorem
e_220012 -
theorem
e_220013 -
theorem
e_220020 -
theorem
e_220021 -
theorem
e_220022 -
theorem
e_220023 -
theorem
e_220030 -
theorem
e_220031 -
theorem
e_220032 -
theorem
e_220033 -
theorem
e_220100 -
theorem
e_220101 -
theorem
e_220102 -
theorem
e_220103 -
theorem
e_220110 -
theorem
e_220111 -
theorem
e_220112 -
theorem
e_220113 -
theorem
e_220120 -
theorem
e_220121 -
theorem
e_220122 -
theorem
e_220123 -
theorem
e_220130 -
theorem
e_220131 -
theorem
e_220132 -
theorem
e_220133 -
theorem
e_220200 -
theorem
e_220201 -
theorem
e_220202 -
theorem
e_220203 -
theorem
e_220210 -
theorem
e_220211 -
theorem
e_220212 -
theorem
e_220213 -
theorem
e_220220 -
theorem
e_220221 -
theorem
e_220222 -
theorem
e_220223 -
theorem
e_220230 -
theorem
e_220231 -
theorem
e_220232 -
theorem
e_220233 -
theorem
e_220300 -
theorem
e_220301 -
theorem
e_220302 -
theorem
e_220303 -
theorem
e_220310 -
theorem
e_220311 -
theorem
e_220312 -
theorem
e_220313 -
theorem
e_220320 -
theorem
e_220321 -
theorem
e_220322 -
theorem
e_220323 -
theorem
e_220330 -
theorem
e_220331 -
theorem
e_220332 -
theorem
e_220333 -
theorem
e_221000 -
theorem
e_221001 -
theorem
e_221002 -
theorem
e_221003 -
theorem
e_221010 -
theorem
e_221011 -
theorem
e_221012 -
theorem
e_221013 -
theorem
e_221020 -
theorem
e_221021 -
theorem
e_221022 -
theorem
e_221023 -
theorem
e_221030 -
theorem
e_221031 -
theorem
e_221032 -
theorem
e_221033