Gravity Rsbaryogenesis Alpha Inflaton Pos

A small positive number

The declaration alpha_inflaton_pos establishes a single, narrow fact: the number alpha_inflaton, defined as phi to the power minus two, is greater than zero. In plain terms, it proves that a particular parameter, which the Recognition Science framework models as the alpha-attractor parameter for an inflaton potential, is a positive real number. The proof itself is a direct consequence of the fact that phi, the golden ratio, is positive.

This is a theorem in the framework's machine-checked library of formal theorems, meaning its truth is verified by a computer. The declaration does not claim that this parameter matches any observed value, nor does it assert that the inflaton potential it belongs to is the correct description of the early universe. It only certifies the sign of the number, a necessary but minimal condition for the parameter to be physically meaningful in the framework's model.

The context for this result is the framework's broader baryogenesis mechanism, which aims to derive the matter-antimatter asymmetry of the universe from a set of principles. Within that mechanism, the framework defines a prediction for the baryon asymmetry, eta_B, as approximately 5.1 times ten to the minus ten, and compares it to an observed value of 6.1 times ten to the minus ten. The theorem alpha_inflaton_pos is a small piece of this larger structure, ensuring that one of the model's parameters has the correct sign.

What the declaration does not do is prove that the framework's baryogenesis mechanism is correct. It does not establish that the predicted asymmetry matches the observed one, nor does it validate the choice of the inflaton potential. It simply verifies a basic mathematical property of a single defined quantity, a necessary step in the formalization but not a confirmation of the underlying physical theory.

theorem alpha_inflaton_pos : 0 < alpha_inflaton := Real.rpow_pos_of_pos phi_pos _

theorem alpha_inflaton_pos : 0 < alpha_inflaton := Real.rpow_pos_of_pos phi_pos _

What this page does not claim

The declaration does not claim that alpha_inflaton matches any measured value. It does not assert that the framework's baryogenesis mechanism is a correct description of the universe. It does not validate the choice of the inflaton potential or any other aspect of the cosmology model.

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: