IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk07
Chunk 07 of the generated midpoint m² TT numerator certificates for 4D Regge calculus. It packages a fixed block of scale-32 integer table entries (e_130000–e_130023) that the kernel can decide without native evaluation. Downstream assembly folds these chunks into the global m2Num identity over all 4096 index tuples. Citation target for anyone auditing the exact discrete TT numerator.
claimA finite block of certified integer table entries $e_{130000},\ldots,e_{130023}$ contributing to the midpoint $m^2$ transverse-traceless numerator identity in 4D Regge calculus, at scale factor 32, for use in the global sum $m_2^{\mathrm{Num}}=8\cdot Z_{\mathrm{explicit}}$ over the $4096$ index tuples.
background
Recognition Science gravity work formalizes discrete Regge identities so that continuum limits and continuum constants sit on machine-checkable algebra rather than floating-point numerics. The midpoint $m^2$ TT identity is one such exact discrete relation in 4D.
Upstream, the kernel-certificate module supplies generated lemmas built by scripts/qg/regge_4d_m2_kernel_certs_20260721.py: integer List.foldl reductions against scale-32 tables, discharged by decide only (no native_decide). This chunk is one contiguous slice of that table, named by the $e_{13xxxx}$ family.
The local setting is pure certificate packaging: no new physics axioms, only finite integer equalities the kernel can re-check.
proof idea
Definition and certificate module, not a discursive proof. Each sibling e_13xxxx is a closed integer identity (or a thin wrapper around one) produced by the generator script and re-verified with kernel decide on fold results over the scale-32 tables. The module simply groups a contiguous index block so the assembler can import chunks without loading the full 4096-tuple table at once. No tactic narrative beyond that batch of decidable equalities.
why it matters in Recognition Science
Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, whose doc-comment states the goal: assemble $m_2^{\mathrm{Num}}=8\cdot Z_{\mathrm{explicit}}$ over all 4096 index tuples. Without the chunked certificates, that global numerator identity cannot be closed inside Lean’s kernel budget.
In the broader gravity stack this is scaffolding for exact discrete TT projections used when matching Regge curvature data to continuum limits and RS unit conventions. It does not itself force $D=3$ or the eight-tick structure; it is a numerical-algebraic brick those continuum arguments rely on once the discrete identity is sealed.
scope and limits
- Does not prove the full 4096-tuple m2Num identity; only one index chunk.
- Does not introduce continuum gravity, Einstein equations, or RS forcing T0–T8.
- Does not use native_decide; certificates are kernel-decide only.
- Does not define the geometric meaning of the TT projector; only integer table facts.
- Does not claim completeness of other chunks; assembly is downstream.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_130000 -
theorem
e_130001 -
theorem
e_130002 -
theorem
e_130003 -
theorem
e_130010 -
theorem
e_130011 -
theorem
e_130012 -
theorem
e_130013 -
theorem
e_130020 -
theorem
e_130021 -
theorem
e_130022 -
theorem
e_130023 -
theorem
e_130030 -
theorem
e_130031 -
theorem
e_130032 -
theorem
e_130033 -
theorem
e_130100 -
theorem
e_130101 -
theorem
e_130102 -
theorem
e_130103 -
theorem
e_130110 -
theorem
e_130111 -
theorem
e_130112 -
theorem
e_130113 -
theorem
e_130120 -
theorem
e_130121 -
theorem
e_130122 -
theorem
e_130123 -
theorem
e_130130 -
theorem
e_130131 -
theorem
e_130132 -
theorem
e_130133 -
theorem
e_130200 -
theorem
e_130201 -
theorem
e_130202 -
theorem
e_130203 -
theorem
e_130210 -
theorem
e_130211 -
theorem
e_130212 -
theorem
e_130213 -
theorem
e_130220 -
theorem
e_130221 -
theorem
e_130222 -
theorem
e_130223 -
theorem
e_130230 -
theorem
e_130231 -
theorem
e_130232 -
theorem
e_130233 -
theorem
e_130300 -
theorem
e_130301 -
theorem
e_130302 -
theorem
e_130303 -
theorem
e_130310 -
theorem
e_130311 -
theorem
e_130312 -
theorem
e_130313 -
theorem
e_130320 -
theorem
e_130321 -
theorem
e_130322 -
theorem
e_130323 -
theorem
e_130330 -
theorem
e_130331 -
theorem
e_130332 -
theorem
e_130333 -
theorem
e_131000 -
theorem
e_131001 -
theorem
e_131002 -
theorem
e_131003 -
theorem
e_131010 -
theorem
e_131011 -
theorem
e_131012 -
theorem
e_131013 -
theorem
e_131020 -
theorem
e_131021 -
theorem
e_131022 -
theorem
e_131023 -
theorem
e_131030 -
theorem
e_131031 -
theorem
e_131032 -
theorem
e_131033