IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk11
Chunk 11 of the generated midpoint m² TT identity certificates for 4D Regge calculus. It packages a block of kernel-decidable numerical identities (the e_2300xx family) used when assembling the global m2Num sum. Downstream assembly folds these chunks into m2Num = 8·explicitZ over all 4096 index tuples. Proofs are pure kernel decide on scale-32 integer tables, not analytic arguments.
claimA finite block of certified numerical identities for the 4D Regge midpoint $m^2$ transverse-traceless (TT) kernel: each entry asserts an exact integer relation on the scale-32 tables for a fixed multi-index in the chunk covering the $e_{2300xx}$ range, contributing to the global sum $m_2^{\mathrm{Num}} = 8\,Z_{\mathrm{explicit}}$ over all $4096$ index tuples.
background
In the Recognition Science gravity stack, 4D Regge calculus identities are checked by reducing the midpoint $m^2$ TT kernel to exact integer arithmetic on scale-32 tables. The upstream kernel-cert module supplies the decide-only infrastructure: Int List.foldl over those tables, with no native_decide, so every certificate is kernel-checkable.
This module is one generated chunk in that pipeline. Sibling names $e_{230000},\ldots,e_{230023}$ mark the local multi-index block. The theoretical setting is discrete gravity bookkeeping: verify that the numerical $m^2$ contribution matches the explicit closed form before the global assembly step.
No new continuum physics is introduced here; the chunk only materializes a slice of the finite verification table produced by the generator script regge_4d_m2_kernel_certs_20260721.py.
proof idea
Definition-and-certificate module, not an analytic proof. Each local lemma is a kernel decide on a precomputed integer identity from the scale-32 fold tables imported via the KernelCert module. Structure is uniform across the $e_{2300xx}$ family: unfold the table entry, run decide, done. No tactic search, no rewriting beyond what the generator baked in.
why it matters in Recognition Science
Feeds the assembler module that builds $m_2^{\mathrm{Num}} = 8\cdot Z_{\mathrm{explicit}}$ over all 4096 index tuples. Without every chunk discharging its block, the global midpoint $m^2$ TT identity cannot be closed in Lean. In the gravity analysis chain this is pure scaffolding for an exact discrete identity, not a continuum Einstein-equation derivation; it sits downstream of the kernel certs and upstream of the full numerical assembly used to underwrite the Regge midpoint claim.
scope and limits
- Does not prove the continuum TT gauge identity; only finite scale-32 integer certificates.
- Does not cover index tuples outside the e_2300xx chunk block.
- Does not introduce analytic bounds or error estimates beyond exact decide.
- Does not assemble the global m2Num sum; that is the downstream module.
- Does not depend on native_decide or external oracle evaluation.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_230000 -
theorem
e_230001 -
theorem
e_230002 -
theorem
e_230003 -
theorem
e_230010 -
theorem
e_230011 -
theorem
e_230012 -
theorem
e_230013 -
theorem
e_230020 -
theorem
e_230021 -
theorem
e_230022 -
theorem
e_230023 -
theorem
e_230030 -
theorem
e_230031 -
theorem
e_230032 -
theorem
e_230033 -
theorem
e_230100 -
theorem
e_230101 -
theorem
e_230102 -
theorem
e_230103 -
theorem
e_230110 -
theorem
e_230111 -
theorem
e_230112 -
theorem
e_230113 -
theorem
e_230120 -
theorem
e_230121 -
theorem
e_230122 -
theorem
e_230123 -
theorem
e_230130 -
theorem
e_230131 -
theorem
e_230132 -
theorem
e_230133 -
theorem
e_230200 -
theorem
e_230201 -
theorem
e_230202 -
theorem
e_230203 -
theorem
e_230210 -
theorem
e_230211 -
theorem
e_230212 -
theorem
e_230213 -
theorem
e_230220 -
theorem
e_230221 -
theorem
e_230222 -
theorem
e_230223 -
theorem
e_230230 -
theorem
e_230231 -
theorem
e_230232 -
theorem
e_230233 -
theorem
e_230300 -
theorem
e_230301 -
theorem
e_230302 -
theorem
e_230303 -
theorem
e_230310 -
theorem
e_230311 -
theorem
e_230312 -
theorem
e_230313 -
theorem
e_230320 -
theorem
e_230321 -
theorem
e_230322 -
theorem
e_230323 -
theorem
e_230330 -
theorem
e_230331 -
theorem
e_230332 -
theorem
e_230333 -
theorem
e_231000 -
theorem
e_231001 -
theorem
e_231002 -
theorem
e_231003 -
theorem
e_231010 -
theorem
e_231011 -
theorem
e_231012 -
theorem
e_231013 -
theorem
e_231020 -
theorem
e_231021 -
theorem
e_231022 -
theorem
e_231023 -
theorem
e_231030 -
theorem
e_231031 -
theorem
e_231032 -
theorem
e_231033