pith. machine review for the scientific record. sign in
theorem proved tactic proof high

lambdaRS_band

show as:
view Lean formalization →

The theorem proves that the RS cosmological constant Lambda_RS equals eight phi to the fifth over forty-five and lies strictly inside the interval from 1.88 to 2.03. Cosmologists working inside the Recognition Science framework cite this band when matching the predicted dark-energy density against Planck data. The argument substitutes the Fibonacci identity phi^5 equals five phi plus three, inserts the numerical bounds 1.61 less than phi less than 1.62, and closes each side of the resulting inequality with nlinarith followed by linarith.

claimLet $Lambda_RS := 8 phi^5 / 45$. Then $1.88 < Lambda_RS < 2.03$.

background

The module OmegaLambdaBITKernelBand supplies the RS-native cosmological constant as Lambda_RS = 8 phi^5 / 45, where phi is the golden ratio fixed by the self-similar point of the Recognition Composition Law. The key algebraic identity phi^5 = 5 phi + 3 is supplied by phi5_eq, which itself rests on the quadratic relation phi^2 = phi + 1 and repeated nlinarith reductions. The module imports the tight numerical bounds phi greater than 1.61 and phi less than 1.62 from Constants; these bounds are proved by comparing squares to 5 and invoking the monotonicity of the square-root function.

proof idea

The tactic proof first unfolds the definition of lambdaRS. It then obtains the exact identity phi^5 = 5 phi + 3 from phi5_eq and the two phi bounds from phi_gt_onePointSixOne and phi_lt_onePointSixTwo. The goal is split by constructor into a lower and an upper inequality. Each side is rewritten by substituting the identity, after which div_lt_div_of_pos_right is applied and the resulting linear inequalities are discharged by nlinarith and linarith.

why it matters in Recognition Science

This theorem supplies the certified numerical band required by omegaLambdaBandCert and by cosmologicalConstantCert in the CosmologicalConstantFromRS module. It therefore completes the formal placement of the RS cosmological constant inside the interval (1.88, 2.03) that follows from the phi-ladder and the eight-tick octave structure. The result is cited whenever the Recognition Science prediction for dark energy is compared with the observed Omega_Lambda approximately 0.6847 times three H_0 squared.

scope and limits

Lean usage

theorem cosmologicalConstantCert : CosmologicalConstantCert where phi5_val := phi5_eq lambda_pos := lambdaRS_pos lambda_band := lambdaRS_band

formal statement (Lean)

  34theorem lambdaRS_band :
  35    (1.88 : ℝ) < lambdaRS ∧ lambdaRS < 2.03 := by

proof body

Tactic-mode proof.

  36  unfold lambdaRS
  37  have h5 : phi ^ 5 = 5 * phi + 3 := phi5_eq
  38  have h1 := phi_gt_onePointSixOne
  39  have h2 := phi_lt_onePointSixTwo
  40  constructor
  41  · have : 8 * phi ^ 5 / 45 > 8 * (5 * 1.61 + 3) / 45 := by
  42      apply div_lt_div_of_pos_right _ (by norm_num)
  43      nlinarith
  44    linarith
  45  · have : 8 * phi ^ 5 / 45 < 8 * (5 * 1.62 + 3) / 45 := by
  46      apply div_lt_div_of_pos_right _ (by norm_num)
  47      nlinarith
  48    linarith
  49
  50/-- Λ_RS > 0. -/

used by (3)

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

depends on (10)

Lean names referenced from this declaration's body.