IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk15
Chunk 15 of the generated midpoint $m^2$ transverse-traceless identity certificates in 4D Regge analysis. It holds a block of kernel-decided equalities (the $e_{3300xx}$ family) used when assembling $m_2^{\mathrm{Num}}=8\cdot Z$ over all 4096 index tuples. Anyone auditing the numerical half of the exact midpoint identity cites this chunk. Each entry is discharged by kernel `decide` on scale-32 integer fold tables, with no `native_decide`.
claimA finite block of certified equalities for a designated slice of the 4096 four-index tuples in the 4D Regge midpoint $m^2$ TT identity, each equating the corresponding numerator contribution to $8\cdot Z$ at scale 32.
background
In the 4D Regge sector of the gravity analysis, the midpoint $m^2$ transverse-traceless (TT) identity is checked by reducing both sides to integer tables at a fixed scale (here scale 32) and comparing them by pure kernel decision. The full check runs over $4096=2^{12}$ index tuples; those tuples are partitioned into generated chunks so that each file stays small and kernel-friendly.
Upstream, the kernel-certificate module supplies the shared fold and table infrastructure: Int List.foldl accumulators and scale-32 lookup data, with every atomic comparison proved by decide only (explicitly no native_decide). This chunk imports that kernel layer and exposes a consecutive family of named equalities $e_{330000},\ldots$ for its assigned index window.
The local setting is therefore purely algebraic bookkeeping inside discrete Regge calculus: no continuum limit, no floating-point arithmetic, and no physical units beyond the dimensionless integer tables.
proof idea
This is a generated certificate module, not a hand-written argument. A Python script (regge_4d_m2_kernel_certs_20260721.py) emits one lemma per index tuple in the chunk; each lemma body is a kernel decide on the precomputed scale-32 fold tables from the upstream kernel-cert module. There is no tactic search beyond decide, and no analytic identity is re-derived here.
why it matters in Recognition Science
The downstream assemble module imports every chunk and glues them into the global statement $m_2^{\mathrm{Num}}=8\cdot\mathrm{explicit}Z$ over all 4096 tuples. Without this chunk, that assembly has a hole in its index cover and the exact midpoint $m^2$ TT identity cannot be closed in Lean. In the broader Recognition gravity stack, the identity is a discrete consistency check on the Regge side of the curvature bookkeeping; it does not itself force $D=3$ or the eight-tick octave, but it is part of the certified discrete geometry layer those continuum claims sit on.
scope and limits
- Does not prove the identity outside the assigned index window of chunk 15.
- Does not address continuum Regge calculus or smooth TT gauge fixing.
- Does not use or justify floating-point numerics; only scale-32 integer tables.
- Does not assemble the global $m_2^{\mathrm{Num}}=8\cdot Z$ statement (that is the parent module).
- Does not discharge physical units, coupling constants, or phi-ladder mass formulae.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_330000 -
theorem
e_330001 -
theorem
e_330002 -
theorem
e_330003 -
theorem
e_330010 -
theorem
e_330011 -
theorem
e_330012 -
theorem
e_330013 -
theorem
e_330020 -
theorem
e_330021 -
theorem
e_330022 -
theorem
e_330023 -
theorem
e_330030 -
theorem
e_330031 -
theorem
e_330032 -
theorem
e_330033 -
theorem
e_330100 -
theorem
e_330101 -
theorem
e_330102 -
theorem
e_330103 -
theorem
e_330110 -
theorem
e_330111 -
theorem
e_330112 -
theorem
e_330113 -
theorem
e_330120 -
theorem
e_330121 -
theorem
e_330122 -
theorem
e_330123 -
theorem
e_330130 -
theorem
e_330131 -
theorem
e_330132 -
theorem
e_330133 -
theorem
e_330200 -
theorem
e_330201 -
theorem
e_330202 -
theorem
e_330203 -
theorem
e_330210 -
theorem
e_330211 -
theorem
e_330212 -
theorem
e_330213 -
theorem
e_330220 -
theorem
e_330221 -
theorem
e_330222 -
theorem
e_330223 -
theorem
e_330230 -
theorem
e_330231 -
theorem
e_330232 -
theorem
e_330233 -
theorem
e_330300 -
theorem
e_330301 -
theorem
e_330302 -
theorem
e_330303 -
theorem
e_330310 -
theorem
e_330311 -
theorem
e_330312 -
theorem
e_330313 -
theorem
e_330320 -
theorem
e_330321 -
theorem
e_330322 -
theorem
e_330323 -
theorem
e_330330 -
theorem
e_330331 -
theorem
e_330332 -
theorem
e_330333 -
theorem
e_331000 -
theorem
e_331001 -
theorem
e_331002 -
theorem
e_331003 -
theorem
e_331010 -
theorem
e_331011 -
theorem
e_331012 -
theorem
e_331013 -
theorem
e_331020 -
theorem
e_331021 -
theorem
e_331022 -
theorem
e_331023 -
theorem
e_331030 -
theorem
e_331031 -
theorem
e_331032 -
theorem
e_331033