equilibrium_is_zero

formal source

  40theorem freeWillPositionCount : Fintype.card FreeWillPosition = 5 := by decide
  41
  42/-- Free choice: degeneracy at J = 0. -/
  43theorem equilibrium_is_zero : Jcost 1 = 0 := Jcost_unit0
  44
  45/-- Choice symmetry: each choice and its opposite have equal cost. -/
  46theorem choice_symmetric {r : ℝ} (hr : 0 < r) :
  47    Jcost r = Jcost r⁻¹ := Jcost_symm hr
  48
  49/-- Constraint: off-equilibrium choices carry recognition cost. -/
  50theorem constrained_choice {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  51    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  52
  53/-- Free choice exists at J = 0 (multiple paths attain minimum). -/
  54def HasFreeChoice (paths : List ℝ) : Prop :=
  55  paths.length ≥ 2 ∧ ∀ r ∈ paths, r > 0 ∧ Jcost r = 0
  56
  57/-- A trivial free-choice instance: {1, 1}. -/
  58theorem trivial_free_choice : HasFreeChoice [1, 1] := by
  59  constructor
  60  · decide
  61  · intro r hr
  62    simp at hr
  63    exact ⟨by linarith [phi_gt_onePointFive], by rw [hr]; exact Jcost_unit0⟩
  64
  65structure FreeWillCert where
  66  five_positions : Fintype.card FreeWillPosition = 5
  67  equilibrium : Jcost 1 = 0
  68  symmetry : ∀ {r : ℝ}, 0 < r → Jcost r = Jcost r⁻¹
  69  constraint : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  70  free_choice_exists : HasFreeChoice [1, 1]
  71
  72def freeWillCert : FreeWillCert where
  73  five_positions := freeWillPositionCount