Fusion lower bounds for cyclic set circuits

A cyclic circuit is a finite system of AND/OR equations whose gates may refer to any other gate. Its semantics is the least fixed point of the induced monotone operator, equivalently the limit obtained by iterating from the empty state. We package the least-fixed-point property explicitly; a later module can construct this package from an iteration procedure without changing the fusion argument.

At a semantic solution, every AND equation contributes the pair of its two operand sets restricted to the target complement. The leastness condition is exactly what prevents an unsupported cycle from manufacturing a target point. Consequently these pairs cover every semi-filter above the target, and their number is exactly the cyclic circuit's AND cost.

structure Algebraic.Fusion.CyclicCircuit (σ : Signature) (n g : ℕ) : Type u_1

A system of cyclic circuit equations and a designated output gate.

• lines : Fin g → Line σ n g

  Every gate may read any input or any gate in the same system.

• output : Fin g

  Gate designated as the output.

def Algebraic.Fusion.CyclicCircuit.atomAt {σ : Signature} {n g : ℕ} {U : Type u_2} (circuit : CyclicCircuit σ n g) (inputs : Fin n → U) (state : Fin g → U) (gate : Fin g) : Atom σ U

Semantic atom represented by one cyclic equation at a proposed state.

Equations

• circuit.atomAt inputs state gate = { op := (circuit.lines gate).op, arguments := Cslib.Circuits.Wire.elim inputs state ∘ (circuit.lines gate).wires }

@[simp]

theorem Algebraic.Fusion.CyclicCircuit.atomAt_result {σ : Signature} {n g : ℕ} {U : Type u_2} (circuit : CyclicCircuit σ n g) (interpretation : Interpretation σ U) (inputs : Fin n → U) (state : Fin g → U) (gate : Fin g) : (circuit.atomAt inputs state gate).result interpretation = (circuit.lines gate).eval interpretation inputs state

The result of a cyclic atom is the corresponding line evaluated in the same state.

def Algebraic.Fusion.CyclicCircuit.IsPrefixed {σ : Signature} {n g : ℕ} {U : Type u_2} (circuit : CyclicCircuit σ n g) [LE U] (interpretation : Interpretation σ U) (inputs : Fin n → U) (state : Fin g → U) : Prop

A state is pre-fixed when every equation result is below its assigned gate value.

Equations

• circuit.IsPrefixed interpretation inputs state = ∀ (gate : Fin g), (circuit.atomAt inputs state gate).result interpretation ≤ state gate

structure Algebraic.Fusion.CyclicCircuit.Constructs {U : Type u_1} {σ : Signature} {g : ℕ} {problem : Problem U} (circuit : CyclicCircuit σ problem.inputCount g) [LE U] (interpretation : Interpretation σ U) : Type u_1

Proof-carrying least-fixed-point construction of a target value.

• values : Fin g → U

  Least semantic solution of the cyclic equations.

• fixed (gate : Fin g) : self.values gate = (circuit.atomAt problem.inputs self.values gate).result interpretation

  Every gate value satisfies its equation exactly.

• least (candidate : Fin g → U) : circuit.IsPrefixed interpretation problem.inputs candidate → ∀ (gate : Fin g), self.values gate ≤ candidate gate

  The solution lies below every pre-fixed state.

• output_eq : self.values circuit.output = problem.target

  The designated gate has the requested target value.

def Algebraic.Fusion.CyclicCircuit.atoms {σ : Signature} {n g : ℕ} {U : Type u_2} (circuit : CyclicCircuit σ n g) (inputs : Fin n → U) (state : Fin g → U) : List (Atom σ U)

Semantic atoms of all cyclic equations.

Equations

• circuit.atoms inputs state = List.ofFn (circuit.atomAt inputs state)

@[simp]

theorem Algebraic.Fusion.CyclicCircuit.atomAt_mem_atoms {σ : Signature} {n g : ℕ} {U : Type u_2} (circuit : CyclicCircuit σ n g) (inputs : Fin n → U) (state : Fin g → U) (gate : Fin g) : circuit.atomAt inputs state gate ∈ circuit.atoms inputs state

