Encyclopedia Cosmology Cosmology Eta Bexact Rung Derivation Eta B Rung From Chirality Eq
ARTICLE 4 claims 4 theorems
Cosmology Eta Bexact Rung Derivation Eta B Rung From Chirality Eq
A machine-checked theorem derives the baryon-to-photon ratio's exponent from a discrete symmetry, but the physical bridge to the cosmos remains open.
The chirality route to −44
The baryon-to-photon ratio η_B measures how many protons and neutrons exist for every photon left over from the early universe, roughly one baryon for every billion photons. In the Recognition Science framework, this ratio is pinned to a power of the golden ratio, φ^−44, where −44 is called the η_B rung. The declaration eta_B_rung_from_chirality_eq is a theorem in the framework's machine-checked library of formal theorems. It proves that a number built from two discrete symmetry properties equals −44, matching the rung derived from the spatial dimension D = 3.
The theorem's inputs are concrete. One is the flip count of a Gray code cycle on three bits, a sequence where each step changes exactly one bit, and the first step changes 4 bits. The other is a torsion gap, a difference between two entries in a spectral sequence, with absolute value 11. Their product, 4 × 11 = 44, negated, gives −44. The proof is a short chain of arithmetic equalities, checked by the kernel, with no framework-specific axioms beyond the standard three logical postulates.
This is one of three routes that converge on −44. A second route derives −44 from the number of independent degrees of freedom in a recognition event at D = 3, and a third from the Standard Model's 90 fermionic degrees of freedom halved. The framework proves all three agree, and that the chirality route is only defined at D = 3. The convergence is structural, not statistical: the routes share the same gap integer 45, so they are not independent draws.
What the theorem does not claim is the physical step. It establishes an arithmetic identity inside the framework's formal system. It does not prove that this integer is the measured baryon-to-photon ratio, nor that the framework's recognition events are the actual physics of the early universe. That bridge, from the formal structure to physical cosmology, remains an open target. The framework can still be falsified at any of the named structural inputs, such as the flip count or the torsion spectrum.
THEOREM eta_B_rung_from_chirality_eq · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
/-- The chirality route yields −44. -/
theorem eta_B_rung_from_chirality_eq : eta_B_rung_from_chirality = -44 := by
unfold eta_B_rung_from_chirality
have hflip : bitFlipCount 0 = 4 := bit0_flips_four
have htor : (torsionGap 0 1).natAbs = 11 := by native_decide
rw [hflip, htor]
decide
THEOREM eta_B_rung_from_chirality_eq · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
/-- The chirality route yields −44. -/
theorem eta_B_rung_from_chirality_eq : eta_B_rung_from_chirality = -44 := by
unfold eta_B_rung_from_chirality
have hflip : bitFlipCount 0 = 4 := bit0_flips_four
have htor : (torsionGap 0 1).natAbs = 11 := by native_decide
rw [hflip, htor]
decide
THEOREM routes_AB_agree · routes_AC_agree · routes_BC_agree · chirality_only_defined_at_D3 · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
/-- **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]
/-- D = 3 is the unique non-degenerate dimension where the chirality
product (4 × 11) and the gap-from-dimension formula (D²(D+2) − 1)
both produce the same integer 44, because:
- D = 3 is forced by T8 (linking + 8-tick + sync)
- The Gray code on Q^D is defined for D = 3 specifically
- The torsion spectrum {0, 11, 17} is a CW-filtration consequence at D = 3
For any other D the chirality route does not even type-check
(bitFlipCount is `Fin 3 → ℕ` by construction). -/
theorem chirality_only_defined_at_D3 :
eta_B_rung_from_chirality
= eta_B_rung_from_dimension Foundation.GapDerivation.D := by
rw [routes_AB_agree.symm]
THEOREM chirality_product_equals_gap_minus_one · fermionic_half_equals_gap · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
/-- The chirality flip-count × torsion product equals the gap minus the
active edge. This is a non-trivial structural identity at D = 3:
bitFlipCount(0) × |torsionGap(0,1)| = consciousnessGap(D) − A
LHS comes from the Gray code on Q₃ × CW filtration torsion.
RHS comes from the gap-from-dimension formula D²(D+2) − 1.
Both equal 44 at D = 3. -/
theorem chirality_product_equals_gap_minus_one :
((bitFlipCount 0 : ℤ) * (torsionGap 0 1).natAbs)
= (Foundation.GapDerivation.consciousnessGap Foundation.GapDerivation.D : ℤ)
- Foundation.GapDerivation.A := by
have hflip : bitFlipCount 0 = 4 := bit0_flips_four
have htor : (torsionGap 0 1).natAbs = 11 := by native_decide
have hgap : (Foundation.GapDerivation.consciousnessGap Foundation.GapDerivation.D : ℤ) = 45 := by
exact_mod_cast Foundation.GapDerivation.gap_at_D3
rw [hflip, htor, hgap]
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
What this page does not claim
The theorem does not prove that the framework's recognition events are the physical processes of the early universe. The theorem does not establish that the measured baryon-to-photon ratio equals φ^−44; that comparison is an empirical check, not a formal result. The theorem does not derive the fine-structure constant or any other coupling constant.
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:
- What physical mechanism connects the framework's recognition events to the actual baryon-to-photon ratio?
- How does the Gray code flip count relate to the CKM torsion spectrum in the framework's construction?
- Can the framework derive the baryon-to-photon ratio's value without referencing the spatial dimension D = 3?
- What experimental measurement would falsify the framework's prediction of η_B = φ^−44?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM eta_B_rung_from_chirality_eq · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
/-- The chirality route yields −44. -/ theorem eta_B_rung_from_chirality_eq : eta_B_rung_from_chirality = -44 := by unfold eta_B_rung_from_chirality have hflip : bitFlipCount 0 = 4 := bit0_flips_four have htor : (torsionGap 0 1).natAbs = 11 := by native_decide rw [hflip, htor] decideThe theorem proves that a number built from two discrete symmetry properties equals −44, matching the rung derived from the spatial dimension D = 3. eta_B_rung_from_chirality_eq · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.leanTHEOREM eta_B_rung_from_chirality_eq · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
/-- The chirality route yields −44. -/ theorem eta_B_rung_from_chirality_eq : eta_B_rung_from_chirality = -44 := by unfold eta_B_rung_from_chirality have hflip : bitFlipCount 0 = 4 := bit0_flips_four have htor : (torsionGap 0 1).natAbs = 11 := by native_decide rw [hflip, htor] decideTheir product, 4 × 11 = 44, negated, gives −44. eta_B_rung_from_chirality_eq · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.leanTHEOREM routes_AB_agree · routes_AC_agree · routes_BC_agree · chirality_only_defined_at_D3 · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
/-- **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]/-- D = 3 is the unique non-degenerate dimension where the chirality product (4 × 11) and the gap-from-dimension formula (D²(D+2) − 1) both produce the same integer 44, because: - D = 3 is forced by T8 (linking + 8-tick + sync) - The Gray code on Q^D is defined for D = 3 specifically - The torsion spectrum {0, 11, 17} is a CW-filtration consequence at D = 3 For any other D the chirality route does not even type-check (bitFlipCount is `Fin 3 → ℕ` by construction). -/ theorem chirality_only_defined_at_D3 : eta_B_rung_from_chirality = eta_B_rung_from_dimension Foundation.GapDerivation.D := by rw [routes_AB_agree.symm]The framework proves all three agree, and that the chirality route is only defined at D = 3. routes_AB_agree · routes_AC_agree · routes_BC_agree · chirality_only_defined_at_D3 · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.leanTHEOREM chirality_product_equals_gap_minus_one · fermionic_half_equals_gap · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean
/-- The chirality flip-count × torsion product equals the gap minus the active edge. This is a non-trivial structural identity at D = 3: bitFlipCount(0) × |torsionGap(0,1)| = consciousnessGap(D) − A LHS comes from the Gray code on Q₃ × CW filtration torsion. RHS comes from the gap-from-dimension formula D²(D+2) − 1. Both equal 44 at D = 3. -/ theorem chirality_product_equals_gap_minus_one : ((bitFlipCount 0 : ℤ) * (torsionGap 0 1).natAbs) = (Foundation.GapDerivation.consciousnessGap Foundation.GapDerivation.D : ℤ) - Foundation.GapDerivation.A := by have hflip : bitFlipCount 0 = 4 := bit0_flips_four have htor : (torsionGap 0 1).natAbs = 11 := by native_decide have hgap : (Foundation.GapDerivation.consciousnessGap Foundation.GapDerivation.D : ℤ) = 45 := by exact_mod_cast Foundation.GapDerivation.gap_at_D3 rw [hflip, htor, hgap] 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] decideThe convergence is structural, not statistical: the routes share the same gap integer 45, so they are not independent draws. chirality_product_equals_gap_minus_one · fermionic_half_equals_gap · IndisputableMonolith/Cosmology/EtaBExactRungDerivation.lean