  39theorem near_nothing_is_costly {x : ℝ} (hx : 0 < x) (hlt : x < 1) :
  40    Jcost x > 0 := non_existence_costs hx (ne_of_lt hlt)
  41
  42structure ExistenceCert where
  43  five_modes : Fintype.card ExistenceMode = 5
  44  existence_zero : Jcost 1 = 0
  45  non_existence_positive : ∀ {x : ℝ}, 0 < x → x ≠ 1 → 0 < Jcost x
  46
  47def existenceCert : ExistenceCert where
  48  five_modes := existenceModeCount
  49  existence_zero := existence_zero_cost
  50  non_existence_positive := non_existence_costs
  51
  52end IndisputableMonolith.Philosophy.ExistenceFromJCost

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.