Proofs for multiplication in coordinates

Write X(u) = ∑ j, u j • b j for the element with coordinates u, and split the 2 n inputs into the coordinates x of the first factor (xCoords) and y of the second (yCoords).

• Fixing one factor. With the second factor fixed to Y = X(y₀), the product changes by shiftLeft b y₀ d = b.repr (X(d_x) * Y) when the input changes by d (fieldMul_sub_left), and symmetrically with the first factor fixed (fieldMul_sub_right). So the kernel form of the restricted rank-cut bound (card_pow_le_supportedKernel_of_trace) applies on these slices.
• Averaging the fixed factor. For P within the first factor and rows Q, summing the kernel supportedKernel (shiftLeft b y₀) P Q over all y₀ counts the pairs (d, y₀). The vector d = 0 lies in every kernel; for d ≠ 0 the element X(d_x) is nonzero, so Y ↦ X(d_x) * Y is a bijection and exactly |F| ^ (n - |Q|) values y₀ put d in the kernel (card_filter_shiftLeft_eq). The sum is at most |F| ^ n + |F| ^ (|P| + n - |Q|) (sum_card_supportedKernel_le), at most 2 |F| ^ n when |P| ≤ |Q|; with two blocks, some y₀ makes both kernels number at most 4 together (exists_card_add_card_le_four).
• The cut bound (le_add_two_of_trace). A split holding a inputs of the first factor and n - a outputs has two blocks with |P| = |Q|, so |F| ^ n ≤ |F| ^ (|A| + |B|) · 4 and n ≤ |A| + |B| + 2.
• One component (mem_component_of_trace). The component of an output is closed, so both kernels are full on it (apply_eq_zero_of_closed_of_trace). Since b j * ((b j)⁻¹ * b i) = b i, a suitable fixed factor makes any block with a column and a row nonzero; so the component holds every input of either factor and every output.
• Distinct terminals (terminal_injective). The outputs are distinct wires (fix y = 1), and none is an input of the first factor (fix y = 0). So the number of first-factor inputs and outputs in a prefix grows by at most one per wire, and a prefix ending at one of them holds exactly n. Charging it to the component holding all 2 n inputs gives n - 2 ≤ (A + η) (s - 2 n)⁺ + 3 log₂ (2 n + 3 s) + C (sub_two_le_of_trace), and the asymptotic (2 + 1/A - ε) n bound follows as for totally regular maps.

The two factors

def Algebraic.Cutwidth.MultiOutput.Internal.xCoords (n : ℕ) : Finset (Fin (n + n))

The inputs holding the coordinates of the first factor.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.xCoords n = Finset.map (Fin.castAddEmb n) Finset.univ

def Algebraic.Cutwidth.MultiOutput.Internal.yCoords (n : ℕ) : Finset (Fin (n + n))

The inputs holding the coordinates of the second factor.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.yCoords n = Finset.map (Fin.natAddEmb n) Finset.univ

theorem Algebraic.Cutwidth.MultiOutput.Internal.castAdd_mem_xCoords {n : ℕ} (j : Fin n) : Fin.castAdd n j ∈ xCoords n

theorem Algebraic.Cutwidth.MultiOutput.Internal.natAdd_notMem_xCoords {n : ℕ} (j : Fin n) : Fin.natAdd n j ∉ xCoords n

theorem Algebraic.Cutwidth.MultiOutput.Internal.natAdd_mem_yCoords {n : ℕ} (j : Fin n) : Fin.natAdd n j ∈ yCoords n

theorem Algebraic.Cutwidth.MultiOutput.Internal.castAdd_notMem_yCoords {n : ℕ} (j : Fin n) : Fin.castAdd n j ∉ yCoords n

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_xCoords {n : ℕ} : (xCoords n).card = n

theorem Algebraic.Cutwidth.MultiOutput.Internal.mem_xCoords {n : ℕ} {k : Fin (n + n)} : k ∈ xCoords n ↔ ∃ (j : Fin n), Fin.castAdd n j = k

theorem Algebraic.Cutwidth.MultiOutput.Internal.inputsIn_inter_xCoords {n s : ℕ} (S : Finset (Wire (n + n) s)) : SingleCut.inputsIn S ∩ xCoords n = Finset.map (Fin.castAddEmb n) {j : Fin n | Wire.input (Fin.castAdd n j) ∈ S}

