Cosmology Eta Bexact Rung Derivation Eta B Rung From Dimension At D3

The rung from dimension

The baryon-to-photon ratio, written η_B, is a number cosmologists measure by counting ordinary matter and light in the sky. In the Recognition Science framework, this ratio is not a free parameter. It is pinned to a power of the golden ratio, and the exponent is the integer −44. The declaration eta_B_rung_from_dimension_at_D3 proves that this exponent follows from the dimensionality of space alone, without any input from the measured value of η_B.

The proof works through a ledger, a discrete record of recognition events. At dimension D, the framework counts D² independent ledger parities and D+2 degrees of freedom (D spatial, one temporal, one ledger balance). Their product is the consciousness gap, a count of structural possibilities: for D=3, that is 3² × 5 = 45. The rung is then one minus this gap, written as the formula 1 − D²(D+2). At D=3, this gives 1 − 45 = −44.

The declaration is part of a convergence theorem: three independent routes all land on −44. A second route multiplies a chirality flip count (4) by a torsion gap (11) to get 44, negated. A third route takes the Standard Model's 90 fermionic degrees of freedom, halves them (the matter-antimatter doubling), subtracts from one, and again reaches −44. The machine-checked library of formal theorems proves all three agree exactly.

The result is conditional on the framework's structural inputs. It is not a measurement of η_B, and it does not derive the fine-structure constant. It does, however, offer a concrete prediction: if the framework's identification of these structural counts is correct, then the exponent −44 is forced, and any measured deviation from the corresponding η_B value would falsify that identification.

/-- At D = 3, the gap-from-dimension route yields −44. -/
theorem eta_B_rung_from_dimension_at_D3 :
    eta_B_rung_from_dimension Foundation.GapDerivation.D = -44 := by
  unfold eta_B_rung_from_dimension
  have hgap : (Foundation.GapDerivation.consciousnessGap Foundation.GapDerivation.D : ℤ) = 45 := by
    exact_mod_cast Foundation.GapDerivation.gap_at_D3
  rw [hgap]
  decide

/-- **CONVERGENCE THEOREM A=B**: The gap-from-dimension and chirality
    routes agree at D = 3. -/
theorem routes_AB_agree :
    eta_B_rung_from_dimension Foundation.GapDerivation.D = eta_B_rung_from_chirality := by
  rw [eta_B_rung_from_dimension_at_D3, eta_B_rung_from_chirality_eq]

/-- **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]

/-- **CONVERGENCE THEOREM B=C**: The chirality and fermionic DOF routes
    agree at D = 3. -/
theorem routes_BC_agree :
    eta_B_rung_from_chirality = eta_B_rung_from_fermionic := by
  rw [eta_B_rung_from_chirality_eq, eta_B_rung_from_fermionic_eq]

/-- 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

What this page does not claim

The declaration does not measure the baryon-to-photon ratio from astronomical data. The declaration does not derive the fine-structure constant. The declaration does not prove that three spatial dimensions are the only possible dimensionality; it only shows what the rung would be if D were 3.

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: