fermionic_half_equals_gap
plain-language theorem explainer
The theorem establishes that half the fermionic degrees of freedom equals the integration gap at D=3, giving the numerical identity 45=45. Cosmologists deriving the exact φ-rung for the baryon-to-photon ratio η_B cite this as the fermionic combinatorial witness among three reparameterizations of the integer 44. The proof is a short tactic sequence that unfolds the doubling definition, substitutes the known gap value 45, and decides the resulting equality.
Claim. At spatial dimension $D=3$, half the fermionic degrees of freedom equals the integration gap: $45=45$, where fermionic degrees of freedom arise from matter-antimatter doubling of the parity-configuration product that defines the gap.
background
The module derives the integer rung −44 for η_B via three combinatorial witnesses, all reducing to integrationGap(D)−1=44 at D=3. The integration gap is defined as parityCount(d) times configDim(d). FermionicDOF is the matter-antimatter doubling of that gap value. Upstream results establish integrationGap_at_D3 as the concrete value 45 at three dimensions and fermionicDOF_eq as the doubling that yields 90. The local setting treats the three witnesses (dimension gap, chirality-torsion, fermionic doubling) as distinct reparameterizations of the same underlying integer rather than independent routes.
proof idea
The proof first rewrites using fermionicDOF_eq to obtain the concrete count 90. It then applies integrationGap_at_D3 to replace the gap with its known value 45 at D=3. The final decide tactic confirms the integer equality 45=45.
why it matters
This supplies the fermionic witness inside etaBExactRungCert, the certification theorem that all three witnesses agree on the rung −44. It realizes the fermionic-DOF doubling route described in the module documentation and connects the integration gap from Foundation.IntegrationGap to the cosmology of baryon asymmetry. Within the framework it instantiates the D=3 case of the eight-tick octave at T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.