pith. machine review for the scientific record. sign in
def definition def or abbrev high

lambdaRS

show as:
view Lean formalization →

Definition sets Λ_RS to 8φ^5/45 in native units. Cosmologists working in the Recognition Science framework cite this expression when matching the predicted vacuum energy density against the observed Ω_Λ band. The definition is a direct noncomputable assignment of the real number expression.

claim$Λ_{RS} := 8 φ^5 / 45$

background

The module treats the cosmological constant in the BIT kernel band for S3 cosmology. The golden ratio φ is the self-similar fixed point forced by the T6 step of the unified forcing chain, and the identity φ^5 = 5φ + 3 is the Fibonacci relation used to evaluate powers. The definition is imported from CosmologicalConstantFromRS to support formal band certification.

proof idea

Direct definition that assigns the real number 8 * phi ^ 5 / 45. No lemmas are invoked inside the body; the supporting identity φ^5 = 5φ + 3 is recorded only in the documentation comment for downstream use.

why it matters in Recognition Science

The definition supplies the explicit RS form of Λ_RS that feeds lambdaRS_band (proving the interval (1.88, 2.03)) and the certificate structures OmegaLambdaBandCert and CosmologicalConstantCert. It realizes the RS structural prediction for the cosmological constant inside the phi-ladder and eight-tick octave framework.

scope and limits

formal statement (Lean)

  24noncomputable def lambdaRS : ℝ := 8 * phi ^ 5 / 45

proof body

Definition body.

  25
  26/-- φ⁵ = 5φ + 3. -/

used by (7)

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

depends on (1)

Lean names referenced from this declaration's body.