Cosmology Eta Bexact Rung Derivation Eta B Rung From Fermionic Eq

The fermionic route to -44

The baryon-to-photon ratio, often written η_B, is a cosmological number that describes the slight surplus of matter over antimatter left over from the early universe. In the Recognition Science framework, this ratio is pinned to a specific power of the golden ratio, φ^(-44). The declaration eta_B_rung_from_fermionic_eq is a machine-checked proof that this exponent, -44, can be derived by counting the degrees of freedom in the Standard Model's fermionic sector.

The derivation starts with a simple count. The framework models a ledger, a discrete record of recognition events, and the Standard Model's fermionic fields contribute 90 such degrees of freedom. Halving this number, to account for the matter-antimatter doubling, gives 45. The proof then subtracts this from a single active edge, A = 1, yielding 1 - 45 = -44. The theorem states this equality formally: eta_B_rung_from_fermionic = -44.

This fermionic route is one of three independent structural paths that all converge on the same integer. Another route derives -44 from the product of a bit-flip count and a torsion gap (4 × 11), and a third from the number of dimensions (D = 3). The framework's library contains proofs that these routes agree, forming a convergence theorem. The key point is that none of these routes use η_B = φ^(-44) as an input; the agreement is presented as a non-trivial structural result, not a fit.

What this declaration does not claim is that it measures the actual cosmological baryon-to-photon ratio. The value -44 is a structural rung within the framework, and the connection to the measured η_B is an empirical check, not a theorem. The framework itself is falsifiable at the level of its named structural inputs, such as the fermionic degree count of 90. The proof establishes an internal consistency, not a direct observation of the universe's matter content.

/-- The fermionic DOF route yields −44. -/
theorem eta_B_rung_from_fermionic_eq : eta_B_rung_from_fermionic = -44 := by
  unfold eta_B_rung_from_fermionic
  have hferm : fermionic_dof = 90 := fermionic_dof_eq
  rw [hferm]
  decide

/-- The fermionic-DOF half equals the consciousness gap. This identity
    is the bridge: matter and antimatter each carry one full
    consciousness-gap worth of fermions, so dividing by 2 recovers the
    gap. -/
theorem fermionic_half_equals_gap :
    ((fermionic_dof / 2 : ℕ) : ℤ)
      = (Foundation.GapDerivation.consciousnessGap Foundation.GapDerivation.D : ℤ) := by
  have hferm : fermionic_dof = 90 := fermionic_dof_eq
  have hgap : (Foundation.GapDerivation.consciousnessGap Foundation.GapDerivation.D : ℤ) = 45 := by
    exact_mod_cast Foundation.GapDerivation.gap_at_D3
  rw [hferm, hgap]
  decide

/-- **CONVERGENCE THEOREM A=C**: The gap-from-dimension and fermionic
    DOF routes agree at D = 3. -/
theorem routes_AC_agree :
    eta_B_rung_from_dimension Foundation.GapDerivation.D = eta_B_rung_from_fermionic := by
  rw [eta_B_rung_from_dimension_at_D3, eta_B_rung_from_fermionic_eq]

What this page does not claim

This does not claim to measure the actual cosmological baryon-to-photon ratio. The derivation does not use the measured η_B as an input. The convergence theorem does not claim statistical independence of the three routes.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: