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

horton_bifurcation_ratio_gt_one

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)

  90theorem horton_bifurcation_ratio_gt_one : 1 < horton_bifurcation_ratio := by

proof body

Term-mode proof.

  91  unfold horton_bifurcation_ratio
  92  have : (1 : ℝ) < phi := one_lt_phi
  93  nlinarith [phi_pos, one_lt_phi]
  94
  95/-- Two-step identity: `R_b = R_l^2`. The σ-conservation forcing in
  96  one statement: bifurcation per order is two length-steps per order. -/

used by (1)

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

depends on (16)

Lean names referenced from this declaration's body.