Algebra-generic fusion lower bounds

Fusion arguments turn the gates of a concrete computation into a static cover of a family of observations. This file contains the part of that argument which is independent of Boolean sets, semi-filters, or any particular circuit basis.

An observation compares two predicates on every semantic value: a reference predicate and an observed predicate. Inputs satisfy the implication from the reference predicate to the observed predicate, while the target violates it. Consequently, every circuit constructing the target contains a gate at which that implication is not preserved. The resulting local gate configurations cover all observations, and their total weight is exactly the circuit cost.

structure Algebraic.Fusion.Problem (U : Type u) : Type u

A fixed algebraic construction problem: construct target from inputs.

• inputCount : ℕ

  Number of available generators.

• inputs : Fin self.inputCount → U

  The generators available as circuit inputs.

• target : U

  The value to be constructed.

structure Algebraic.Fusion.Atom (σ : Signature) (U : Type u) : Type (max u u_1)

One operation together with the semantic values supplied to its arguments.

• op : σ.Op

  Operation performed at the gate.

• arguments : Fin (σ.Arity self.op) → U

  Semantic value supplied to each argument.

def Algebraic.Fusion.Atom.result {σ : Signature} {U : Type u_2} (atom : Atom σ U) (interpretation : Interpretation σ U) : U

The semantic result of a fusion atom.

Equations

• atom.result interpretation = interpretation atom.op atom.arguments

def Algebraic.Fusion.Atom.cost {σ : Signature} {U : Type u_2} (atom : Atom σ U) (operationCost : OperationCost σ) : ℕ

The weight of one fusion atom.

Equations

• atom.cost operationCost = operationCost atom.op

def Algebraic.Fusion.Atom.listCost {σ : Signature} {U : Type u_2} (atoms : List (Atom σ U)) (operationCost : OperationCost σ) : ℕ

Total weight of a list of fusion atoms.

Equations

• Algebraic.Fusion.Atom.listCost atoms operationCost = (List.map (fun (atom : Algebraic.Fusion.Atom σ U) => atom.cost operationCost) atoms).sum

@[simp]

theorem Algebraic.Fusion.Atom.listCost_nil {σ : Signature} {U : Type u_2} (operationCost : OperationCost σ) : listCost [] operationCost = 0

@[simp]

theorem Algebraic.Fusion.Atom.listCost_append {σ : Signature} {U : Type u_2} (left right : List (Atom σ U)) (operationCost : OperationCost σ) : listCost (left ++ right) operationCost = listCost left operationCost + listCost right operationCost

@[simp]

theorem Algebraic.Fusion.Atom.listCost_singleton {σ : Signature} {U : Type u_2} (atom : Atom σ U) (operationCost : OperationCost σ) : listCost [atom] operationCost = atom.cost operationCost

structure Algebraic.Fusion.Model {σ : Signature} {U : Type u_2} (operationCost : OperationCost σ) (interpretation : Interpretation σ U) (problem : Problem U) : Type (max u_2 (w + 1))

An observation model for one construction problem. A witness supplies a reference predicate and an observed predicate on semantic values. Every input is sound for every witness, whereas the target is reference-true and observed-false.

The model deliberately imposes no Boolean or order structure on U. For set-theoretic fusion, witnesses will be points equipped with semi-filters. For arithmetic circuits they can instead be linear, rank, derivative, or other algebraic observations.

• Witness : Type w

  Observations which every proposed cover must exclude.

• reference : self.Witness → U → Prop

  The reference view of a semantic value.

• observed : self.Witness → U → Prop

  The fused or approximating view of a semantic value.

• input_sound (witness : self.Witness) (input : Fin problem.inputCount) : self.reference witness (problem.inputs input) → self.observed witness (problem.inputs input)

  Every generator is sound under every observation.

• target_reference (witness : self.Witness) : self.reference witness problem.target

  The target is true in every reference view.

• target_not_observed (witness : self.Witness) : ¬self.observed witness problem.target

  The target is false in every observed view.

