pith. machine review for the scientific record. sign in
structure definition def or abbrev

Q3State

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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) : ℝ :=

proof body

Definition body.

 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. -/

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (31)

Lean names referenced from this declaration's body.

… and 1 more