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

CircuitDecides

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)

 128def CircuitDecides {n : ℕ} (c : BooleanCircuit n) (f : CNFFormula n) : Prop :=

proof body

Definition body.

 129  ∃ eval : Assignment n → Bool,
 130    (∀ a : Assignment n, eval a = (f.satisfiedBy a))
 131
 132/-! ## Part 2: Circuit Z-Complexity Capacity -/
 133
 134/-- The **bond count** of a circuit is the total number of wires (parent→child edges).
 135    Each gate contributes at most 2 wires (arity_le). -/

used by (9)

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

depends on (19)

Lean names referenced from this declaration's body.