fermionicDOF
plain-language theorem explainer
The fermionic degrees of freedom count is defined as twice the integration gap at dimension D. Cosmologists deriving the exact rung for the baryon asymmetry eta_B cite this as the third combinatorial witness. It encodes matter-antimatter doubling on the parity-configuration product. The definition is a direct one-line abbreviation with no additional computation.
Claim. The fermionic degrees of freedom count equals twice the integration gap evaluated at spatial dimension $D$, where the integration gap is the product of parity count and configuration dimension.
background
The module derives the integer rung -44 for eta_B via three combinatorial witnesses at D=3. These witnesses reparameterize the same underlying integer D squared times (D plus 2) minus 1. The integration gap is defined upstream as the product of parity count and configuration dimension. This definition supplies the fermionic witness by doubling that gap to encode matter-antimatter doubling.
proof idea
The definition is a direct one-line abbreviation that doubles the value of the upstream integration gap at dimension D.
why it matters
This definition supplies the fermionic witness that feeds the certificate structure unifying the three routes to the -44 rung. It appears in the equality theorems verifying each witness and in the fermionic half-equals-gap result. The module documentation states these are distinct combinatorial reparameterizations of the same integer at D=3, not independent forcing routes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.