Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Aggregate.Geometry.Affine.Shared.Relative

Pairing after some primary coordinates have been fixed #

The affine restriction argument starts on any affine flat. Its charge subtracts outputs already constant there, including gates not yet reached in topological order. Only conjunctions with two remaining primary coordinates need single charges.

source
def Algebraic.Aggregate.Geometry.Shared.remainingMark {n g : ℕ} (line : Line signature n g) (fixed : Finset (Fin n)) :
Bool

A conjunction still having at least two primary coordinates outside the fixed set.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algebraic.Aggregate.Geometry.Shared.remainingCount {n g : ℕ} :
    Program signature n g → Finset (Fin n) → ℕ

    Number of conjunctions still having at least two unfixed primary coordinates.

    Equations
    Instances For
      source
      theorem Algebraic.Aggregate.Geometry.Shared.affineOn_line_of_remaining_small {n g : ℕ} (p : Program signature n g) (line : Line signature n g) (S : AffineFlat n) (fixed : Finset (Fin n)) (fixedOn : ∀ i ∈ fixed, ConstantOn S fun (x : Fin n → Bool) => x i) (small : (primaryInputs line \ fixed).card ≤ 1) (constant : ∀ (slot : Fin (signature.Arity line.op)) (i : Fin g), line.wires slot = Wire.gate i → ConstantOn S (p.gateFunction interpretation i)) :
      AffineOn S (lineFunction p line)

      Fixed primary coordinates and constant internal predecessors can be omitted when checking whether a line depends on at most one variable.

      source
      theorem Algebraic.Aggregate.Geometry.Shared.exists_affine_restriction {n g : ℕ} (p : Program signature n g) (S : AffineFlat n) (fixed : Finset (Fin n)) (fixedOn : ∀ i ∈ fixed, ConstantOn S fun (x : Fin n → Bool) => x i) :
      ∃ (T : AffineFlat n) (d : ℕ), T.carrier ⊆ S.carrier ∧ (∀ (i : Fin g), AffineOn T (p.gateFunction interpretation i)) ∧ 2 ^ d * T.carrier.card = S.carrier.card ∧ 2 * d + constantCount p S ≤ constantCount p T + remainingCount p fixed

      Affine elimination from an arbitrary initial flat charges only new constants and conjunctions with at least two still-unfixed primary variables.