Gravity Rsbaryogenesis Kappa Cp Lt One

The small CP-odd coupling

The declaration kappa_CP_lt_one establishes a simple inequality about a number the framework calls kappa_CP, a coupling constant that controls the strength of a certain interaction. In plain terms, it proves that this coupling is less than 1, and a companion theorem shows it is also greater than 0. The number itself is defined as the golden ratio raised to the power -9, which is approximately 0.0131. This is a small number, and the inequality confirms that the interaction it describes is weak in the framework's units.

The proof of this inequality is not a deep physical argument; it follows from the fact that the golden ratio is greater than 1. Raising a number greater than 1 to a negative exponent always yields a value between 0 and 1. The declaration is a formal, machine-checked theorem, meaning it is a logical consequence of the definitions chosen, not a measurement or a hypothesis. It is part of a larger structure in the framework's library that aims to derive properties of the early universe from a few starting assumptions.

In the context of the framework's baryogenesis mechanism, which attempts to explain the observed excess of matter over antimatter, this small coupling is one of two CP-odd parameters. The other, lambda_CP, is the golden ratio raised to the power -7, which is larger than kappa_CP but still less than 1. The framework proves that kappa_CP is smaller than lambda_CP, a relationship it labels as 'grav_stronger'. The smallness of these couplings is a necessary condition for the mechanism to produce the observed baryon asymmetry, which the framework estimates at about 5.1 times 10 to the power -10, compared to an observed value of about 6.1 times 10 to the power -10.

What this declaration does not claim is as important as what it proves. It does not assert that the framework's baryogenesis mechanism is correct, nor does it derive the value of the baryon asymmetry from first principles. The inequality is a statement about a defined quantity, not a physical law. The framework's overall model is a set of definitions and hypotheses, and this theorem is a small, verified piece of that model. The physical interpretation and the comparison to observation are separate, empirical steps that the framework's library also formalizes, but this particular declaration only establishes the numerical bound.

/-- κ_CP < 1 (follows from κ < λ < 1). -/
theorem kappa_CP_lt_one : kappa_CP < 1 :=
  lt_trans lambda_gt_kappa lambda_CP_lt_one

/-- The CP-odd electromagnetic coupling: κ_CP = φ⁻⁹.
    This determines the strength of the χFF̃ term. -/
noncomputable def kappa_CP : ℝ := phi ^ (-(9 : ℝ))

theorem kappa_CP_bounds : 0 < kappa_CP ∧ kappa_CP < 1 :=
  ⟨kappa_CP_pos, kappa_CP_lt_one⟩

What this page does not claim

The declaration does not prove that the framework's baryogenesis mechanism is physically correct. The declaration does not derive the value of the baryon asymmetry from the smallness of kappa_CP. The declaration does not make any claim about the value of kappa_CP in conventional particle physics.

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: