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)

  72noncomputable def hypothesis1 : ℝ := 1 / tau0^2

proof body

Definition body.

  73
  74/-- Hypothesis 2: Λ ∝ (τ₀ / t_universe)²
  75
  76    t_universe ~ 4.4 × 10¹⁷ s
  77    (τ₀ / t_u)² ~ (1.3e-27 / 4.4e17)² ~ 10⁻⁸⁸
  78
  79    Λ ~ τ₀⁻² × 10⁻⁸⁸ ~ 10⁻³⁵ m⁻²
  80
  81    Getting closer but still too large. -/

used by (2)

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

depends on (8)

Lean names referenced from this declaration's body.