Input ports in a connected component

A connected closed set containing at least two inputs has no isolated input. Thus its existing ordinary slot edges suffice for all input ports; no auxiliary port edges are needed. The underlying multigraph and its degree and size estimates remain unchanged.

theorem Algebraic.Cutwidth.Aggregate.Wiring.fanout_pos_of_path {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (j : Fin n) (hj : Wire.input j ∈ K.carrier) {w : Wire n s} (hpath : Relation.ReflTransGen (MultiOutput.Linked p) (Wire.input j) w) (hne : Wire.input j ≠ w) : 0 < MultiOutput.Internal.WireGraph.fanout K ⟨Wire.input j, hj⟩

A path from an input to a distinct wire starts with a slot fed by that input.

theorem Algebraic.Cutwidth.Aggregate.Wiring.inputsHaveFanout_of_connected {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (hconn : ∀ u ∈ K.carrier, ∀ v ∈ K.carrier, Relation.ReflTransGen (MultiOutput.Linked p) u v) (hcard : 1 < (SingleCut.inputsIn K.carrier).card) : InputsHaveFanout K

Two or more inputs in a connected closed set all have positive fanout.

theorem Algebraic.Cutwidth.Aggregate.Wiring.nonempty_edge_of_inputsHaveFanout {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (hinput : InputsHaveFanout K) (hne : (SingleCut.inputsIn K.carrier).Nonempty) : Nonempty (MultiOutput.Internal.WireGraph.Edge K)

A closed set with a nonisolated input has a nonempty edge type.

theorem Algebraic.Cutwidth.Aggregate.Wiring.card_edge_sub_card_vertex {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) : ↑(Fintype.card (MultiOutput.Internal.WireGraph.Edge K)) - ↑(Fintype.card (MultiOutput.Internal.WireGraph.Vertex K)) = ↑(Fintype.card (MultiOutput.Internal.WireGraph.Slot K)) - ↑(Fintype.card (MultiOutput.Internal.WireGraph.Signal K))

Copy expansion preserves the exact difference between slots and signals.

theorem Algebraic.Cutwidth.Aggregate.Wiring.card_edge_sub_card_vertex_le_of_slot_bound {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) {b : ℕ} (hslots : Fintype.card (MultiOutput.Internal.WireGraph.Slot K) ≤ 2 * b) : ↑(Fintype.card (MultiOutput.Internal.WireGraph.Edge K)) - ↑(Fintype.card (MultiOutput.Internal.WireGraph.Vertex K)) ≤ 2 * ↑b - ↑(SingleCut.inputsIn K.carrier).card - ↑(MultiOutput.gatesIn K.carrier).card

An exact slot budget yields an edge-excess bound without charging nullary gates.

theorem Algebraic.Cutwidth.Aggregate.Wiring.card_vertex_le_of_slot_bound {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) {b : ℕ} (hslots : Fintype.card (MultiOutput.Internal.WireGraph.Slot K) ≤ 2 * b) : Fintype.card (MultiOutput.Internal.WireGraph.Vertex K) ≤ (SingleCut.inputsIn K.carrier).card + (MultiOutput.gatesIn K.carrier).card + 2 * b

Copy vertices cost at most one vertex per slot.

noncomputable def Algebraic.Cutwidth.Aggregate.Wiring.activeGates {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) : Finset (Fin s)

The selected gates that read at least one wire; nullary gates are excluded.

Equations

• Algebraic.Cutwidth.Aggregate.Wiring.activeGates K = {g ∈ Algebraic.Cutwidth.MultiOutput.gatesIn K.carrier | 0 < σ.Arity (p.lines g).op}

theorem Algebraic.Cutwidth.Aggregate.Wiring.card_slot_le_two_mul_activeGates {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (hp : p.FanInAtMost 2) : Fintype.card (MultiOutput.Internal.WireGraph.Slot K) ≤ 2 * (activeGates K).card

Slots are charged only to gates with nonzero arity.

theorem Algebraic.Cutwidth.Aggregate.Wiring.card_edge_sub_card_vertex_le_activeGates {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) (hp : p.FanInAtMost 2) : ↑(Fintype.card (MultiOutput.Internal.WireGraph.Edge K)) - ↑(Fintype.card (MultiOutput.Internal.WireGraph.Vertex K)) ≤ ↑(activeGates K).card - ↑(SingleCut.inputsIn K.carrier).card

Nullary gates do not increase the edge-excess upper bound.

theorem Algebraic.Cutwidth.Aggregate.Wiring.network_toMultigraph {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) : (network K hinput I).toMultigraph = MultiOutput.Internal.WireGraph.graph K

The compiler preserves the wire graph exactly.

theorem Algebraic.Cutwidth.Aggregate.Wiring.network_loopless {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) : (network K hinput I).Loopless

The compiled network has no loops.

theorem Algebraic.Cutwidth.Aggregate.Wiring.network_maxDegreeLE_three {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) (hp : p.FanInAtMost 2) : (network K hinput I).MaxDegreeLE 3

Fan-in at most two gives maximum degree at most three.

theorem Algebraic.Cutwidth.Aggregate.Wiring.network_connected {σ : Signature} {n s : ℕ} {p : Program σ n s} (K : MultiOutput.Internal.ClosedSet p) [Nonempty (MultiOutput.Internal.WireGraph.Edge K)] (hinput : InputsHaveFanout K) (I : Interpretation σ Bool) (hne : K.carrier.Nonempty) (hconn : ∀ u ∈ K.carrier, ∀ v ∈ K.carrier, Relation.ReflTransGen (MultiOutput.Linked p) u v) : (network K hinput I).Connected

A connected closed component remains connected after fanout expansion.