Guess-independent erased graphs

Changing guessed output bits changes nullary constants but not slots, components, or their primary inputs. Only original binary gates contribute incoming slots.

def Algebraic.Aggregate.transportClosedSet {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a b : Guess p) (K : Cutwidth.MultiOutput.Internal.ClosedSet (erase p a)) : Cutwidth.MultiOutput.Internal.ClosedSet (erase p b)

Transfer an erased closed component to another guess, retaining exactly its carrier.

Equations

• Algebraic.Aggregate.transportClosedSet p a b K = { carrier := K.carrier, closed := ⋯ }

theorem Algebraic.Aggregate.linked_erase_iff {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a b : Guess p) (u v : Wire n g) : Cutwidth.MultiOutput.Linked (erase p a) u v ↔ Cutwidth.MultiOutput.Linked (erase p b) u v

theorem Algebraic.Aggregate.connected_transportClosedSet {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a b : Guess p) (K : Cutwidth.MultiOutput.Internal.ClosedSet (erase p a)) (connected : ∀ u ∈ K.carrier, ∀ v ∈ K.carrier, Relation.ReflTransGen (Cutwidth.MultiOutput.Linked (erase p a)) u v) (u : Wire n g) : u ∈ (transportClosedSet p a b K).carrier → ∀ v ∈ (transportClosedSet p a b K).carrier, Relation.ReflTransGen (Cutwidth.MultiOutput.Linked (erase p b)) u v

theorem Algebraic.Aggregate.card_activeGates_le {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) (a : Guess p) (K : Cutwidth.MultiOutput.Internal.ClosedSet (erase p a)) : (Cutwidth.Aggregate.Wiring.activeGates K).card ≤ ordinaryCount p

Special nullary vertices are never charged as binary gate vertices.