pith. sign in
module module high

IndisputableMonolith.Unification.RegistryPredictionsProved

show as:
view Lean formalization →

The module establishes that the Ω_Λ formula derived from the Recognition Science registry is well-defined and satisfies the bound Ω_Λ < 11/16. Cosmologists addressing the cosmological constant problem cite these certified inequalities. The argument assembles direct calculations from the imported phi-forcing, gap-weight, and alpha modules into a collection of explicit bounds.

claimThe dark energy density parameter satisfies $\Omega_\Lambda < 11/16$ with the defining formula well-defined in RS-native units.

background

This module operates in the Unification domain and imports the core RS constants (τ₀ = 1 tick), the alpha pipeline, the gap weight w₈ · ln(φ) from the 8-tick projection, and the PhiForcing module. The latter proves that φ is forced by self-similarity in a discrete ledger with J-cost structure. The module's siblings supply the concrete inequalities (omega_lambda_lt_11_16, omega_lambda_positive, phi_6_hierarchy_bounds) that together certify the registry prediction.

proof idea

The module is a collection of explicit inequality theorems. Each applies the phi-ladder and gap-weight definitions imported from PhiForcing and GapWeight to obtain the stated bounds on Ω_Λ; no single master tactic is used beyond direct algebraic reduction and numeric certification.

why it matters in Recognition Science

The module supplies the certified Ω_Λ bounds required by the downstream CosmologicalConstantDerivation module, which addresses registry item C-010 on the determination of Λ. It closes the gap between the phi-forcing foundation and the cosmological constant derivation.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.

declarations in this module (9)