eta_B_rung_from_fermionic_eq
The fermionic degrees-of-freedom witness for the baryon-to-photon ratio rung equals −44 at three spatial dimensions. Researchers deriving η_B within Recognition Science cite this as the third of three equivalent combinatorial expressions for the integer that fixes the φ-rung. The proof is a term reduction that unfolds the witness definition, substitutes fermionicDOF = 90, and decides the arithmetic.
claimThe fermionic-DOF doubling witness for the η_B rung, defined as $1 - (fermionicDOF / 2)$, equals $-44$ at $D = 3$, where $fermionicDOF = 90$.
background
The module presents three combinatorial reparameterizations of the integer $D^2(D+2)-1=44$ at $D=3$ that fix the φ-rung of η_B. The fermionic witness arises from matter-antimatter doubling of the integration gap, so $fermionicDOF = 2 × integrationGap(D)$ and the witness is $1 - fermionicDOF/2$. Upstream, eta_B_rung_from_fermionic is defined as $A - fermionicDOF/2$ with $A=1$, and fermionicDOF_eq asserts $fermionicDOF=90$ by reduction to integrationGap_at_D3. The local setting unifies this route with the gap-from-dimension and chirality-torsion witnesses as distinct expressions of the same integer.
proof idea
The term proof unfolds eta_B_rung_from_fermionic, rewrites via the lemma fermionicDOF_eq to insert the value 90, and applies decide to confirm the arithmetic yields −44.
why it matters in Recognition Science
This theorem supplies witness C inside etaBExactRungCert, the certificate that assembles the three witnesses together with their pairwise agreement theorems. It completes the fermionic-DOF doubling reparameterization of the integer 44 arising from $D^2(D+2)-1$ at $D=3$, consistent with the forced spatial dimension in the UnifiedForcingChain. The result closes one path in the combinatorial unification for the η_B rung using only the kernel.
scope and limits
- Does not claim the three witnesses are statistically independent.
- Does not derive fermionicDOF from first principles beyond integrationGap_at_D3.
- Does not extend the identity to dimensions other than D=3.
- Does not supply dynamical equations for the rung placement.
formal statement (Lean)
80theorem eta_B_rung_from_fermionic_eq : eta_B_rung_from_fermionic = -44 := by
proof body
Term-mode proof.
81 unfold eta_B_rung_from_fermionic
82 rw [fermionicDOF_eq]
83 decide
84
85/-! ## Convergence of the three witnesses -/
86
87/-- The gap-from-dimension and chirality × torsion witnesses agree at `D = 3`. -/