Encyclopedia Gravity Gravity Rsbaryogenesis Lambda Cp Lt One
ARTICLE 3 claims 2 theorems 1 model
Gravity Rsbaryogenesis Lambda Cp Lt One
A single number, less than one, is the seed of a parameter-free account of why matter survived antimatter.
A small number with a large job
In physics, the imbalance between matter and antimatter in the observable universe is one of the great unsolved problems. The standard model of particle physics has no way to explain why we see matter at all. The measured ratio of baryons (protons and neutrons) to photons is about 6.1 × 10⁻¹⁰, a number that cosmology must explain but the standard model cannot. The Recognition Science framework addresses this with a mechanism it calls RS baryogenesis.
The declaration lambda_CP_lt_one is a small but load-bearing theorem in that mechanism. It proves that a quantity named lambda_CP, which the framework defines as the golden ratio φ raised to the power −7, is strictly between zero and one. In plain language, it establishes that a specific coupling constant, a number measuring the strength of an interaction, is positive and less than one. This is not a trivial bound. In the framework's account, this coupling is the seed of the entire matter-antimatter asymmetry.
The golden ratio φ is about 1.618, so φ⁻⁷ is about 0.034. The framework derives this number, and a companion coupling kappa_CP = φ⁻⁹, from the golden ratio alone, with no free parameters. These two numbers feed into a calculation that yields a predicted baryon asymmetry of 5.1 × 10⁻¹⁰, which the framework's library proves is within 20 percent of the observed value. The theorem lambda_CP_lt_one is the anchor of that calculation: it certifies that the coupling is a valid, small parameter, the kind of number that makes a perturbative calculation trustworthy.
The theorem itself is a formal statement in the framework's machine-checked library of formal theorems. It proves the inequality and nothing more. It does not prove that the baryogenesis mechanism is correct, that the golden ratio is the true source of the asymmetry, or that the prediction of 5.1 × 10⁻¹⁰ is the final word. Those are claims of a different kind, resting on the framework's broader assumptions and on the empirical comparison, not on this single inequality.
What the theorem does give is a precise, checkable fact: a specific number defined by the framework is a positive quantity less than one. That fact is the foundation of a larger edifice. It is the kind of small, exact result that a large theory needs if it is to be taken seriously. The reader can now see that the framework's baryogenesis story begins with a well-defined, bounded parameter, not with an arbitrary choice.
THEOREM lambda_CP_bounds · IndisputableMonolith/Gravity/RSBaryogenesis.lean
theorem lambda_CP_bounds : 0 < lambda_CP ∧ lambda_CP < 1 :=
⟨lambda_CP_pos, lambda_CP_lt_one⟩
MODEL lambda_CP · kappa_CP · IndisputableMonolith/Gravity/RSBaryogenesis.lean
/-- The CP-odd gravitational coupling: λ_CP = φ⁻⁷.
This determines the strength of the χRR̃ term in the
CP-violating Lagrangian. -/
noncomputable def lambda_CP : ℝ := phi ^ (-(7 : ℝ))
/-- The CP-odd electromagnetic coupling: κ_CP = φ⁻⁹.
This determines the strength of the χFF̃ term. -/
noncomputable def kappa_CP : ℝ := phi ^ (-(9 : ℝ))
THEOREM eta_B_within_20_percent · IndisputableMonolith/Gravity/RSBaryogenesis.lean
theorem eta_B_within_20_percent :
eta_B_fractional_offset < 0.20 := by
unfold eta_B_fractional_offset eta_B_prediction eta_B_observed
norm_num
What this page does not claim
The theorem does not prove the baryogenesis mechanism is physically correct. The theorem does not establish that the golden ratio is the true source of the asymmetry. The theorem does not prove the predicted asymmetry is the final measured value.
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/Gravity/RSBaryogenesis.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 in the framework turns these two small couplings into a full baryogenesis calculation?
- How does the framework derive the recognition mass scale from the Planck mass?
- What is the alpha-attractor parameter and how does it connect to inflation?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM lambda_CP_bounds · IndisputableMonolith/Gravity/RSBaryogenesis.lean
theorem lambda_CP_bounds : 0 < lambda_CP ∧ lambda_CP < 1 := ⟨lambda_CP_pos, lambda_CP_lt_one⟩It proves that a quantity named lambda_CP, which the framework defines as the golden ratio φ raised to the power −7, is strictly between zero and one. lambda_CP_bounds · IndisputableMonolith/Gravity/RSBaryogenesis.leanMODEL lambda_CP · kappa_CP · IndisputableMonolith/Gravity/RSBaryogenesis.lean
/-- The CP-odd gravitational coupling: λ_CP = φ⁻⁷. This determines the strength of the χRR̃ term in the CP-violating Lagrangian. -/ noncomputable def lambda_CP : ℝ := phi ^ (-(7 : ℝ))/-- The CP-odd electromagnetic coupling: κ_CP = φ⁻⁹. This determines the strength of the χFF̃ term. -/ noncomputable def kappa_CP : ℝ := phi ^ (-(9 : ℝ))The framework derives this number, and a companion coupling kappa_CP = φ⁻⁹, from the golden ratio alone, with no free parameters. lambda_CP · kappa_CP · IndisputableMonolith/Gravity/RSBaryogenesis.leanTHEOREM eta_B_within_20_percent · IndisputableMonolith/Gravity/RSBaryogenesis.lean
theorem eta_B_within_20_percent : eta_B_fractional_offset < 0.20 := by unfold eta_B_fractional_offset eta_B_prediction eta_B_observed norm_numThe framework's library proves is within 20 percent of the observed value. eta_B_within_20_percent · IndisputableMonolith/Gravity/RSBaryogenesis.lean