IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk00
First enumerated chunk of certified midpoint m² numerator contributions for the 4D Regge TT identity. Supplies a block of scale-32 integer table entries (the e_0000** family) that the assembler folds into m2Num = 8·explicitZ over all 4096 index tuples. Gravity analysts cite it only as raw certified data; the proofs are kernel decide on precomputed fold tables from the kernel-cert module.
claimChunk 00 of the certified integer tables for the midpoint $m^2$ numerator in the 4D Regge TT identity: a finite family of scale-32 entries $e_{0000**}$ that contribute to $m_2^{\mathrm{Num}} = 8\,Z_{\mathrm{explicit}}$ when assembled over the full $4096$ index tuples.
background
In the 4D Regge analysis, the midpoint $m^2$ TT identity is checked by reducing a large discrete sum to integer arithmetic on scale-32 tables. The kernel-cert module supplies those tables and proves the kernel predicates by decide only (no native_decide), generated from scripts/qg/regge_4d_m2_kernel_certs_20260721.py via Int List.foldl.
This module is the first data chunk in that pipeline. Its siblings are named entries $e_{000000},\ldots$ holding the certified numerator fragments for a contiguous block of index tuples. No new geometric definitions are introduced here; the ambient objects (midpoint $m^2$, TT projector, Regge edge lengths) live upstream in the Gravity.Analysis stack.
The assembly target is global: over all $4096 = 2^{12}$ index tuples one must obtain $m_2^{\mathrm{Num}} = 8\cdot Z_{\mathrm{explicit}}$. Chunking keeps individual files small enough for the kernel checker while preserving a pure, decidable certificate trail.
proof idea
Definition-and-certificate module, not a single theorem. Each $e_{******}$ entry is a concrete integer (or small integer list) drawn from the scale-32 kernel tables; correctness of the underlying kernel predicates is discharged upstream by decide on fold results. This chunk contributes no independent tactic proof beyond whatever thin wrappers re-export those decided facts. The real work is bookkeeping: partition the 4096-tuple range so the assembler can foldl chunk contributions into the global $m_2^{\mathrm{Num}}$ identity.
why it matters in Recognition Science
Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, whose job is to assemble $m_2^{\mathrm{Num}} = 8\cdot Z_{\mathrm{explicit}}$ over all 4096 index tuples. Without the chunked numerator tables, the global midpoint $m^2$ TT identity in 4D Regge calculus cannot be certified inside the kernel. The module is pure scaffolding data in the gravity analysis chain: it does not state a physical law, but it is a required link between the generated kernel certificates and the assembled numerator identity used by higher Regge exactness results.
scope and limits
- Does not state or prove the full 4D midpoint $m^2$ TT identity.
- Does not cover all 4096 index tuples; only chunk 00 of the numerator tables.
- Does not introduce geometric Regge or TT definitions; those live upstream.
- Does not use native_decide; relies on kernel decide from the cert module.
- Does not assemble $m_2^{\mathrm{Num}}$; assembly is downstream.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_000000 -
theorem
e_000001 -
theorem
e_000002 -
theorem
e_000003 -
theorem
e_000010 -
theorem
e_000011 -
theorem
e_000012 -
theorem
e_000013 -
theorem
e_000020 -
theorem
e_000021 -
theorem
e_000022 -
theorem
e_000023 -
theorem
e_000030 -
theorem
e_000031 -
theorem
e_000032 -
theorem
e_000033 -
theorem
e_000100 -
theorem
e_000101 -
theorem
e_000102 -
theorem
e_000103 -
theorem
e_000110 -
theorem
e_000111 -
theorem
e_000112 -
theorem
e_000113 -
theorem
e_000120 -
theorem
e_000121 -
theorem
e_000122 -
theorem
e_000123 -
theorem
e_000130 -
theorem
e_000131 -
theorem
e_000132 -
theorem
e_000133 -
theorem
e_000200 -
theorem
e_000201 -
theorem
e_000202 -
theorem
e_000203 -
theorem
e_000210 -
theorem
e_000211 -
theorem
e_000212 -
theorem
e_000213 -
theorem
e_000220 -
theorem
e_000221 -
theorem
e_000222 -
theorem
e_000223 -
theorem
e_000230 -
theorem
e_000231 -
theorem
e_000232 -
theorem
e_000233 -
theorem
e_000300 -
theorem
e_000301 -
theorem
e_000302 -
theorem
e_000303 -
theorem
e_000310 -
theorem
e_000311 -
theorem
e_000312 -
theorem
e_000313 -
theorem
e_000320 -
theorem
e_000321 -
theorem
e_000322 -
theorem
e_000323 -
theorem
e_000330 -
theorem
e_000331 -
theorem
e_000332 -
theorem
e_000333 -
theorem
e_001000 -
theorem
e_001001 -
theorem
e_001002 -
theorem
e_001003 -
theorem
e_001010 -
theorem
e_001011 -
theorem
e_001012 -
theorem
e_001013 -
theorem
e_001020 -
theorem
e_001021 -
theorem
e_001022 -
theorem
e_001023 -
theorem
e_001030 -
theorem
e_001031 -
theorem
e_001032 -
theorem
e_001033