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

hypothesis5

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)

 106noncomputable def hypothesis5 : ℝ := Real.sqrt (1 - 1/(2*phi + 1))

proof body

Definition body.

 107
 108/-- Hypothesis 6: A more complex φ-expression.
 109
 110    cos(θ_W) = (φ³ - 1) / (φ³ + 1)
 111    = (4.236 - 1) / (4.236 + 1) = 3.236 / 5.236 ≈ 0.618
 112
 113    This is too small. -/

used by (2)

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

depends on (9)

Lean names referenced from this declaration's body.