The first-factor inputs placed in S, as coordinates of all inputs.

Fixing one factor

theorem Algebraic.Cutwidth.MultiOutput.Internal.fieldMul_eq {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (z : Fin (n + n) → F) : fieldMul b z = b.equivFun ((b.equivFun.symm fun (j : Fin n) => z (Fin.castAdd n j)) * b.equivFun.symm fun (j : Fin n) => z (Fin.natAdd n j))

theorem Algebraic.Cutwidth.MultiOutput.Internal.fieldMul_append {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (x y : Fin n → F) : fieldMul b (Fin.append x y) = b.equivFun (b.equivFun.symm x * b.equivFun.symm y)

theorem Algebraic.Cutwidth.MultiOutput.Internal.fieldMul_append_equivFun {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (u v : K) : fieldMul b (Fin.append (b.equivFun u) (b.equivFun v)) = b.equivFun (u * v)

Multiplication in coordinates multiplies.

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.shiftLeft {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (y₀ : Fin n → F) (d : Fin (n + n) → F) : Fin n → F

The change of the product when the input changes by d and the second factor has the coordinates y₀.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.shiftLeft b y₀ d = b.equivFun ((b.equivFun.symm fun (j : Fin n) => d (Fin.castAdd n j)) * b.equivFun.symm y₀)

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.shiftRight {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (x₀ : Fin n → F) (d : Fin (n + n) → F) : Fin n → F

The change of the product when the input changes by d and the first factor has the coordinates x₀.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.shiftRight b x₀ d = b.equivFun (b.equivFun.symm x₀ * b.equivFun.symm fun (j : Fin n) => d (Fin.natAdd n j))

theorem Algebraic.Cutwidth.MultiOutput.Internal.fieldMul_sub_left {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (y₀ : Fin n → F) (z z' : Fin (n + n) → F) (hz : ∀ k ∉ xCoords n, z k = Fin.append 0 y₀ k) (hz' : ∀ k ∉ xCoords n, z' k = Fin.append 0 y₀ k) : fieldMul b z' - fieldMul b z = shiftLeft b y₀ (z' - z)

With the second factor fixed, the product changes by shiftLeft.

theorem Algebraic.Cutwidth.MultiOutput.Internal.fieldMul_sub_right {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (x₀ : Fin n → F) (z z' : Fin (n + n) → F) (hz : ∀ k ∉ yCoords n, z k = Fin.append x₀ 0 k) (hz' : ∀ k ∉ yCoords n, z' k = Fin.append x₀ 0 k) : fieldMul b z' - fieldMul b z = shiftRight b x₀ (z' - z)

With the first factor fixed, the product changes by shiftRight.

theorem Algebraic.Cutwidth.MultiOutput.Internal.equivFun_symm_single {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (j : Fin n) : b.equivFun.symm (Pi.single j 1) = b j

theorem Algebraic.Cutwidth.MultiOutput.Internal.shiftLeft_single {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (y₀ : Fin n → F) (j : Fin n) : shiftLeft b y₀ (Pi.single (Fin.castAdd n j) 1) = b.equivFun (b j * b.equivFun.symm y₀)

A unit vector on a first-factor input shifts the product by b j times the second factor.

theorem Algebraic.Cutwidth.MultiOutput.Internal.shiftRight_single {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (x₀ : Fin n → F) (j : Fin n) : shiftRight b x₀ (Pi.single (Fin.natAdd n j) 1) = b.equivFun (b.equivFun.symm x₀ * b j)

A unit vector on a second-factor input shifts the product by the first factor times b j.

theorem Algebraic.Cutwidth.MultiOutput.Internal.shiftLeft_single_apply {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (j i : Fin n) : shiftLeft b (b.equivFun ((b j)⁻¹ * b i)) (Pi.single (Fin.castAdd n j) 1) i = 1

Every block entry can be made nonzero: with the second factor (b j)⁻¹ * b i, the unit vector on the first-factor input j shifts output i by one.

theorem Algebraic.Cutwidth.MultiOutput.Internal.shiftRight_single_apply {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (j i : Fin n) : shiftRight b (b.equivFun (b i * (b j)⁻¹)) (Pi.single (Fin.natAdd n j) 1) i = 1

With the first factor b i * (b j)⁻¹, the unit vector on the second-factor input j shifts output i by one.

Averaging the fixed factor

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_filter_forall_eq_zero {n : ℕ} {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (Q : Finset (Fin n)) : {u : Fin n → F | ∀ i ∈ Q, u i = 0}.card = Fintype.card F ^ Qᶜ.card

The vectors vanishing on Q number |F| ^ |Qᶜ|.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_filter_shiftLeft_eq {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) {d : Fin (n + n) → F} (hd : (b.equivFun.symm fun (j : Fin n) => d (Fin.castAdd n j)) ≠ 0) (Q : Finset (Fin n)) : {y₀ : Fin n → F | ∀ i ∈ Q, shiftLeft b y₀ d i = 0}.card = Fintype.card F ^ Qᶜ.card

For a vector d whose first-factor part is a nonzero element, exactly |F| ^ |Qᶜ| second factors put it in the kernel on the rows Q.

theorem Algebraic.Cutwidth.MultiOutput.Internal.sum_card_supportedKernel_le {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (P : Finset (Fin (n + n))) (hP : P ⊆ xCoords n) (Q : Finset (Fin n)) : ∑ y₀ : Fin n → F, (supportedKernel (shiftLeft b y₀) P Q).card ≤ Fintype.card F ^ n + Fintype.card F ^ P.card * Fintype.card F ^ Qᶜ.card

Averaging over the fixed factor. For P within the first factor, the kernels on P and Q number at most |F| ^ n + |F| ^ |P| · |F| ^ |Qᶜ| in total over all second factors.

theorem Algebraic.Cutwidth.MultiOutput.Internal.sum_card_supportedKernel_le_two_mul {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (P : Finset (Fin (n + n))) (hP : P ⊆ xCoords n) (Q : Finset (Fin n)) (hPQ : P.card ≤ Q.card) : ∑ y₀ : Fin n → F, (supportedKernel (shiftLeft b y₀) P Q).card ≤ 2 * Fintype.card F ^ n

When |P| ≤ |Q|, the kernels number at most 2 |F| ^ n in total.

theorem Algebraic.Cutwidth.MultiOutput.Internal.exists_card_add_card_le_four {n : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (P₁ P₂ : Finset (Fin (n + n))) (hP₁ : P₁ ⊆ xCoords n) (hP₂ : P₂ ⊆ xCoords n) (Q₁ Q₂ : Finset (Fin n)) (h₁ : P₁.card ≤ Q₁.card) (h₂ : P₂.card ≤ Q₂.card) : ∃ (y₀ : Fin n → F), (supportedKernel (shiftLeft b y₀) P₁ Q₁).card + (supportedKernel (shiftLeft b y₀) P₂ Q₂).card ≤ 4

Some fixed factor makes two kernels small. If |P₁| ≤ |Q₁| and |P₂| ≤ |Q₂|, some second factor makes the two kernels number at most 4 together.

The cut bound

theorem Algebraic.Cutwidth.MultiOutput.Internal.le_add_two_of_trace {σ : Signature} {n s : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (p : Program σ (n + n) s) (I : Interpretation σ F) (out : Fin n → Wire (n + n) s) (hf : ∀ (z : Fin (n + n) → F) (i : Fin n), p.trace I z (out i) = fieldMul b z i) (S : Finset (Wire (n + n) s)) (hS : {j : Fin n | Wire.input (Fin.castAdd n j) ∈ S}.card + (outputsIn out S).card = n) : n ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card + 2

The cut bound for multiplication. If the wires out of a program carry fieldMul b, every split holding a inputs of the first factor and n - a outputs is crossed by at least n - 2 signals.

One component and distinct terminals

theorem Algebraic.Cutwidth.MultiOutput.Internal.mem_component_of_trace {σ : Signature} {n s : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (hn : 0 < n) (p : Program σ (n + n) s) (I : Interpretation σ F) (out : Fin n → Wire (n + n) s) (hf : ∀ (z : Fin (n + n) → F) (i : Fin n), p.trace I z (out i) = fieldMul b z i) : (∀ (k : Fin (n + n)), Wire.input k ∈ component p (out ⟨0, hn⟩)) ∧ ∀ (i : Fin n), out i ∈ component p (out ⟨0, hn⟩)

All inputs and outputs lie in one component. If the wires out of a program carry fieldMul b and n ≥ 1, the component of the first output contains every input and every output.

theorem Algebraic.Cutwidth.MultiOutput.Internal.out_injective {σ : Signature} {n s : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (p : Program σ (n + n) s) (I : Interpretation σ F) (out : Fin n → Wire (n + n) s) (hf : ∀ (z : Fin (n + n) → F) (i : Fin n), p.trace I z (out i) = fieldMul b z i) : Function.Injective out

A program carrying fieldMul b carries distinct outputs on distinct wires: with the second factor 1, the outputs are the coordinates of the first factor.

theorem Algebraic.Cutwidth.MultiOutput.Internal.out_ne_input {σ : Signature} {n s : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (p : Program σ (n + n) s) (I : Interpretation σ F) (out : Fin n → Wire (n + n) s) (hf : ∀ (z : Fin (n + n) → F) (i : Fin n), p.trace I z (out i) = fieldMul b z i) (i j : Fin n) : out i ≠ Wire.input (Fin.castAdd n j)

No output of a program carrying fieldMul b is an input of the first factor: with the second factor 0, every output is zero.

def Algebraic.Cutwidth.MultiOutput.Internal.terminal {n s : ℕ} (out : Fin n → Wire (n + n) s) : Fin n ⊕ Fin n → Wire (n + n) s

The terminals: the inputs of the first factor, then the outputs.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.terminal out = Sum.elim (fun (j : Fin n) => Cslib.Circuits.Wire.input (Fin.castAdd n j)) out

theorem Algebraic.Cutwidth.MultiOutput.Internal.terminal_injective {σ : Signature} {n s : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) (p : Program σ (n + n) s) (I : Interpretation σ F) (out : Fin n → Wire (n + n) s) (hf : ∀ (z : Fin (n + n) → F) (i : Fin n), p.trace I z (out i) = fieldMul b z i) : Function.Injective (terminal out)

Distinct terminals lie on distinct wires.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_filter_terminal {n s : ℕ} (out : Fin n → Wire (n + n) s) (q : Wire (n + n) s → Prop) [DecidablePred q] : {a : Fin n ⊕ Fin n | q (terminal out a)}.card = {j : Fin n | q (Wire.input (Fin.castAdd n j))}.card + {i : Fin n | q (out i)}.card

Counting terminals splits into first-factor inputs and outputs.

The finite bound

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_terminal_prefixBelow_succ_le {n s : ℕ} (rank : Wire (n + n) s → ℕ) (hrank : Function.Injective rank) (out : Fin n → Wire (n + n) s) (hterm : Function.Injective (terminal out)) (t : ℕ) : {a : Fin n ⊕ Fin n | rank (terminal out a) < t + 1}.card ≤ {a : Fin n ⊕ Fin n | rank (terminal out a) < t}.card + 1

theorem Algebraic.Cutwidth.MultiOutput.Internal.sub_two_le_of_trace {σ : Signature} {n s : ℕ} {F : Type u_1} {K : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Field K] [Algebra F K] (b : Module.Basis (Fin n) F K) {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) (p : Program σ (n + n) s) (hp : p.FanInAtMost 2) (I : Interpretation σ F) (out : Fin n → Wire (n + n) s) (hf : ∀ (z : Fin (n + n) → F) (i : Fin n), p.trace I z (out i) = fieldMul b z i) : ↑n - 2 ≤ (A + η) * max (↑s - 2 * ↑n) 0 + 3 * Real.logb 2 (2 * ↑n + 3 * ↑s) + C

The finite bound for multiplication. A fan-in-two program over any signature whose wires out carry fieldMul b has n - 2 ≤ (A + η) (s - 2 n)⁺ + 3 log₂ (2 n + 3 s) + C.

Asymptotics

theorem Algebraic.Cutwidth.MultiOutput.Internal.eventually_lt_size_of_orderingBound_fieldMul {A : ℝ} (hA : 0 < A) (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound A η C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (F : Type u) [inst : Field F] [Fintype F] (K : Type w) [inst_2 : Field K] [inst_3 : Algebra F K] (b : Module.Basis (Fin n) F K) (σ : Signature) (I : Interpretation σ F) (c : Circuit σ (n + n) n), c.FanInAtMost 2 → c.Computes I (fieldMul b) → (2 + 1 / A - ε) * ↑n < ↑c.size

The asymptotic bound for multiplication with a general ordering coefficient.