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

hypothesis1

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)

  78noncomputable def hypothesis1 : ℝ := Real.sqrt (1 - 1/phi^2)

proof body

Definition body.

  79
  80/-- Hypothesis 2: cos(θ_W) = (φ + 1) / (φ + 2)
  81
  82    (1.618 + 1) / (1.618 + 2) = 2.618 / 3.618 ≈ 0.724
  83
  84    This is also too small. -/

used by (2)

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

depends on (7)

Lean names referenced from this declaration's body.