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

hubble_formula_structure

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  83theorem hubble_formula_structure : ∃ (H0 : ℝ), H0 = Real.log phi / 8 := by

proof body

Term-mode proof.

  84  use Real.log phi / 8
  85
  86/-! ## Section: Phi Powers for Cosmology -/
  87
  88/-- **CALCULATED**: φ² bounds (useful for many calculations).
  89    
  90    With 1.61 < φ < 1.62: 2.59 < φ² < 2.62 -/

depends on (4)

Lean names referenced from this declaration's body.