Pith. sign in
module module moderate

IndisputableMonolith.Foundation.GapDerivation

show as:
view Lean formalization →

Derives the Recognition dimension gap from spatial dimension D = 3 (forced by T8), via configuration dimension and the nine ledger parities. Cosmology authors cite it when pinning the integer gap that enters the φ-ladder mass and η_B rung formulas. The module is mostly definitional equalities plus short algebraic identities at D = 3 (parity count, LCM factorization).

claimWith spatial dimension $D = 3$ (T8), the configuration dimension, the count of independent $\mathbb{Z}_2$ ledger parities, and the dimension gap are fixed; at $D = 3$ one has $\mathrm{gap} = \mathrm{lcm}$-factorization identities linking parity count to the dual-route configuration count.

background

Recognition Science forces spatial dimension by the T8 step of the unified forcing chain: $D = 3$. This module works in that fixed dimension. It imports the RS constants layer and the Nine Parities formalization of the double-entry ledger under tick reversal and conjugation: the nine independent $\mathbb{Z}2$ labels ${P{cp}, P_{B-L}, P_Y, P_T, P_C^{(1)}, P_C^{(2)}, P_C^{(3)}, P_\tau^{(1)}, P_\tau^{(2)}}$.

The local objects are spatial dimension $D$, a configuration dimension built from $D$, a parity count drawn from that nine-parity set, and the dimension gap obtained from them. Several named equalities specialize these quantities at $D = 3$ and record that the parity count matches an explicit enumeration and that the gap factors as an LCM.

proof idea

Definition module with short algebraic specializations, not a deep proof development. $D$ is introduced as the T8 spatial dimension. Configuration dimension, parity count, and dimension gap are defined from $D$ and the nine-parity data. Lemmas then evaluate at $D = 3$: configuration dimension and parity count specialize, a dual-route identity and $3D = D^2$ style relation are recorded, parity count is checked against the enumeration, and the gap at $D = 3$ is factored and identified with an LCM form.

why it matters in Recognition Science

Supplies the integer gap structure that cosmology modules import when deriving baryon asymmetry rungs from $D = 3$ alone. Downstream, EtaBExactRungDerivation closes the open-frontier item of deriving the integer $-44$ that pins $\eta_B$ to its $\varphi$-rung by three independent routes from $D = 3$; those routes need the gap and parity-count identities packaged here. EtaBPrefactorDerivation likewise imports the module while treating the order-one prefactor as a selected ansatz rather than a derivation. In the broader framework this sits under T8 ($D = 3$) and feeds the mass-ladder gap term $\mathrm{gap}(Z)$ used on the $\varphi$-ladder.

scope and limits

used by (2)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (23)