ExistenceMode

formal source

  22namespace IndisputableMonolith.Philosophy.ExistenceFromJCost
  23open Cost
  24
  25inductive ExistenceMode where
  26  | physical | biological | conscious | mathematical | ethical
  27  deriving DecidableEq, Repr, BEq, Fintype
  28
  29theorem existenceModeCount : Fintype.card ExistenceMode = 5 := by decide
  30
  31/-- Existence = J = 0. -/
  32theorem existence_zero_cost : Jcost 1 = 0 := Jcost_unit0
  33
  34/-- Non-existence costs: J > 0 for x ≠ 1. -/
  35theorem non_existence_costs {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) :
  36    0 < Jcost x := Jcost_pos_of_ne_one x hx hne
  37
  38/-- Near-nothing is costly: J(x) increases as x → 0. -/
  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