IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk13
Chunk 13 of the generated midpoint m² TT-identity certificates for 4D Regge calculus. It holds a block of kernel-decidable numerical equalities (siblings e_310000–e_310023 and kin) used when assembling the global m2Num sum. Gravity analysts import it only as a leaf under the assemble module. Each entry is discharged by decide on scale-32 integer tables, with no analytic argument inside the chunk.
claimA finite block of certified numerical identities for the midpoint $m^2$ transverse-traceless (TT) sector in 4D Regge calculus, covering the chunk-13 index range. After clearing denominators by a factor of $32$, each identity is an equality of integers obtained from fold-accumulated kernel tables.
background
Recognition Science gravity work includes an exact midpoint identity for the $m^2$ TT sector of 4D Regge calculus. The identity is not proved by a single closed-form rewrite; it is certified over the full discrete index set by generated kernel tables.
The upstream kernel-cert module documents the generation path: script regge_4d_m2_kernel_certs_20260721.py, Int accumulation via List.foldl, scale-32 tables, and proofs that use only kernel decide (no native_decide). This chunk module is one slice of those certificates.
Naming e_310000, e_310001, … marks individual certified equalities inside the chunk. Downstream assembly treats the chunks as opaque imports and sums them into a global numerator.
proof idea
Definition-and-certificate module, not a prose proof. Each sibling is a closed proposition on a scaled integer identity; the proof is a one-shot kernel decide against the fold-built scale-32 table from the kernel-cert import. No lemmas beyond that infrastructure are invoked inside the chunk. The module argument is exhaustive case coverage of its index block, then re-export for assembly.
why it matters in Recognition Science
Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, whose doc-comment states the goal: assemble $m_2\mathrm{Num} = 8\cdot\mathrm{explicitZ}$ over all 4096 index tuples. Without every chunk, the global numerator identity cannot be stitched. In the gravity analysis stack this is bookkeeping infrastructure for the exact midpoint $m^2$ TT identity, not a new physical law. It sits under the broader Regge/exact-identity line rather than the T0–T8 forcing chain, and exists so the assemble module can remain a thin fold over certified blocks.
scope and limits
- Does not state or prove the global midpoint m² TT identity; only one index chunk.
- Does not derive continuum GR or Einstein equations from the certificates.
- Does not use native_decide; certificates are kernel decide on scaled integers only.
- Does not define m2Num or explicitZ; those live in the assemble layer.
- Does not cover index tuples outside the chunk-13 sibling range.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_310000 -
theorem
e_310001 -
theorem
e_310002 -
theorem
e_310003 -
theorem
e_310010 -
theorem
e_310011 -
theorem
e_310012 -
theorem
e_310013 -
theorem
e_310020 -
theorem
e_310021 -
theorem
e_310022 -
theorem
e_310023 -
theorem
e_310030 -
theorem
e_310031 -
theorem
e_310032 -
theorem
e_310033 -
theorem
e_310100 -
theorem
e_310101 -
theorem
e_310102 -
theorem
e_310103 -
theorem
e_310110 -
theorem
e_310111 -
theorem
e_310112 -
theorem
e_310113 -
theorem
e_310120 -
theorem
e_310121 -
theorem
e_310122 -
theorem
e_310123 -
theorem
e_310130 -
theorem
e_310131 -
theorem
e_310132 -
theorem
e_310133 -
theorem
e_310200 -
theorem
e_310201 -
theorem
e_310202 -
theorem
e_310203 -
theorem
e_310210 -
theorem
e_310211 -
theorem
e_310212 -
theorem
e_310213 -
theorem
e_310220 -
theorem
e_310221 -
theorem
e_310222 -
theorem
e_310223 -
theorem
e_310230 -
theorem
e_310231 -
theorem
e_310232 -
theorem
e_310233 -
theorem
e_310300 -
theorem
e_310301 -
theorem
e_310302 -
theorem
e_310303 -
theorem
e_310310 -
theorem
e_310311 -
theorem
e_310312 -
theorem
e_310313 -
theorem
e_310320 -
theorem
e_310321 -
theorem
e_310322 -
theorem
e_310323 -
theorem
e_310330 -
theorem
e_310331 -
theorem
e_310332 -
theorem
e_310333 -
theorem
e_311000 -
theorem
e_311001 -
theorem
e_311002 -
theorem
e_311003 -
theorem
e_311010 -
theorem
e_311011 -
theorem
e_311012 -
theorem
e_311013 -
theorem
e_311020 -
theorem
e_311021 -
theorem
e_311022 -
theorem
e_311023 -
theorem
e_311030 -
theorem
e_311031 -
theorem
e_311032 -
theorem
e_311033