IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk02
Chunk 02 of machine-generated kernel certificates for the exact midpoint m² transverse-traceless identity in 4D Regge calculus. Each lemma certifies one discrete index tuple via fold and scale-32 table lookup, discharged by kernel decide. Downstream assembly folds these chunks into m2Num = 8·explicitZ over all 4096 tuples. Cite when auditing the discrete gravity identity pipeline.
claimFor each certified multi-index $\iota$ in chunk 02 of the 4D midpoint $m^2$ TT table, the discrete kernel evaluation equals the predicted scale-32 integer entry, so the corresponding summand of $m^2_{\mathrm{Num}}$ is exact.
background
Recognition Science gravity work formalizes Regge calculus identities in Lean so continuum claims rest on finite, checkable discrete algebra. The midpoint $m^2$ transverse-traceless (TT) identity is one such target: a numerical relation among curvature and edge data on a 4D complex, evaluated at midpoints.
Upstream, ReggeExactMidpointM2TTIdentity4DKernelCert supplies generated kernel certificates: "Int List.foldl + scale-32 tables; kernel decide only (no native_decide)." This module is one numbered chunk of those certificates. Sibling names e_020000–e_020023 label individual index-tuple lemmas inside the chunk.
The ambient setting is exact discrete verification, not continuum approximation: every equality is an integer or rational identity closed by the Lean kernel.
proof idea
Definition-and-certificate module, not a single narrative proof. Each e_02**** lemma is a thin wrapper: evaluate the fold over the scale-32 kernel table at a fixed multi-index, then close the equality by decide. No analytic estimates; the argument is exhaustive finite checking of precomputed tables generated by scripts/qg/regge_4d_m2_kernel_certs_20260721.py. Chunking keeps individual files small while covering a contiguous block of the 4096-tuple space.
why it matters in Recognition Science
Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, whose doc-comment states the goal: "Assemble m2Num = 8·explicitZ over all 4096 index tuples." Without every chunk's certificates, the global numerical identity cannot be glued. In the broader RS gravity stack this is scaffolding for exact discrete control of the TT sector of the midpoint mass-squared identity, a prerequisite for claiming continuum limits without floating-point gaps. It does not itself state a continuum theorem; it closes one finite block of the kernel table that the assembler consumes.
scope and limits
- Does not prove the full 4096-tuple m2Num identity; only chunk 02 certificates.
- Does not address continuum or smooth limits of the Regge complex.
- Does not introduce new physics constants; only discrete kernel equalities.
- Does not use native_decide; relies solely on kernel decide over tables.
- Does not certify tuples outside the e_02**** index block.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_020000 -
theorem
e_020001 -
theorem
e_020002 -
theorem
e_020003 -
theorem
e_020010 -
theorem
e_020011 -
theorem
e_020012 -
theorem
e_020013 -
theorem
e_020020 -
theorem
e_020021 -
theorem
e_020022 -
theorem
e_020023 -
theorem
e_020030 -
theorem
e_020031 -
theorem
e_020032 -
theorem
e_020033 -
theorem
e_020100 -
theorem
e_020101 -
theorem
e_020102 -
theorem
e_020103 -
theorem
e_020110 -
theorem
e_020111 -
theorem
e_020112 -
theorem
e_020113 -
theorem
e_020120 -
theorem
e_020121 -
theorem
e_020122 -
theorem
e_020123 -
theorem
e_020130 -
theorem
e_020131 -
theorem
e_020132 -
theorem
e_020133 -
theorem
e_020200 -
theorem
e_020201 -
theorem
e_020202 -
theorem
e_020203 -
theorem
e_020210 -
theorem
e_020211 -
theorem
e_020212 -
theorem
e_020213 -
theorem
e_020220 -
theorem
e_020221 -
theorem
e_020222 -
theorem
e_020223 -
theorem
e_020230 -
theorem
e_020231 -
theorem
e_020232 -
theorem
e_020233 -
theorem
e_020300 -
theorem
e_020301 -
theorem
e_020302 -
theorem
e_020303 -
theorem
e_020310 -
theorem
e_020311 -
theorem
e_020312 -
theorem
e_020313 -
theorem
e_020320 -
theorem
e_020321 -
theorem
e_020322 -
theorem
e_020323 -
theorem
e_020330 -
theorem
e_020331 -
theorem
e_020332 -
theorem
e_020333 -
theorem
e_021000 -
theorem
e_021001 -
theorem
e_021002 -
theorem
e_021003 -
theorem
e_021010 -
theorem
e_021011 -
theorem
e_021012 -
theorem
e_021013 -
theorem
e_021020 -
theorem
e_021021 -
theorem
e_021022 -
theorem
e_021023 -
theorem
e_021030 -
theorem
e_021031 -
theorem
e_021032 -
theorem
e_021033