IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk04
Chunk 04 of the generated numerical certificates for the 4D Regge midpoint m² TT identity. It packages a block of kernel-certified edge values (the e_1000xx family) used when assembling the global m2Num sum. Downstream assembly folds these chunks with the scale-32 tables. The content is decide-only kernel data, not a hand proof.
claimA finite block of certified numerical edge contributions $e_{1000xx}$ entering the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus, to be summed as part of $m_2^{\mathrm{Num}} = 8 \cdot Z_{\mathrm{explicit}}$ over the full $4096$ index tuples.
background
Recognition Science gravity analysis here works in discrete Regge calculus in four dimensions. The midpoint $m^2$ TT identity is an algebraic relation on edge lengths and curvature defects that must hold exactly on the certified kernel before continuum limits or continuum matching are discussed.
Upstream, ReggeExactMidpointM2TTIdentity4DKernelCert supplies generated kernel certificates: Int List.foldl over scale-32 tables, discharged by decide only (no native_decide). Script source: scripts/qg/regge_4d_m2_kernel_certs_20260721.py.
This module is one numbered chunk of those certificates. Sibling names $e_{100000},\ldots,e_{100023}$ are the local certified edge entries in the chunk.
proof idea
Definition and certificate module, not a tactic proof. Values are precomputed kernel certificates imported from the upstream kernel-cert module and exposed as named edge constants. Discharge is by kernel decide on the fold/scale-32 tables; there is no analytic expansion inside this file.
why it matters in Recognition Science
Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, which assembles $m_2^{\mathrm{Num}} = 8\cdot Z_{\mathrm{explicit}}$ over all 4096 index tuples. Without the chunked edge certificates, the global numerical identity cannot be closed in Lean. Sits in the Gravity analysis path that checks exact discrete identities before continuum or phenomenological claims. Does not itself state a continuum Einstein or Newtonian limit.
scope and limits
- Does not prove the full 4096-tuple m2Num identity alone; only one certificate chunk.
- Does not supply continuum GR or Newtonian gravity limits.
- Does not use native_decide; certificates are kernel decide only.
- Does not define the assembly map; that lives in the Assemble module.
- Does not claim physical units or observational fits.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_100000 -
theorem
e_100001 -
theorem
e_100002 -
theorem
e_100003 -
theorem
e_100010 -
theorem
e_100011 -
theorem
e_100012 -
theorem
e_100013 -
theorem
e_100020 -
theorem
e_100021 -
theorem
e_100022 -
theorem
e_100023 -
theorem
e_100030 -
theorem
e_100031 -
theorem
e_100032 -
theorem
e_100033 -
theorem
e_100100 -
theorem
e_100101 -
theorem
e_100102 -
theorem
e_100103 -
theorem
e_100110 -
theorem
e_100111 -
theorem
e_100112 -
theorem
e_100113 -
theorem
e_100120 -
theorem
e_100121 -
theorem
e_100122 -
theorem
e_100123 -
theorem
e_100130 -
theorem
e_100131 -
theorem
e_100132 -
theorem
e_100133 -
theorem
e_100200 -
theorem
e_100201 -
theorem
e_100202 -
theorem
e_100203 -
theorem
e_100210 -
theorem
e_100211 -
theorem
e_100212 -
theorem
e_100213 -
theorem
e_100220 -
theorem
e_100221 -
theorem
e_100222 -
theorem
e_100223 -
theorem
e_100230 -
theorem
e_100231 -
theorem
e_100232 -
theorem
e_100233 -
theorem
e_100300 -
theorem
e_100301 -
theorem
e_100302 -
theorem
e_100303 -
theorem
e_100310 -
theorem
e_100311 -
theorem
e_100312 -
theorem
e_100313 -
theorem
e_100320 -
theorem
e_100321 -
theorem
e_100322 -
theorem
e_100323 -
theorem
e_100330 -
theorem
e_100331 -
theorem
e_100332 -
theorem
e_100333 -
theorem
e_101000 -
theorem
e_101001 -
theorem
e_101002 -
theorem
e_101003 -
theorem
e_101010 -
theorem
e_101011 -
theorem
e_101012 -
theorem
e_101013 -
theorem
e_101020 -
theorem
e_101021 -
theorem
e_101022 -
theorem
e_101023 -
theorem
e_101030 -
theorem
e_101031 -
theorem
e_101032 -
theorem
e_101033