Cosmology Eta Bexact Rung Derivation Eta B Rung From Dimension Factored

The factored rung formula

The baryon-to-photon ratio, written η_B, is a cosmological number: the count of ordinary matter particles (protons and neutrons) for every photon left over from the early universe. In the Recognition Science framework, this ratio sits on a ladder of powers of the golden ratio φ, and its exponent is the integer −44. The declaration eta_B_rung_from_dimension_factored (a theorem in the framework's machine-checked library of formal theorems) establishes that this exponent can be written as a simple product: 1 minus the number of ledger parities times the number of configuration dimensions.

In plain terms, the theorem says the rung is not an arbitrary fitted number. It is the difference between one active edge and a product of two structural counts. At three spatial dimensions, the count of independent ledger parities is 9 (three squared), and the count of configuration dimensions is 5 (three spatial, one temporal, one ledger balance). Their product is 45, so the rung is 1 − 45 = −44. The theorem factors this calculation: it proves the formula for any dimension d, not just d = 3, rewriting the earlier definition into this product form.

The theorem's force is that it isolates where the number 45 comes from. It does not invent 45; it derives it from the dimension count. The same 45 appears in two other routes: a chirality route (4 × 11 = 44, negated) and a fermionic route (90 degrees of freedom divided by 2, minus 1). The library proves all three routes agree at −44, and calls this a convergence theorem. The factored form is the dimensional route's contribution to that convergence.

What the theorem does not claim is just as important. It does not claim that η_B itself is measured to be exactly φ^(−44); that comparison against cosmological observations is a separate empirical check, not a theorem. It does not claim the product formula is physically meaningful outside the framework's definitions of parity count and configuration dimension. And it does not claim that the convergence of the three routes proves the framework true: the docstring explicitly says the framework can still be falsified at any of the named structural inputs. The theorem is a structural identity inside the framework, not a measurement and not a proof of the framework's physical truth.

/-- The route in terms of the configuration dimension and the parity count. -/
theorem eta_B_rung_from_dimension_factored (d : ℕ) :
    eta_B_rung_from_dimension d =
      Foundation.GapDerivation.A
        - ((Foundation.GapDerivation.parityCount d : ℤ)
            * (Foundation.GapDerivation.configDim d : ℤ)) := by
  unfold eta_B_rung_from_dimension Foundation.GapDerivation.consciousnessGap
  push_cast
  ring

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

/-- **THE η_B EXACT RUNG THEOREM**:

    The φ-rung exponent −44 of the baryon-to-photon ratio is forced
    by D = 3 via convergent structural routes that all agree.

    No route uses the empirical value of η_B as input. The agreement
    is a derivation, not a fit. -/
theorem etaBExactRungCert : EtaBExactRungCert where
  route_A_dimension := eta_B_rung_from_dimension_at_D3
  route_B_chirality := eta_B_rung_from_chirality_eq
  route_C_fermionic := eta_B_rung_from_fermionic_eq
  AB_agree := routes_AB_agree
  AC_agree := routes_AC_agree
  BC_agree := routes_BC_agree
  chirality_gap_bridge := chirality_product_equals_gap_minus_one
  fermionic_gap_bridge := fermionic_half_equals_gap
  matches_existing := matches_existing_eta_B_rung
  rung_sum := derived_rung_sum

What this page does not claim

The theorem does not claim the measured cosmological η_B equals φ^(−44); that is an empirical check, not a proved identity. The theorem does not claim the product formula has physical meaning outside the framework's definitions. The theorem does not claim the convergence of routes proves the framework true; the docstring names falsifiable inputs.

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: