IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk04
Chunk 04 of machine-checked numerical certificates for the 4D Regge midpoint m² transverse-traceless identity. It packages a block of scale-32 table entries (the e_1000xx family) that the kernel can decide without native evaluation. Gravity analysts assembling the global m2Num sum over the 4096 index tuples cite this chunk as one of the fold inputs.
claimA finite block of certified integer identities supporting the midpoint $m^2$ TT relation in 4D Regge calculus: each entry asserts equality of a scaled fold expression against a precomputed table value at scale $32$, for index labels in the $1000xx$ range of the $4096$-tuple enumeration.
background
Recognition Science gravity work formalizes discrete curvature via Regge calculus. The midpoint $m^2$ transverse-traceless (TT) identity is an algebraic constraint on edge lengths and deficit data that must hold exactly in 4D for the continuum limit to match the continuum TT projector.
Upstream, the kernel-certificate module supplies generated lemmas built by Int List.foldl over scale-32 tables; proofs are pure decide (no native_decide). This chunk is one slice of that table, imported only for the numerical side of the identity.
The sibling names e_100000–e_100023 are the concrete certificate atoms in this file. They are not physics postulates; they are finite integer equalities that discharge one segment of the global sum.
proof idea
Definition-and-certificate module, not a single theorem. Each local lemma is a one-shot kernel decide on a closed integer expression coming from the generated fold/table script. No analytic rewriting appears here; the argument structure is exhaustive case coverage of a fixed index block, delegated to the kernel after the upstream cert infrastructure has normalized the expressions.
why it matters in Recognition Science
The assemble module imports this chunk to build $m_2^{\mathrm{Num}} = 8\cdot\mathrm{explicit}Z$ over all $4096$ index tuples. Without the chunked certs, the global numerical identity cannot be closed inside Lean. In the broader RS gravity stack this is scaffolding for exact discrete TT control, not a continuum Einstein-equation derivation. It sits downstream of the kernel cert generator and upstream of the full midpoint $m^2$ TT assembly.
scope and limits
- Does not prove the continuum TT projector or Einstein equations.
- Does not cover all 4096 tuples; only the 1000xx index block.
- Does not use native_decide; relies on kernel decide of pre-scaled integers.
- Does not introduce new physical constants or RS forcing-chain steps.
- Does not assemble m2Num; that is the parent assemble module.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_100000 -
theorem
e_100001 -
theorem
e_100002 -
theorem
e_100003 -
theorem
e_100010 -
theorem
e_100011 -
theorem
e_100012 -
theorem
e_100013 -
theorem
e_100020 -
theorem
e_100021 -
theorem
e_100022 -
theorem
e_100023 -
theorem
e_100030 -
theorem
e_100031 -
theorem
e_100032 -
theorem
e_100033 -
theorem
e_100100 -
theorem
e_100101 -
theorem
e_100102 -
theorem
e_100103 -
theorem
e_100110 -
theorem
e_100111 -
theorem
e_100112 -
theorem
e_100113 -
theorem
e_100120 -
theorem
e_100121 -
theorem
e_100122 -
theorem
e_100123 -
theorem
e_100130 -
theorem
e_100131 -
theorem
e_100132 -
theorem
e_100133 -
theorem
e_100200 -
theorem
e_100201 -
theorem
e_100202 -
theorem
e_100203 -
theorem
e_100210 -
theorem
e_100211 -
theorem
e_100212 -
theorem
e_100213 -
theorem
e_100220 -
theorem
e_100221 -
theorem
e_100222 -
theorem
e_100223 -
theorem
e_100230 -
theorem
e_100231 -
theorem
e_100232 -
theorem
e_100233 -
theorem
e_100300 -
theorem
e_100301 -
theorem
e_100302 -
theorem
e_100303 -
theorem
e_100310 -
theorem
e_100311 -
theorem
e_100312 -
theorem
e_100313 -
theorem
e_100320 -
theorem
e_100321 -
theorem
e_100322 -
theorem
e_100323 -
theorem
e_100330 -
theorem
e_100331 -
theorem
e_100332 -
theorem
e_100333 -
theorem
e_101000 -
theorem
e_101001 -
theorem
e_101002 -
theorem
e_101003 -
theorem
e_101010 -
theorem
e_101011 -
theorem
e_101012 -
theorem
e_101013 -
theorem
e_101020 -
theorem
e_101021 -
theorem
e_101022 -
theorem
e_101023 -
theorem
e_101030 -
theorem
e_101031 -
theorem
e_101032 -
theorem
e_101033