module module moderate

`IndisputableMonolith.Unification.FermionDOFGapBridge`

Defines the bridge from forced spatial dimension D=3 and the eight-tick cadence to a fermion degrees-of-freedom gap used in unification bookkeeping. Introduces dimensionGap, dof per generation, n_generations = D, and total fermionic_dof as RS-native integers. Cosmology derivations that pin the baryon-to-photon rung cite this package. Content is mostly equalities and positivity facts wired to DimensionForcing and PhiForcing.

claimWith spatial dimension $D=3$ forced by T8 and eight-tick period $2^3$, the module sets a dimension gap at $D=3$, degrees of freedom per generation, $n_{\mathrm{gen}}=D$, and total fermionic DOF as the product structure used downstream for $\eta_B$ rung counting.

background

Recognition Science forces $D=3$ spatial dimensions (T8) and an eight-tick octave of period $2^3$ (T7). DimensionForcing packages the topological and ledger arguments that pin $D=3$; PhiForcing supplies the self-similar fixed point $\varphi$ underlying cost and rung arithmetic. RecognitionBandwidth ties holographic bounds, $k_R=\ln\varphi$ bit cost, ILG lags, and the 8-tick cadence into one bandwidth picture.

This module sits in Unification. It names $D$, eightTick, dimensionGap (with evaluation and positivity at $D=3$), dof_per_gen, n_generations with the identification $n_{\mathrm{gen}}=D$, and fermionic_dof. The intent is a thin integer bridge: fermion counting expressed through the same $D$ and tick structure already forced upstream, not a new dynamical mechanism.

Constants and Cost supply the RS-native units and $J$-cost background against which DOF gaps are later compared to recognition bandwidth.

proof idea

Definition-and-equality module rather than a deep proof development. $D$ is the T8-forced spatial dimension; eightTick is $2^3$ with a matching equality lemma. dimensionGap is evaluated at $D=3$ and shown positive. dof_per_gen and n_generations are introduced with n_generations_eq_D identifying generation count with $D$. fermionic_dof assembles the product count. Arguments are direct rewrites against DimensionForcing and the eight-tick definition, not analytic estimates.

why it matters in Recognition Science

Feeds IndisputableMonolith.Cosmology.EtaBExactRungDerivation, which "closes a long-standing item on the open-frontier register" by deriving the integer $-44$ that pins $\eta_B$ to its $\varphi$-rung from $D=3$ alone along three independent routes. Those routes need a clean fermion DOF and dimension-gap package tied to $D=3$ and the eight-tick structure; this module is that package.

In the forcing chain it sits after T7 (eight-tick) and T8 ($D=3$), and before cosmological rung arithmetic. It does not itself derive $\alpha$ or masses; it only standardizes the DOF gap integers so baryon asymmetry bookkeeping can cite one place.

scope and limits

Does not derive $D=3$; imports that fact from DimensionForcing/T8.
Does not compute $\eta_B$ or the integer $-44$; only supplies DOF gap inputs.
Does not prove generation structure from the Standard Model Lagrangian.
Does not address bosonic DOF, dark sectors, or continuum QFT anomalies.
Does not fix $\alpha$, masses, or $k_R$; those live in other modules.

used by (1)

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

IndisputableMonolith.Cosmology.EtaBExactRungDerivation module_import

depends on (6)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.BoltzmannConstant module_import
IndisputableMonolith.Cost module_import
IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.PhiForcing module_import
IndisputableMonolith.Unification.RecognitionBandwidth module_import

declarations in this module (45)

structure or L55
def D L98
def eightTick L101
theorem eightTick_eq L103
def dimensionGap L107
theorem dimensionGap_at_D3 L109
theorem dimensionGap_positive L111
def dof_per_gen L130
theorem dof_per_gen_eq L132
def n_generations L136
theorem n_generations_eq_D L138
def fermionic_dof L144
theorem fermionic_dof_eq L146
theorem fermionic_dof_eq_twice_gap L159
theorem fermionic_matter_antimatter_split L166
def fermi_dirac_weight_D L186
theorem fermi_dirac_weight_D3 L190
theorem fermi_dirac_from_eight_tick L197
theorem fermi_weight_in_D2 L206
theorem fermi_weight_in_D4 L210
def gluon_dof L219
theorem gluon_dof_eq L221
def ew_boson_dof L226
theorem ew_boson_dof_eq L228
def higgs_dof L231
theorem higgs_dof_eq L233
def bosonic_dof L236
theorem bosonic_dof_eq L238
theorem bosonic_dof_eq_poly L243
def g_star_D L261
theorem g_star_D3_eq L266
theorem g_star_D3_positive L271
theorem g_star_via_gap L276
theorem matter_phi45_complementarity L296
theorem rung_sum_equals_one L301
def identity_tick_count L320
def available_ticks_boson L321
def available_ticks_fermion L322
theorem fermion_missing_identity_tick L324
theorem fermi_weight_is_tick_fraction L332
theorem D2_evaluation L344
theorem D4_evaluation L351
theorem D2_prediction L356
theorem D4_prediction L361
theorem fermion_dof_gap_certificate L381