def Algebraic.Fusion.Model.Sound {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) (witness : model.Witness) (value : U) : Prop

The reference-to-observed implication at one semantic value.

Equations

• model.Sound witness value = (model.reference witness value → model.observed witness value)

def Algebraic.Fusion.Atom.PreservedBy {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (atom : Atom σ U) (model : Model operationCost interpretation problem) (witness : model.Witness) : Prop

A witness preserves an atom when sound arguments imply a sound result.

Equations

• atom.PreservedBy model witness = ((∀ (argument : Fin (σ.Arity atom.op)), model.Sound witness (atom.arguments argument)) → model.Sound witness (atom.result interpretation))

def Algebraic.Fusion.Model.IsCover {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) (atoms : List (Atom σ U)) : Prop

A list of atoms covers a model when no witness preserves every atom.

Equations

• model.IsCover atoms = ∀ (witness : model.Witness), ¬∀ atom ∈ atoms, atom.PreservedBy model witness

structure Algebraic.Fusion.Cover {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) : Type (max u u_1)

A proof-carrying finite fusion cover.

• atoms : List (Atom σ U)

  Local gate configurations in the cover.

• isCover : model.IsCover self.atoms

  Every observation is violated by some atom in the list.

def Algebraic.Fusion.Cover.cost {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} (cover : Cover model) : ℕ

Total operation weight of a fusion cover.

Equations

• cover.cost = Algebraic.Fusion.Atom.listCost cover.atoms operationCost

noncomputable def Algebraic.Fusion.Model.coverComplexity {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) : ℕ∞

Minimum weighted cover cost, or ⊤ if no finite cover exists.

Equations

• model.coverComplexity = ⨅ (cover : Algebraic.Fusion.Cover model), ↑cover.cost

theorem Algebraic.Fusion.Model.coverComplexity_le {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) (cover : Cover model) : model.coverComplexity ≤ ↑cover.cost

Every concrete cover upper-bounds minimum cover complexity.

def Algebraic.Fusion.lineAtom {σ : Signature} {n g : ℕ} {U : Type u_2} (line : Line σ n g) (program : Program σ n g) (interpretation : Interpretation σ U) (input : Fin n → U) : Atom σ U

A line evaluated after a prefix program, viewed as a fusion atom.

Equations

• Algebraic.Fusion.lineAtom line program interpretation input = { op := line.op, arguments := program.trace interpretation input ∘ line.wires }

@[simp]

theorem Algebraic.Fusion.lineAtom_op {σ : Signature} {n g : ℕ} {U : Type u_2} (line : Line σ n g) (program : Program σ n g) (interpretation : Interpretation σ U) (input : Fin n → U) : (lineAtom line program interpretation input).op = line.op

theorem Algebraic.Fusion.lineAtom_result {σ : Signature} {n g : ℕ} {U : Type u_2} (line : Line σ n g) (program : Program σ n g) (interpretation : Interpretation σ U) (input : Fin n → U) : (lineAtom line program interpretation input).result interpretation = line.eval interpretation input (program.eval interpretation input)

The result of a line's fusion atom is exactly the line evaluation.

def Algebraic.Fusion.programAtoms {σ : Signature} {U : Type u_2} {n g : ℕ} (interpretation : Interpretation σ U) (input : Fin n → U) (program : Program σ n g) : List (Atom σ U)

Semantic gate configurations of a program, in topological order.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Fusion.programAtoms interpretation input Cslib.Circuits.Program.empty = []

@[simp]

theorem Algebraic.Fusion.programAtoms_empty {σ : Signature} {U : Type u_2} {n : ℕ} (interpretation : Interpretation σ U) (input : Fin n → U) : programAtoms interpretation input Program.empty = []

@[simp]

theorem Algebraic.Fusion.programAtoms_gate {σ : Signature} {n g : ℕ} {U : Type u_2} (program : Program σ n g) (line : Line σ n g) (interpretation : Interpretation σ U) (input : Fin n → U) : programAtoms interpretation input (program.gate line) = programAtoms interpretation input program ++ [lineAtom line program interpretation input]

theorem Algebraic.Fusion.programAtoms_cost {σ : Signature} {n g : ℕ} {U : Type u_2} (program : Program σ n g) (interpretation : Interpretation σ U) (input : Fin n → U) (operationCost : OperationCost σ) : Atom.listCost (programAtoms interpretation input program) operationCost = Program.cost operationCost program

Extracted atoms have exactly the weighted cost of the source program.

theorem Algebraic.Fusion.sound_trace_of_preserves {g : ℕ} {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) (program : Program σ problem.inputCount g) (witness : model.Witness) (preserves : ∀ atom ∈ programAtoms interpretation problem.inputs program, atom.PreservedBy model witness) (wire : Wire problem.inputCount g) : model.Sound witness (program.trace interpretation problem.inputs wire)

If a witness preserves every extracted atom, then every wire in the program is sound for that witness.

def Algebraic.Fusion.Problem.Constructs {U : Type u_1} {σ : Signature} (problem : Problem U) (circuit : Circuit σ problem.inputCount 1) (interpretation : Interpretation σ U) : Prop

A circuit constructs a problem when its sole output is the target value.

Equations

• problem.Constructs circuit interpretation = (circuit.eval interpretation problem.inputs 0 = problem.target)

def Algebraic.Fusion.circuitAtoms {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n → U) : List (Atom σ U)

Semantic gate configurations extracted from a circuit.

Equations

• Algebraic.Fusion.circuitAtoms circuit interpretation input = Algebraic.Fusion.programAtoms interpretation input circuit.program

theorem Algebraic.Fusion.circuitAtoms_cost {σ : Signature} {n m : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (interpretation : Interpretation σ U) (input : Fin n → U) (operationCost : OperationCost σ) : Atom.listCost (circuitAtoms circuit interpretation input) operationCost = circuit.cost operationCost

Extracted circuit atoms have exactly the circuit's weighted cost.

def Algebraic.Fusion.coverOfCircuit {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit interpretation) : Cover model

Every circuit constructing the target supplies a fusion cover.

Equations

• Algebraic.Fusion.coverOfCircuit model circuit constructs = { atoms := Algebraic.Fusion.circuitAtoms circuit interpretation problem.inputs, isCover := ⋯ }

theorem Algebraic.Fusion.coverOfCircuit_cost {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit interpretation) : (coverOfCircuit model circuit constructs).cost = circuit.cost operationCost

The cover extracted from a circuit has exactly the circuit's cost.

theorem Algebraic.Fusion.Model.lowerBound {L : ℕ} {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) (coverLowerBound : ∀ (cover : Cover model), L ≤ cover.cost) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit interpretation) : L ≤ circuit.cost operationCost

A lower bound for every fusion cover is a circuit-cost lower bound.

theorem Algebraic.Fusion.Model.coverComplexity_le_cost {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit interpretation) : model.coverComplexity ≤ ↑(circuit.cost operationCost)

Cover complexity lower-bounds every circuit constructing the target.

structure Algebraic.Fusion.Framework {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} (model : Model operationCost interpretation problem) : Type

A packaged combinatorial lower bound for one fusion model.

• bound : ℕ

  Claimed weighted lower bound.

• coverLowerBound (cover : Cover model) : self.bound ≤ cover.cost

  Every finite fusion cover pays the claimed bound.

theorem Algebraic.Fusion.Framework.lowerBound {σ : Signature} {U : Type u} {operationCost : OperationCost σ} {interpretation : Interpretation σ U} {problem : Problem U} {model : Model operationCost interpretation problem} (framework : Framework model) (circuit : Circuit σ problem.inputCount 1) (constructs : problem.Constructs circuit interpretation) : framework.bound ≤ circuit.cost operationCost

A fusion framework proves its bound for every constructing circuit.