Proofs for restricted splits #
The fibre bound of MultiOutput.Rank sums over all inputs. Its proof only mixes inputs with
equal boundary keys, so it holds for any set Z of inputs closed under mixing
(card_le_of_fibres_of_mix): the members of Z with a fixed key are a product of left and
right parts, and the left parts embed into the left fibre of any member taken within Z.
Coordinatewise products are closed under mixing (mix_mem_piFinset), and so is the slice
of inputs agreeing with a base point z₀ off a set J of free coordinates (slice).
On a slice, if the function changes by g d when the input changes by d, a left fibre minus
its base point consists of vectors supported on the free inputs placed in S whose image
vanishes on the outputs carried outside S (card_inter_leftFibre_le). As the slice has
|U| ^ |J| members (card_slice), this gives card_pow_le_supportedKernel. For a closed set
both kernels must then be full, so g maps vectors supported on one side to vectors vanishing
on the outputs of the other side (apply_eq_zero_of_closed).
The fibre bound on a set closed under mixing #
The left parts of a fibre within Z embed into the left fibre, within Z, of any of its
members.
The right parts of a fibre within Z embed into the right fibre, within Z, of any of its
members.
The fibre bound on a set closed under mixing. If Z is closed under mixing, every
left fibre within Z has at most DT elements and every right fibre within Z at most DS,
then |Z| ≤ |U| ^ (|A| + |B|) · DT · DS.
Coordinatewise products are closed under mixing.
Slices #
The inputs agreeing with z₀ on every coordinate outside J.
Equations
- Algebraic.Cutwidth.MultiOutput.Internal.slice J z₀ = {z : Fin n → U | ∀ k ∉ J, z k = z₀ k}
Instances For
A slice has |U| ^ |J| members.
One-sided forward fibre bound on a slice. On the slice of inputs agreeing with z₀
outside J, if every left fibre within slice J z₀ has at most DT elements, then
|U| ^ |inputsIn S ∩ J| ≤ |U| ^ |forward p S| · DT.
One-sided backward fibre bound on a slice. On the slice of inputs agreeing with z₀
outside J, if every right fibre within slice J z₀ has at most DS elements, then
|U| ^ |(inputsIn S)ᶜ ∩ J| ≤ |U| ^ |backward p S| · DS.
Kernels on a slice #
Kernel vectors are supported vectors, so there are at most |U| ^ |P| of them.
A supported vector whose image does not vanish on Q leaves the kernel short.
Left fibres on a slice. Subtracting the base point maps a left fibre within the slice
injectively into the vectors supported on the free inputs in S whose image vanishes on the
outputs carried outside S.
Right fibres on a slice.
The one-sided forward kernel bound on a slice. If the wires out carry f, and on the
slice of inputs agreeing with z₀ off J the function changes by g d when its input changes
by d, then every split S satisfies
|U| ^ |inputsIn S ∩ J| ≤ |U| ^ |forward p S| · |supportedKernel g (inputsIn S ∩ J) Y_T|.
The one-sided backward kernel bound on a slice. Symmetrically,
|U| ^ |(inputsIn S)ᶜ ∩ J| ≤ |U| ^ |backward p S| · |supportedKernel g ((inputsIn S)ᶜ ∩ J) Y_S|.
The kernel form of the restricted rank-cut bound. If the wires out carry f, and on
the slice of inputs agreeing with z₀ off J the function changes by g d when its input
changes by d, then every split satisfies
|U| ^ |J| ≤ |U| ^ (|A| + |B|) · |ker₁| · |ker₂|, where ker₁ consists of the vectors
supported on the free inputs in S whose image vanishes on the outputs outside S, and
ker₂ symmetrically.
No forward signals separate. If forward p S = ∅, then g maps vectors supported on
the free inputs in S to vectors vanishing on the outputs carried outside S.
No backward signals separate. If backward p S = ∅, then g maps vectors supported on
the free inputs outside S to vectors vanishing on the outputs carried in S.
Closed sets separate. If a split has no forward and no backward signals, then g maps
vectors supported on the free inputs in S to vectors vanishing on the outputs carried outside
S, and vectors supported on the free inputs outside S to vectors vanishing on the outputs
carried in S.