IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk03
Chunk 03 of machine-checked elementary certificates for the 4D Regge midpoint m² TT identity. Each entry is a kernel-decidable equality on scaled integer tables for a fixed index block. Gravity analysts assembling the global m2Num sum cite this chunk; the parent assembler folds it with the other chunks over all 4096 tuples. Proofs are pure `decide` on foldl-built tables, no native evaluation.
claimFor each multi-index $\iota$ in the chunk-03 block of $\{0,\ldots,4095\}$, the scaled integer kernel identity $e_{03\iota}$ asserts that the midpoint $m^2$ TT contribution at $\iota$ equals the corresponding explicit $Z$-table entry (scale factor 32), as required by the 4D Regge midpoint formula.
background
Recognition Science gravity work formalizes Regge calculus identities that relate discrete curvature (deficit angles) to mass-squared and transverse-traceless (TT) projections on a 4D simplicial complex. The midpoint $m^2$ TT identity is one such algebraic relation: after clearing denominators it becomes an equality of integer polynomials evaluable by table lookup.
The upstream kernel-cert module supplies the shared infrastructure: Int tables built by List.foldl, a uniform scale-32 normalization, and a decide-only certificate pattern (no native_decide). This chunk instantiates that pattern for one contiguous block of the 4096 index tuples that label the discrete degrees of freedom.
Sibling declarations e_030000–e_030023 (and the rest of the block) are the individual certificates; each is a closed Prop proved by kernel decision on the precomputed tables.
proof idea
Definition-and-certificate module, not a single theorem. Each e_03**** is a one-line kernel certificate: the goal is an equality of integer expressions built from the shared scale-32 foldl tables; decide discharges it inside the Lean kernel. No tactic automation beyond that, no analytic estimates, and no floating-point. The chunk exists solely to keep individual file sizes and elaboration times manageable while covering its slice of the 4096-tuple space.
why it matters in Recognition Science
The downstream assembler ReggeExactMidpointM2TTIdentity4DM2NumAssemble imports every chunk and builds the global identity $m_2\mathrm{Num}=8\cdot\mathrm{explicit}Z$ by summing the elementary contributions over all 4096 index tuples. Without chunk 03 that sum has a hole; with it, the numerical side of the midpoint $m^2$ TT identity is fully certified.
In the broader RS gravity stack this closes a generated, machine-checked step toward exact discrete Einstein identities on the recognition complex, complementary to the continuum forcing chain (T0–T8) and the continuum constants $c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$. It is pure scaffolding for the assembled theorem, not a physical claim on its own.
scope and limits
- Does not prove the full 4096-tuple m2Num identity; only the chunk-03 block.
- Does not address continuum limits, curvature convergence, or physical units.
- Does not use native_decide or floating-point; certificates are kernel Int equalities only.
- Does not define the midpoint m² TT formula itself; that lives in upstream kernel infrastructure.
- Does not claim uniqueness or minimality of the scale-32 table representation.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_030000 -
theorem
e_030001 -
theorem
e_030002 -
theorem
e_030003 -
theorem
e_030010 -
theorem
e_030011 -
theorem
e_030012 -
theorem
e_030013 -
theorem
e_030020 -
theorem
e_030021 -
theorem
e_030022 -
theorem
e_030023 -
theorem
e_030030 -
theorem
e_030031 -
theorem
e_030032 -
theorem
e_030033 -
theorem
e_030100 -
theorem
e_030101 -
theorem
e_030102 -
theorem
e_030103 -
theorem
e_030110 -
theorem
e_030111 -
theorem
e_030112 -
theorem
e_030113 -
theorem
e_030120 -
theorem
e_030121 -
theorem
e_030122 -
theorem
e_030123 -
theorem
e_030130 -
theorem
e_030131 -
theorem
e_030132 -
theorem
e_030133 -
theorem
e_030200 -
theorem
e_030201 -
theorem
e_030202 -
theorem
e_030203 -
theorem
e_030210 -
theorem
e_030211 -
theorem
e_030212 -
theorem
e_030213 -
theorem
e_030220 -
theorem
e_030221 -
theorem
e_030222 -
theorem
e_030223 -
theorem
e_030230 -
theorem
e_030231 -
theorem
e_030232 -
theorem
e_030233 -
theorem
e_030300 -
theorem
e_030301 -
theorem
e_030302 -
theorem
e_030303 -
theorem
e_030310 -
theorem
e_030311 -
theorem
e_030312 -
theorem
e_030313 -
theorem
e_030320 -
theorem
e_030321 -
theorem
e_030322 -
theorem
e_030323 -
theorem
e_030330 -
theorem
e_030331 -
theorem
e_030332 -
theorem
e_030333 -
theorem
e_031000 -
theorem
e_031001 -
theorem
e_031002 -
theorem
e_031003 -
theorem
e_031010 -
theorem
e_031011 -
theorem
e_031012 -
theorem
e_031013 -
theorem
e_031020 -
theorem
e_031021 -
theorem
e_031022 -
theorem
e_031023 -
theorem
e_031030 -
theorem
e_031031 -
theorem
e_031032 -
theorem
e_031033