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

hypothesis3

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)

  96noncomputable def hypothesis3 : ℝ := 1 / phi^lambda_exponent

proof body

Definition body.

  97
  98/-- **BEST APPROACH**: Λ emerges from J-cost ground state energy.
  99
 100    The vacuum has a nonzero J-cost due to φ-mismatch.
 101    J_vac = Jcost(φ) = (φ + 1/φ)/2 - 1 = (φ² + 1)/(2φ) - 1
 102
 103    This is ~0.118, not the suppression we need.
 104    Need a MORE subtle mechanism. -/

used by (2)

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

depends on (13)

Lean names referenced from this declaration's body.