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

flat_minimizes_cost

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)

 135theorem flat_minimizes_cost :
 136    curvatureCost 1 ≤ curvatureCost 1.01 := by

proof body

Term-mode proof.

 137  unfold curvatureCost
 138  simp only [sub_self, sq, mul_zero, add_zero]
 139  -- Jcost(1) = 0, and Jcost(1 + 0.01²) ≥ 0
 140  rw [Cost.Jcost_unit0]
 141  apply Cost.Jcost_nonneg
 142  -- Need 1 + (1.01 - 1)^2 > 0, which is 1 + 0.0001 = 1.0001 > 0
 143  norm_num
 144
 145/-! ## φ and Critical Density -/
 146
 147/-- In RS, the critical density may be φ-related:
 148
 149    ρ_c = f(φ, τ₀, c, G)
 150
 151    Possible relation:
 152    ρ_c × τ₀³ × c³ / G = φ^n for some n
 153
 154    This would explain why ρ_c has its particular value. -/

depends on (25)

Lean names referenced from this declaration's body.