consciousness_zero_cost

formal source

 350  entries_pos := fun _ => by norm_num
 351
 352/-- **THEOREM**: The consciousness ground state has zero total cost. -/
 353theorem consciousness_zero_cost : consciousness_ground.total_cost = 0 := by
 354  unfold Q3State.total_cost consciousness_ground
 355  simp only [Jcost_unit0, Finset.sum_const_zero]
 356
 357/-- **THEOREM**: The consciousness ground state is at zero defect. -/
 358theorem consciousness_is_zero_defect : consciousness_ground.is_zero_defect :=
 359  fun _ => rfl
 360
 361/-- **THEOREM**: Every state is either conscious (zero defect) or
 362    particle-like (positive defect). There is no middle ground. -/
 363theorem consciousness_or_particle (s : Q3State) :
 364    s.is_zero_defect ∨ ∃ i : Fin 8, s.entries i ≠ 1 := by
 365  by_cases h : ∀ i, s.entries i = 1
 366  · exact Or.inl h
 367  · push_neg at h; exact Or.inr h
 368
 369/-- **THEOREM**: The zero-defect subspace has dimension 1.
 370    There is exactly ONE consciousness ground state (up to phase). -/
 371theorem zero_defect_unique :
 372    ∀ s : Q3State, s.is_zero_defect →
 373    ∀ i : Fin 8, s.entries i = consciousness_ground.entries i :=
 374  fun _s h i => h i
 375
 376/-- **THEOREM**: Any deviation from the ground state costs.
 377    If any entry deviates from 1, the total cost is strictly positive. -/
 378theorem any_deviation_costs (s : Q3State) (i : Fin 8) (hi : s.entries i ≠ 1) :
 379    0 < Jcost (s.entries i) := by
 380  rw [Jcost_eq_sq (ne_of_gt (s.entries_pos i))]
 381  apply div_pos
 382  · have : s.entries i - 1 ≠ 0 := sub_ne_zero.mpr hi
 383    positivity