Pith. sign in
module module high

IndisputableMonolith.Gravity.Analysis.ReggeExactMidpointM2TTIdentity4DM2NumChunk01

show as:
view Lean formalization →

Chunk 01 of the generated midpoint m² TT numerator tables for 4D Regge calculus. It holds a block of explicit integer certificate entries (e_010000–e_010023) used when assembling m2Num = 8·explicitZ over the full 4096 index tuples. Gravity analysts cite it only as a data slice feeding the assemble module. Content is script-generated fold/scale-32 tables discharged by kernel decide.

claimA finite block of explicit integer certificates $e_{010000},\ldots,e_{010023}$ for the midpoint $m^2$ transverse-traceless numerator identity in 4D Regge calculus, at scale 32, to be folded into $m_2^{\mathrm{Num}} = 8\cdot Z_{\mathrm{explicit}}$ over all $4096$ index tuples.

background

Recognition Science gravity analysis here works in discrete 4D Regge calculus. The midpoint $m^2$ transverse-traceless (TT) identity is an algebraic numerator identity on edge/hinge data; its exact form is certified by integer tables rather than symbolic expansion.

Upstream, ReggeExactMidpointM2TTIdentity4DKernelCert supplies the kernel certificates: script-generated (regge_4d_m2_kernel_certs_20260721.py) Int tables built by List.foldl at scale 32, proved only with kernel decide (no native_decide). This module is one numbered chunk of those tables.

The sibling names $e_{0100**}$ are the concrete certificate cells in this slice. Downstream assembly sums them into the global numerator $m_2^{\mathrm{Num}}$.

proof idea

Definition/data module, not a prose proof. Each $e_{0100ij}$ is an explicit integer (or small certified expression) produced by the generator script. Discharge is by kernel decide on the fold/scale-32 tables imported from the kernel-cert module. No tactic narrative beyond table lookup and decidable equality.

why it matters in Recognition Science

Feeds ReggeExactMidpointM2TTIdentity4DM2NumAssemble, whose doc-comment states the goal: assemble $m_2^{\mathrm{Num}} = 8\cdot Z_{\mathrm{explicit}}$ over all 4096 index tuples. Without the chunked tables, the assemble step has nothing to fold. The split into chunks keeps individual files small while preserving a fully kernel-checkable path for the 4D midpoint $m^2$ TT identity in the gravity analysis stack.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (256)

… and 176 more