Proofs for the single-cut criterion

Wires are handled by induction in program order (wire_induction): a gate reads only inputs and earlier gates. Two facts about a cut S follow.

• Cut and paste (trace_mix): if two inputs agree on the forward and backward signals, the mixed input has the first input's values on S and the second input's values outside S. Its gate equations hold because every value a gate reads across the cut is a boundary value.
• Determination (trace_eq_of_agree_backward): the inputs placed in S and the backward signal values determine every value on S.

So the inputs with a fixed boundary key form a product of a left and a right part (card_filter_boundaryKey_eq), and for a fixed backward part the left parts of different keys are disjoint, which bounds their total size (sum_card_leftParts_le). For an accepting set, each product is a one-rectangle, so one side is smaller than the rectangle threshold (card_accepting_le_of_trace).

For the ordering remark, the number of inputs in the prefix of an injective ranking grows by at most one per step (exists_card_inputsIn_prefixBelow_eq), so some prefix holds half of the inputs.

Induction over wires and gate values

theorem Algebraic.Cutwidth.SingleCut.Internal.wire_induction {σ : Signature} {n s : ℕ} (p : Program σ n s) {P : Wire n s → Prop} (input : ∀ (j : Fin n), P (Wire.input j)) (gate : ∀ (g : Fin s), (∀ (w : Wire n s), p.Reads g w → P w) → P (Wire.gate g)) (w : Wire n s) : P w

Induction over the wires of a program in program order: a gate reads only inputs and earlier gates.

theorem Algebraic.Cutwidth.SingleCut.Internal.trace_gate {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) (x : Fin n → U) (g : Fin s) : p.trace I x (Wire.gate g) = I (p.lines g).op fun (a : Fin (σ.Arity (p.lines g).op)) => p.trace I x ((p.lines g).wires a)

The value of a gate is its operation applied to the values of the wires it reads.

theorem Algebraic.Cutwidth.SingleCut.Internal.trace_gate_congr {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) {x x' : Fin n → U} {g : Fin s} (h : ∀ (w : Wire n s), p.Reads g w → p.trace I x w = p.trace I x' w) : p.trace I x (Wire.gate g) = p.trace I x' (Wire.gate g)

Two evaluations agreeing on the wires a gate reads agree on the gate.

Cut and paste, and determination

theorem Algebraic.Cutwidth.SingleCut.Internal.trace_mix {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) {S : Finset (Wire n s)} {x x' : Fin n → U} (hfwd : ∀ w ∈ forward p S, p.trace I x w = p.trace I x' w) (hbwd : ∀ w ∈ backward p S, p.trace I x w = p.trace I x' w) (w : Wire n s) : p.trace I (mix S x x') w = if w ∈ S then p.trace I x w else p.trace I x' w

Cut and paste. If two inputs agree on the forward and backward signals of S, the mixed input has the values of the first input on S and of the second outside S.

