Documentation

Complexity.Computability.Circuit.Boolean.Iteration.SparseDisplacement

Circuits for maps commuting with sparse counter modifications #

If an injective word map h commutes with a map f differing from the binary counter at r inputs, then h has a native De Morgan circuit of at most 100 * (n + 1) * (r + 1) gates. The displacement h x - x changes at at most 2 * r counter edges. A telescoping sum of threshold corrections reconstructs it; comparisons, selectors, additions and constants are all charged. In particular the bound holds for every signed fixed power of a permutation.

These are nonuniform existence results. The correction table is chosen from the whole map; no efficient table-construction algorithm is asserted. A change of coordinates additionally requires circuits for both directions, whose sizes are charged explicitly.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Boolean.Iteration.thresholdSum {w : ℕ} (S : Finset ℕ) (coeff : ℕ → BitVec w) (base x : BitVec w) :
BitVec w

Add the corrections whose thresholds precede the input word.

Instances For
    source
    def Cslib.Circuits.Boolean.Iteration.displacement {n : ℕ} (h : BitVec n → BitVec n) (x : BitVec n) :
    BitVec n

    Word displacement relative to the counter coordinates.

    Instances For
      source
      def Cslib.Circuits.Boolean.Iteration.displacementCuts {n : ℕ} (h : BitVec n → BitVec n) :
      Finset ℕ

      Changes of displacement, including the wraparound edge.

      Instances For
        source
        theorem Cslib.Circuits.Boolean.Iteration.displacement_change_iff {n : ℕ} (h : BitVec n → BitVec n) (x : BitVec n) :
        displacement h (x + 1) ≠ displacement h x ↔ h (x + 1) ≠ h x + 1

        The displacement of h changes across x and x + 1 if and only if h (x + 1) ≠ h x + 1.

        source
        theorem Cslib.Circuits.Boolean.Iteration.thresholdSum_displacement {n : ℕ} (h : BitVec n → BitVec n) (x : BitVec n) :
        thresholdSum (displacementCuts h) (fun (i : ℕ) => displacement h (BitVec.ofNat n (i + 1)) - displacement h (BitVec.ofNat n i)) (displacement h 0) x = displacement h x

        The sparse derivative reconstructs the entire word function by telescoping.

        source
        theorem Cslib.Circuits.Boolean.Iteration.sparse_counter_centralizer {n : ℕ} (f h : BitVec n → BitVec n) (hc : Function.Commute h f) (hi : Function.Injective h) :
        ∃ (out : Circuit signature n n), (out.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => (h (word x)).getLsbD ↑i) ∧ out.size ≤ 100 * (n + 1) * ((FunctionalGraph.disagreement f fun (x : BitVec n) => x + 1).card + 1)

        Every injective map commuting with an r-edited counter has size O(n(r+1)). No transition circuit or state-space enumeration is a hypothesis.

        source
        theorem Cslib.Circuits.Boolean.Iteration.sparse_counter_power {n : ℕ} (f : Equiv.Perm (BitVec n)) (T : ℤ) :
        ∃ (out : Circuit signature n n), (out.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => ((f ^ T) (word x)).getLsbD ↑i) ∧ out.size ≤ 100 * (n + 1) * ((FunctionalGraph.disagreement ⇑f fun (x : BitVec n) => x + 1).card + 1)

        The bound applies uniformly to all signed fixed powers of a permutation.

        source
        theorem Cslib.Circuits.Boolean.Iteration.sparse_coordinate_power {n : ℕ} (f g e : Equiv.Perm (BitVec n)) (hcycle : ∀ (x : BitVec n), e (g x) = e x + 1) (encode decode : Circuit signature n n) (he : encode.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => (e (word x)).getLsbD ↑i) (hd : decode.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => ((Equiv.symm e) (word x)).getLsbD ↑i) (T : ℤ) :
        ∃ (out : Circuit signature n n), (out.Computes interpretation fun (x : Fin n → Bool) (i : Fin n) => ((f ^ T) (word x)).getLsbD ↑i) ∧ out.size ≤ encode.size + decode.size + 100 * (n + 1) * ((FunctionalGraph.disagreement ⇑f ⇑g).card + 1)

        Cheap orbit coordinates transfer the sparse bound, charging both conversion circuits.