IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk14
Chunk 14 of the generated midpoint m² TT-identity certificates for 4D Regge calculus. It holds a contiguous block of kernel-decidable integer equalities (scale-32 foldl tables) used when assembling m2Num = 8·explicitZ over all 4096 index tuples. Gravity auditors of the exact discrete curvature identity cite it only inside that assembly chain. Content is pure certificate data: no analytic argument beyond kernel decide.
claimA finite block of certified integer equalities for the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus, evaluated on scale-32 kernel tables and closed by kernel decision on a contiguous subset of the $4096$ index tuples.
background
In the RS gravity analysis stack, the Regge exact midpoint $m^2$ TT identity is a discrete curvature identity on 4D triangulations. The imported kernel-certificate module supplies script-generated Int List.foldl tables at scale 32, proved with kernel decide only (no native_decide), from scripts/qg/regge_4d_m2_kernel_certs_20260721.py.
This file is one numbered chunk in the m2Num certificate stream. Sibling entries such as the $e_{320000}$–$e_{320023}$ block are individual certified equalities for successive index tuples. The full cover is $4096$ tuples; downstream assembly multiplies the explicit $Z$ contribution by 8 to obtain m2Num.
proof idea
Generated certificate module, not a hand proof. Each local entry is a one-shot kernel decide on a foldl evaluation against the imported scale-32 kernel tables. Structure is a flat list of kernel-closed integer identities for one contiguous index block; no lemmas beyond the kernel cert import and no tactic creativity.
why it matters in Recognition Science
Imported by the m2Num assemble module, whose doc-comment states the goal: assemble m2Num = 8·explicitZ over all 4096 index tuples. Every chunk must close or the global m2Num identity fails. The module is scaffolding in the discrete-gravity verification path that underwrites exact midpoint TT identities used later in RS gravity analysis; it does not itself state a physical law, only a certified arithmetic slice of one.
scope and limits
- Does not prove the full m2Num identity; only one index chunk.
- Does not add analytic lemmas; certificate data only.
- Does not use native_decide; kernel decide only.
- Does not treat continuum limits or unit conversion.
- Does not stand alone without the kernel-cert import and the assemble parent.
used by (1)
depends on (1)
declarations in this module (256)
-
theorem
e_320000 -
theorem
e_320001 -
theorem
e_320002 -
theorem
e_320003 -
theorem
e_320010 -
theorem
e_320011 -
theorem
e_320012 -
theorem
e_320013 -
theorem
e_320020 -
theorem
e_320021 -
theorem
e_320022 -
theorem
e_320023 -
theorem
e_320030 -
theorem
e_320031 -
theorem
e_320032 -
theorem
e_320033 -
theorem
e_320100 -
theorem
e_320101 -
theorem
e_320102 -
theorem
e_320103 -
theorem
e_320110 -
theorem
e_320111 -
theorem
e_320112 -
theorem
e_320113 -
theorem
e_320120 -
theorem
e_320121 -
theorem
e_320122 -
theorem
e_320123 -
theorem
e_320130 -
theorem
e_320131 -
theorem
e_320132 -
theorem
e_320133 -
theorem
e_320200 -
theorem
e_320201 -
theorem
e_320202 -
theorem
e_320203 -
theorem
e_320210 -
theorem
e_320211 -
theorem
e_320212 -
theorem
e_320213 -
theorem
e_320220 -
theorem
e_320221 -
theorem
e_320222 -
theorem
e_320223 -
theorem
e_320230 -
theorem
e_320231 -
theorem
e_320232 -
theorem
e_320233 -
theorem
e_320300 -
theorem
e_320301 -
theorem
e_320302 -
theorem
e_320303 -
theorem
e_320310 -
theorem
e_320311 -
theorem
e_320312 -
theorem
e_320313 -
theorem
e_320320 -
theorem
e_320321 -
theorem
e_320322 -
theorem
e_320323 -
theorem
e_320330 -
theorem
e_320331 -
theorem
e_320332 -
theorem
e_320333 -
theorem
e_321000 -
theorem
e_321001 -
theorem
e_321002 -
theorem
e_321003 -
theorem
e_321010 -
theorem
e_321011 -
theorem
e_321012 -
theorem
e_321013 -
theorem
e_321020 -
theorem
e_321021 -
theorem
e_321022 -
theorem
e_321023 -
theorem
e_321030 -
theorem
e_321031 -
theorem
e_321032 -
theorem
e_321033