pith. machine review for the scientific record. sign in
theorem proved term proof

zero_defect_unique

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)

 371theorem zero_defect_unique :
 372    ∀ s : Q3State, s.is_zero_defect →
 373    ∀ i : Fin 8, s.entries i = consciousness_ground.entries i :=

proof body

Term-mode proof.

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

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.