Unique consistent values at a circuit cut

For any selected gates, there is exactly one consistent assignment of guessed values: the actual evaluation restricted to those gates. Consequently a circuit's output can be described by existentially guessing the cut values, checking the selected gates' equations, and evaluating the output with those guesses. This is a semantic certificate theorem; it makes no formula-size or communication-cost claim.

These are generic extensions of CSLib's Program and Circuit, suitable for upstreaming. Repeated uses of a selected gate read the same guessed value.

theorem Cslib.Circuits.Program.evalCut_eq_eval_of_consistent {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (cut : Finset (Fin g)) (I : Interpretation σ U) (x : Fin n → U) (guess : ↥cut → U) (consistent : p.CutConsistent cut I x guess) : p.evalCut cut I x guess = p.eval I x

A consistent guess recovers all gate values, including unselected gates.

theorem Cslib.Circuits.Program.cutConsistent_iff {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (cut : Finset (Fin g)) (I : Interpretation σ U) (x : Fin n → U) (guess : ↥cut → U) : p.CutConsistent cut I x guess ↔ ∀ (j : ↥cut), guess j = p.eval I x ↑j

Consistency is equivalent to agreement with the actual values at the cut.

theorem Cslib.Circuits.Program.existsUnique_cutConsistent {σ : Signature} {n g : ℕ} {U : Type u_1} (p : Program σ n g) (cut : Finset (Fin g)) (I : Interpretation σ U) (x : Fin n → U) : ∃! guess : ↥cut → U, p.CutConsistent cut I x guess

Every input has exactly one consistent cut certificate.

theorem Cslib.Circuits.Circuit.eval_eq_iff_exists_cut {σ : Signature} {n m : ℕ} {U : Type u_1} (c : Circuit σ n m) (cut : Finset (Fin c.size)) (I : Interpretation σ U) (x : Fin n → U) (y : Fin m → U) : c.eval I x = y ↔ ∃ (guess : ↥cut → U), c.program.CutConsistent cut I x guess ∧ Wire.elim x (c.program.evalCut cut I x guess) ∘ c.outputs = y

Guessing and checking the cut values gives exactly the original circuit's output.