fermionicDOF_eq
plain-language theorem explainer
The theorem establishes that fermionicDOF equals 90 at three spatial dimensions via matter-antimatter doubling of the integration gap. Researchers deriving the exact baryon-to-photon rung integer in Recognition Science cite this to close the fermionic combinatorial witness for -44. The term-mode proof unfolds the doubling definition and substitutes the precomputed gap value of 45 at D=3.
Claim. $2$ times the integration gap at dimension three equals 90, where the integration gap is the product of parity count and configuration dimension.
background
The module computes the integer rung -44 for the baryon-to-photon ratio using three combinatorial witnesses that all reduce to the same expression at D=3. The fermionic witness rests on the definition fermionicDOF := 2 * integrationGap D, with integrationGap d := parityCount d * configDim d and A := 1 the active edge count per tick. The upstream theorem integrationGap_at_D3 states that integrationGap D = 45, obtained by native_decide on the product at D=3. The module doc states that the three witnesses are distinct reparameterizations of D²(D+2)-1 = 44, not independent forcing routes.
proof idea
The term proof unfolds fermionicDOF to expose the doubling 2 * integrationGap D, then applies rw [integrationGap_at_D3] to replace the gap with 45. Arithmetic reduction yields 90. It depends on the native_decide computation inside integrationGap_at_D3 and standard definitional rewriting.
why it matters
This equality supplies the fermionic witness that feeds eta_B_rung_from_fermionic_eq (which proves the rung equals -44) and fermionic_half_equals_gap (which equates half the DOF count to the gap). It completes the third reparameterization of the integration gap at D=3 inside the forcing chain, consistent with T8 fixing D=3 and the eight-tick octave. The module doc notes the structural unification across the three combinatorial settings as the core content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.