Restricted splits #
The fibre bound of MultiOutput.Rank counts all inputs of a circuit. This file restricts it to
a set of inputs, which bounds circuits for maps that are linear only once some inputs are
fixed, such as multiplication with one factor fixed.
The product-domain fibre bound (card_piFinset_le_of_fibres). Split the wires of a circuit
computing f into S and its complement, with forward signals A and backward signals B.
For a coordinatewise product domain D = D₀ × ⋯ × D_{n-1}, if every left fibre taken within
D has at most DT elements and every right fibre within D at most DS, then
|D| ≤ |U| ^ (|A| + |B|) · DT · DS. More generally this holds for every set of inputs closed
under the mixing of SingleCut.mix (card_le_of_fibres_of_mix_of_trace): the proof of the
unrestricted bound only mixes two inputs, and mixing two members of a product stays in it.
The kernel form (card_pow_le_supportedKernel). Fix the inputs outside a set J of free
coordinates to a base point z₀. If on these inputs the function changes by g d whenever the
input changes by d, then every split satisfies
|U| ^ |J| ≤ |U| ^ (|A| + |B|) · |ker₁| · |ker₂|, where ker₁ = supportedKernel g X_S Y_T
consists of the vectors supported on the free inputs X_S placed in S whose image vanishes
on the outputs Y_T carried outside S, and ker₂ = supportedKernel g X_T Y_S. For a linear
g these are kernels of blocks, and the bound is the rank-cut bound
rank g[Y_T, X_S] + rank g[Y_S, X_T] ≤ |A| + |B| restricted to the free inputs.
Closed sets separate (apply_eq_zero_of_closed_of_trace). For a split crossed by no
signal, both kernels are full: g maps vectors supported on X_S to vectors vanishing on
Y_T, and vectors supported on X_T to vectors vanishing on Y_S.
Sets closed under mixing #
The fibre bound on a set closed under mixing, for a program. If the wires out of a
program carry f and Z is closed under mixing for the split S, 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.
The product-domain fibre bound. If a circuit computes f, and for a split S and a
coordinatewise product domain D every left fibre taken within D has at most DT elements
and every right fibre within D at most DS, then |D| ≤ |U| ^ (|A| + |B|) · DT · DS.
The kernel form #
A kernel has at most |U| ^ |P| vectors supported on P.
The forward restricted rank-cut bound, kernel form, for a program. If the wires out
of a program carry f, and on the inputs agreeing with z₀ off J the function changes by
g d when its input changes by d, then every split S satisfies
|U| ^ |X_S| ≤ |U| ^ |A| · |supportedKernel g X_S Y_T|, using only the forward signals
A = forward p S.
The backward restricted rank-cut bound, kernel form, for a program. Symmetrically,
|U| ^ |X_T| ≤ |U| ^ |B| · |supportedKernel g X_T Y_S|, using only the backward signals
B = backward p S.
The restricted rank-cut bound, kernel form, for a program. If the wires out of a
program carry f, and on the inputs agreeing with z₀ off J the function changes by g d
when its input changes by d, then every split S satisfies
|U| ^ |J| ≤ |U| ^ (|A| + |B|) · |supportedKernel g X_S Y_T| · |supportedKernel g X_T Y_S|,
where X_S and X_T are the free inputs in S and outside S, and Y_S and Y_T the
outputs carried in S and outside S.
The forward restricted rank-cut bound, kernel form. If a circuit computes f, and on
the inputs agreeing with z₀ off J the function changes by g d when its input changes by
d, then every split S of its wires satisfies
|U| ^ |X_S| ≤ |U| ^ |A| · |supportedKernel g X_S Y_T|.
The backward restricted rank-cut bound, kernel form. Symmetrically,
|U| ^ |X_T| ≤ |U| ^ |B| · |supportedKernel g X_T Y_S|.
The restricted rank-cut bound, kernel form. If a circuit computes f, and on the
inputs agreeing with z₀ off J the function changes by g d when its input changes by d,
then every split S of its wires satisfies
|U| ^ |J| ≤ |U| ^ (|A| + |B|) · |supportedKernel g X_S Y_T| · |supportedKernel g X_T Y_S|.
Zero forward cut separates left inputs from outside outputs. If a split S has no
forward signals, g maps every vector supported on the free inputs in S to a vector
vanishing on the outputs carried outside S.
Zero backward cut separates outside inputs from inside outputs. Symmetrically, if a
split S has no backward signals, g maps every vector supported on the free inputs outside
S to a vector vanishing on the outputs carried in S.
Closed sets separate. If the wires out of a program carry f, the function changes
by g d when its input changes by d on the inputs agreeing with z₀ off J, and a split
S has no forward and no backward signals, then g maps every vector supported on the free
inputs in S to a vector vanishing on the outputs carried outside S, and every vector
supported on the free inputs outside S to a vector vanishing on the outputs carried in
S.