def Algebraic.Fusion.CyclicCircuit.cost {σ : Signature} {n g : ℕ} (circuit : CyclicCircuit σ n g) (operationCost : OperationCost σ) : ℕ

Weighted cost of all cyclic equations.

Equations

• circuit.cost operationCost = (List.ofFn fun (gate : Fin g) => operationCost (circuit.lines gate).op).sum

theorem Algebraic.Fusion.CyclicCircuit.atoms_cost {σ : Signature} {n g : ℕ} {U : Type u_2} (circuit : CyclicCircuit σ n g) (inputs : Fin n → U) (state : Fin g → U) (operationCost : OperationCost σ) : Atom.listCost (circuit.atoms inputs state) operationCost = circuit.cost operationCost

Semantic cyclic atoms have exactly the syntactic equation cost.

theorem Algebraic.Fusion.CyclicCircuit.atomAt_mono {n g : ℕ} {Γ : Type u_1} (circuit : CyclicCircuit AndOr.signature n g) (inputs : Fin n → Set Γ) {lower upper : Fin g → Set Γ} (stateSubset : ∀ (gate : Fin g), lower gate ⊆ upper gate) (gate : Fin g) : (circuit.atomAt inputs lower gate).result (AndOr.setInterpretation Γ) ⊆ (circuit.atomAt inputs upper gate).result (AndOr.setInterpretation Γ)

AND/OR cyclic equations are monotone in their gate state.

noncomputable def Algebraic.Fusion.pairCoverOfCyclic {Γ : Type u_1} {g : ℕ} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (circuit : CyclicCircuit AndOr.signature problem.inputCount g) (constructs : circuit.Constructs (AndOr.setInterpretation Γ)) : PairCover problem admissible

Every least-fixed-point cyclic construction yields a semi-filter pair cover with one pair per AND equation.

Equations

• Algebraic.Fusion.pairCoverOfCyclic problem admissible circuit constructs = { pairs := Algebraic.Fusion.intersectionPairs problem (circuit.atoms problem.inputs constructs.values), isCover := ⋯ }

theorem Algebraic.Fusion.pairCoverOfCyclic_cost {Γ : Type u_1} {g : ℕ} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (circuit : CyclicCircuit AndOr.signature problem.inputCount g) (constructs : circuit.Constructs (AndOr.setInterpretation Γ)) : (pairCoverOfCyclic problem admissible circuit constructs).cost = circuit.cost AndOr.andCost

The cyclicly extracted pair cover has exactly the circuit's AND cost.

theorem Algebraic.Fusion.cyclic_pairCover_lowerBound {Γ : Type u_1} {L g : ℕ} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (coverLowerBound : ∀ (cover : PairCover problem admissible), L ≤ cover.cost) (circuit : CyclicCircuit AndOr.signature problem.inputCount g) (constructs : circuit.Constructs (AndOr.setInterpretation Γ)) : L ≤ circuit.cost AndOr.andCost

Every semi-filter pair-cover lower bound applies to least-fixed-point cyclic circuits.

noncomputable def Algebraic.Fusion.andOrCyclicComplexity {Γ : Type u_1} (problem : SetProblem Γ) : ℕ∞

Least AND cost of a binary AND/OR cyclic construction.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Fusion.andOrCyclicComplexity_le {Γ : Type u_1} {g : ℕ} (problem : SetProblem Γ) (circuit : CyclicCircuit AndOr.signature problem.inputCount g) (constructs : circuit.Constructs (AndOr.setInterpretation Γ)) : andOrCyclicComplexity problem ≤ ↑(circuit.cost AndOr.andCost)

Every concrete binary cyclic construction upper-bounds its complexity.

theorem Algebraic.Fusion.pairCoverComplexity_le_andOrCyclicComplexity {Γ : Type u_1} (problem : SetProblem Γ) : pairCoverComplexity problem ≤ andOrCyclicComplexity problem

Pair-cover complexity is no larger than binary cyclic AND complexity.