Field-independent rank bounds from local linear realizations #
Across a wire cut, every exterior row restricted to the interior primary inputs lies in the span of the forward signal rows. The two directed block ranks are therefore bounded by their respective signal counts, over any field.
theorem
Algebraic.Cutwidth.MultiOutput.Linear.Realization.restrict_mem_span_forward
{σ : Signature}
{F : Type u_1}
[Field F]
{n s : ℕ}
{p : Program σ n s}
(r : Realization p F)
(S : Finset (Wire n s))
(wire : Wire n s)
(outside : wire ∉ S)
:
(fun (j : ↥(SingleCut.inputsIn S)) => r.value wire ↑j) ∈ Submodule.span F (Set.range fun (w : ↥(SingleCut.forward p S)) (j : ↥(SingleCut.inputsIn S)) => r.value ↑w ↑j)
An exterior wire's interior-input coefficients are generated by the forward signals.
theorem
Algebraic.Cutwidth.MultiOutput.Linear.Realization.blockRank_le_forward
{σ : Signature}
{F : Type u_1}
[Field F]
{n s m : ℕ}
{p : Program σ n s}
(r : Realization p F)
(out : Fin m → Wire n s)
(M : Matrix (Fin m) (Fin n) F)
(rows : ∀ (i : Fin m), r.value (out i) = M i)
(S : Finset (Wire n s))
:
One directed matrix block has rank at most the number of forward signals.
theorem
Algebraic.Cutwidth.MultiOutput.Linear.Realization.blockRank_le_backward
{σ : Signature}
{F : Type u_1}
[Field F]
{n s m : ℕ}
{p : Program σ n s}
(r : Realization p F)
(out : Fin m → Wire n s)
(M : Matrix (Fin m) (Fin n) F)
(rows : ∀ (i : Fin m), r.value (out i) = M i)
(S : Finset (Wire n s))
:
The opposite directed block is bounded by the backward signals.
theorem
Algebraic.Cutwidth.MultiOutput.Linear.Realization.blockRank_add_blockRank_le
{σ : Signature}
{F : Type u_1}
[Field F]
{n s m : ℕ}
{p : Program σ n s}
(r : Realization p F)
(out : Fin m → Wire n s)
(M : Matrix (Fin m) (Fin n) F)
(rows : ∀ (i : Fin m), r.value (out i) = M i)
(S : Finset (Wire n s))
:
blockRank M (outputsIn out S)ᶜ (SingleCut.inputsIn S) + blockRank M (outputsIn out S) (SingleCut.inputsIn S)ᶜ ≤ (SingleCut.forward p S).card + (SingleCut.backward p S).card
Local linear coefficients give the rank-cut inequality over arbitrary fields.
theorem
Algebraic.Cutwidth.MultiOutput.Linear.Realization.outputs_injective
{σ : Signature}
{F : Type u_1}
[Field F]
{n s : ℕ}
{p : Program σ n s}
(r : Realization p F)
(out : Fin n → Wire n s)
{M : Matrix (Fin n) (Fin n) F}
(regular : TotallyRegular M)
(rows : ∀ (i : Fin n), r.value (out i) = M i)
:
A totally regular square output matrix requires distinct original output wires.