  35  nlinarith
  36
  37/-- φ⁵ > 11.05 (using φ > 1.61). -/
  38theorem phi5_gt : (11.05 : ℝ) < phi ^ 5 := by
  39  rw [phi5_eq]
  40  linarith [phi_gt_onePointSixOne]
  41
  42/-- φ⁵ < 11.11 (using φ < 1.62). -/
  43theorem phi5_lt : phi ^ 5 < (11.11 : ℝ) := by
  44  rw [phi5_eq]
  45  linarith [phi_lt_onePointSixTwo]
  46
  47inductive ZAgingChannel where
  48  | matterDensity
  49  | radiationDensity
  50  | darkEnergy
  51  | curvature
  52  | scalarPerturbation
  53  deriving DecidableEq, Repr, BEq, Fintype
  54
  55theorem zAgingChannel_count : Fintype.card ZAgingChannel = 5 := by decide
  56
  57/-- Hubble ratio band: (1.075, 1.091) contains empirical 1.083. -/
  58noncomputable def hubbleRatioBand : ℝ × ℝ := (1.075, 1.091)
  59
  60theorem hubbleBand_contains_empirical : hubbleRatioBand.1 < 1.083 ∧ 1.083 < hubbleRatioBand.2 := by
  61  unfold hubbleRatioBand
  62  constructor <;> norm_num
  63
  64theorem hubbleBand_width_pos : hubbleRatioBand.1 < hubbleRatioBand.2 := by
  65  unfold hubbleRatioBand; norm_num
  66
  67structure HubbleTensionCert where
  68  phi5_fibonacci : phi ^ 5 = 5 * phi + 3

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.