Q3State

formal source

 328
 329/-- A recognition state on the Q₃ lattice: an assignment of ratios
 330    to the 8 vertices, each positive. -/
 331structure Q3State where
 332  entries : Fin 8 → ℝ
 333  entries_pos : ∀ i, 0 < entries i
 334
 335/-- Total J-cost (defect) of a Q₃ state. -/
 336def Q3State.total_cost (s : Q3State) : ℝ :=
 337  Finset.univ.sum (fun i => Jcost (s.entries i))
 338
 339/-- A Q₃ state is at zero defect iff every entry equals 1. -/
 340def Q3State.is_zero_defect (s : Q3State) : Prop :=
 341  ∀ i : Fin 8, s.entries i = 1
 342
 343/-- A Q₃ state is particle-like iff it has positive total defect. -/
 344def Q3State.is_particle (s : Q3State) : Prop :=
 345  0 < s.total_cost
 346
 347/-- The consciousness ground state: all entries at unity. -/
 348def consciousness_ground : Q3State where
 349  entries := fun _ => 1
 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