theorem Algebraic.Cutwidth.SingleCut.Internal.trace_eq_of_agree_backward {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) {S : Finset (Wire n s)} {x x' : Fin n → U} (hin : ∀ j ∈ inputsIn S, x j = x' j) (hbwd : ∀ w ∈ backward p S, p.trace I x w = p.trace I x' w) (w : Wire n s) : w ∈ S → p.trace I x w = p.trace I x' w

Determination. The inputs placed in S and the backward signal values determine every value on S.

theorem Algebraic.Cutwidth.SingleCut.Internal.trace_eq_of_agree_forward {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) {S : Finset (Wire n s)} {x x' : Fin n → U} (hin : ∀ j ∉ inputsIn S, x j = x' j) (hfwd : ∀ w ∈ forward p S, p.trace I x w = p.trace I x' w) (w : Wire n s) : w ∉ S → p.trace I x w = p.trace I x' w

Determination outside the cut. The inputs placed outside S and the forward signal values determine every value outside S.

Boundary keys

theorem Algebraic.Cutwidth.SingleCut.Internal.agree_forward_of_boundaryKey_eq {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {I : Interpretation σ U} {S : Finset (Wire n s)} {x x' : Fin n → U} (h : boundaryKey p I S x = boundaryKey p I S x') (w : Wire n s) : w ∈ forward p S → p.trace I x w = p.trace I x' w

Equal boundary keys mean agreement on the forward signals.

theorem Algebraic.Cutwidth.SingleCut.Internal.agree_backward_of_boundaryKey_eq {σ : Signature} {n s : ℕ} {U : Type u_1} {p : Program σ n s} {I : Interpretation σ U} {S : Finset (Wire n s)} {x x' : Fin n → U} (h : boundaryKey p I S x = boundaryKey p I S x') (w : Wire n s) : w ∈ backward p S → p.trace I x w = p.trace I x' w

Equal boundary keys mean agreement on the backward signals.

theorem Algebraic.Cutwidth.SingleCut.Internal.forward_subset {σ : Signature} {n s : ℕ} (p : Program σ n s) (S : Finset (Wire n s)) : forward p S ⊆ S

theorem Algebraic.Cutwidth.SingleCut.Internal.not_mem_of_mem_backward {σ : Signature} {n s : ℕ} {p : Program σ n s} {S : Finset (Wire n s)} {w : Wire n s} (hw : w ∈ backward p S) : w ∉ S

theorem Algebraic.Cutwidth.SingleCut.Internal.boundaryKey_mix {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) {S : Finset (Wire n s)} {x x' : Fin n → U} (h : boundaryKey p I S x = boundaryKey p I S x') : boundaryKey p I S (mix S x x') = boundaryKey p I S x

Mixing two inputs with equal boundary keys keeps the key.

theorem Algebraic.Cutwidth.SingleCut.Internal.leftPart_eq_iff {n s : ℕ} {U : Type u_1} {S : Finset (Wire n s)} {x x' : Fin n → U} : leftPart S x = leftPart S x' ↔ ∀ j ∈ inputsIn S, x j = x' j

theorem Algebraic.Cutwidth.SingleCut.Internal.rightPart_eq_iff {n s : ℕ} {U : Type u_1} {S : Finset (Wire n s)} {x x' : Fin n → U} : rightPart S x = rightPart S x' ↔ ∀ j ∉ inputsIn S, x j = x' j

theorem Algebraic.Cutwidth.SingleCut.Internal.boundaryKey_eq_of_leftPart_eq {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) {S : Finset (Wire n s)} {x x' : Fin n → U} (hl : leftPart S x = leftPart S x') (hb : (boundaryKey p I S x).2 = (boundaryKey p I S x').2) : boundaryKey p I S x = boundaryKey p I S x'

Left parts and backward values determine the key.

theorem Algebraic.Cutwidth.SingleCut.Internal.boundaryKey_eq_of_rightPart_eq {σ : Signature} {n s : ℕ} {U : Type u_1} (p : Program σ n s) (I : Interpretation σ U) {S : Finset (Wire n s)} {x x' : Fin n → U} (hr : rightPart S x = rightPart S x') (ha : (boundaryKey p I S x).1 = (boundaryKey p I S x').1) : boundaryKey p I S x = boundaryKey p I S x'

Right parts and forward values determine the key.

Products

theorem Algebraic.Cutwidth.SingleCut.Internal.leftPart_mix {n s : ℕ} {U : Type u_1} (S : Finset (Wire n s)) (x x' : Fin n → U) : leftPart S (mix S x x') = leftPart S x

theorem Algebraic.Cutwidth.SingleCut.Internal.rightPart_mix {n s : ℕ} {U : Type u_1} (S : Finset (Wire n s)) (x x' : Fin n → U) : rightPart S (mix S x x') = rightPart S x'

theorem Algebraic.Cutwidth.SingleCut.Internal.eq_of_leftPart_eq_of_rightPart_eq {n s : ℕ} {U : Type u_1} {S : Finset (Wire n s)} {x x' : Fin n → U} (hl : leftPart S x = leftPart S x') (hr : rightPart S x = rightPart S x') : x = x'

An input is determined by its left and right parts.

theorem Algebraic.Cutwidth.SingleCut.Internal.mix_mem_filter {σ : Signature} {n s : ℕ} {U : Type u_1} [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) {S : Finset (Wire n s)} {Z : Finset (Fin n → U)} (hZ : ∀ x ∈ Z, ∀ x' ∈ Z, boundaryKey p I S x = boundaryKey p I S x' → mix S x x' ∈ Z) {κ : (↥(forward p S) → U) × (↥(backward p S) → U)} {x x' : Fin n → U} (hx : x ∈ {x ∈ Z | boundaryKey p I S x = κ}) (hx' : x' ∈ {x ∈ Z | boundaryKey p I S x = κ}) : mix S x x' ∈ {x ∈ Z | boundaryKey p I S x = κ}

In a set closed under mixing inputs with equal keys, the inputs with a given key are closed under mixing.

theorem Algebraic.Cutwidth.SingleCut.Internal.card_filter_boundaryKey_eq {σ : Signature} {n s : ℕ} {U : Type u_1} [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) {S : Finset (Wire n s)} {Z : Finset (Fin n → U)} (hZ : ∀ x ∈ Z, ∀ x' ∈ Z, boundaryKey p I S x = boundaryKey p I S x' → mix S x x' ∈ Z) (κ : (↥(forward p S) → U) × (↥(backward p S) → U)) : {x ∈ Z | boundaryKey p I S x = κ}.card = (leftParts p I S Z κ).card * (rightParts p I S Z κ).card

Product fibres. In a set closed under mixing inputs with equal keys, the inputs with a given key are exactly the products of their left and right parts.

Partition bounds

theorem Algebraic.Cutwidth.SingleCut.Internal.sum_card_leftParts_le {σ : Signature} {n s : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (S : Finset (Wire n s)) (Z : Finset (Fin n → U)) : ∑ κ ∈ Finset.image (boundaryKey p I S) Z, (leftParts p I S Z κ).card ≤ Fintype.card U ^ ((inputsIn S).card + (backward p S).card)

The left parts partition the left inputs for each backward part. Summed over the keys realized in Z, the left parts number at most |U| ^ (i + |B|).

theorem Algebraic.Cutwidth.SingleCut.Internal.sum_card_rightParts_le {σ : Signature} {n s : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (S : Finset (Wire n s)) (Z : Finset (Fin n → U)) : ∑ κ ∈ Finset.image (boundaryKey p I S) Z, (rightParts p I S Z κ).card ≤ Fintype.card U ^ (n - (inputsIn S).card + (forward p S).card)

The right parts partition the right inputs for each forward part. Summed over the keys realized in Z, the right parts number at most |U| ^ (n - i + |A|).

theorem Algebraic.Cutwidth.SingleCut.Internal.card_image_boundaryKey_le {σ : Signature} {n s : ℕ} {U : Type u_1} [Fintype U] [DecidableEq U] (p : Program σ n s) (I : Interpretation σ U) (S : Finset (Wire n s)) (Z : Finset (Fin n → U)) : (Finset.image (boundaryKey p I S) Z).card ≤ Fintype.card U ^ ((forward p S).card + (backward p S).card)

There are at most |U| ^ (|A| + |B|) boundary keys.

The single-cut criterion

theorem Algebraic.Cutwidth.SingleCut.Internal.glue_leftPart_rightPart {n s : ℕ} (S : Finset (Wire n s)) (x x' : Fin n → Bool) : glue (inputsIn S) (leftPart S x) (rightPart S x') = mix S x x'

Gluing a left part of x and a right part of x' is mixing them.

theorem Algebraic.Cutwidth.SingleCut.Internal.pos_of_rectangleFree {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hrect : RectangleFree f K) : 0 < K

A rectangle-free threshold is positive: the empty rectangle has no side below zero.

theorem Algebraic.Cutwidth.SingleCut.Internal.card_accepting_le_of_trace {σ : Signature} {n s : ℕ} (p : Program σ n s) (I : Interpretation σ Bool) (out : Wire n s) {f : Cslib.BooleanFunction n} (hf : ∀ (x : Cslib.BitString n), f x = p.trace I x out) {K : ℕ} (hrect : RectangleFree f K) (S : Finset (Wire n s)) : (accepting f).card ≤ (K - 1) * (2 ^ ((inputsIn S).card + (backward p S).card) + 2 ^ (n - (inputsIn S).card + (forward p S).card))

The single-cut criterion, for the function carried by a wire out.

theorem Algebraic.Cutwidth.SingleCut.Internal.card_accepting_lt_of_trace {σ : Signature} {n s : ℕ} (p : Program σ n s) (I : Interpretation σ Bool) (out : Wire n s) {f : Cslib.BooleanFunction n} (hf : ∀ (x : Cslib.BitString n), f x = p.trace I x out) {K : ℕ} (hrect : RectangleFree f K) (S : Finset (Wire n s)) : (accepting f).card < K * (2 ^ ((inputsIn S).card + (backward p S).card) + 2 ^ (n - (inputsIn S).card + (forward p S).card))

The strict form of the single-cut criterion.

theorem Algebraic.Cutwidth.SingleCut.Internal.le_max_add_clog_of_trace {σ : Signature} {n s : ℕ} (p : Program σ n s) (I : Interpretation σ Bool) (out : Wire n s) {f : Cslib.BooleanFunction n} (hf : ∀ (x : Cslib.BitString n), f x = p.trace I x out) {K : ℕ} (hrect : RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (accepting f).card) (S : Finset (Wire n s)) : n ≤ max ((inputsIn S).card + (backward p S).card) (n - (inputsIn S).card + (forward p S).card) + Nat.clog 2 K + 2

The single-cut corollary. With at least 2 ^ (n - 2) accepted inputs, one side of every cut sees at least n - ⌈log₂ K⌉ - 2 free bits.

theorem Algebraic.Cutwidth.SingleCut.Internal.sub_logb_lt_max_of_trace {σ : Signature} {n s : ℕ} (p : Program σ n s) (I : Interpretation σ Bool) (out : Wire n s) {f : Cslib.BooleanFunction n} (hf : ∀ (x : Cslib.BitString n), f x = p.trace I x out) {K : ℕ} (hrect : RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (accepting f).card) (S : Finset (Wire n s)) : ↑n - Real.logb 2 ↑K - 3 < ↑(max ((inputsIn S).card + (backward p S).card) (n - (inputsIn S).card + (forward p S).card))

The real-logarithm form of the single-cut corollary.

Circuits and orderings

theorem Algebraic.Cutwidth.SingleCut.Internal.eq_trace_of_computes {σ : Signature} {n : ℕ} {c : Circuit σ n 1} {I : Interpretation σ Bool} {f : Cslib.BooleanFunction n} (hc : c.Computes I fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) (x : Fin n → Bool) : f x = c.program.trace I x (c.outputs 0)

A single-output circuit computing f carries f on its output wire.

theorem Algebraic.Cutwidth.SingleCut.Internal.max_le_max_add (i n a b : ℕ) : max (i + b) (n - i + a) ≤ max i (n - i) + a + b

One side of a cut sees at most max i (n - i) inputs plus all crossing signals.

theorem Algebraic.Cutwidth.SingleCut.Internal.exists_eq_of_succ_le (g : ℕ → ℕ) (h : ℕ) (hzero : g 0 = 0) (hstep : ∀ (t : ℕ), g (t + 1) ≤ g t + 1) (M : ℕ) (hM : h ≤ g M) : ∃ (t : ℕ), g t = h

A monotone step function from 0 that reaches h takes the value h.

@[reducible, inline]

abbrev Algebraic.Cutwidth.SingleCut.Internal.prefixBelow {n s : ℕ} (rank : Wire n s → ℕ) (t : ℕ) : Finset (Wire n s)

The prefix of the wires ranked below t.

Equations

• Algebraic.Cutwidth.SingleCut.Internal.prefixBelow rank t = {w : Cslib.Circuits.Wire n s | rank w < t}

theorem Algebraic.Cutwidth.SingleCut.Internal.exists_card_inputsIn_prefixBelow_eq {n s : ℕ} (rank : Wire n s → ℕ) (hrank : Function.Injective rank) {h : ℕ} (hh : h ≤ n) : ∃ (t : ℕ), (inputsIn (prefixBelow rank t)).card = h

Prefixes take every input count. For an injective ranking of the wires, some prefix contains exactly h inputs, for every h ≤ n.

theorem Algebraic.Cutwidth.SingleCut.Internal.exists_prefix_le_of_trace {σ : Signature} {n s : ℕ} (p : Program σ n s) (I : Interpretation σ Bool) (out : Wire n s) {f : Cslib.BooleanFunction n} (hf : ∀ (x : Cslib.BitString n), f x = p.trace I x out) {K : ℕ} (hrect : RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (accepting f).card) (rank : Wire n s → ℕ) (hrank : Function.Injective rank) : ∃ (t : ℕ), n / 2 ≤ (forward p (prefixBelow rank t)).card + (backward p (prefixBelow rank t)).card + Nat.clog 2 K + 2

Every ordering has a heavily crossed prefix, for the function carried by a wire.