Fusion for cyclic finite-join/meet circuits

This module extends cyclic fusion extraction from binary AND/OR circuits to a basis with binary meet and arbitrary finite joins. Joins, including nullary join, are free. Every least-fixed-point construction again yields exactly one fusion pair per meet equation.

def Algebraic.Fusion.Atom.meetPair? {Γ : Type u_1} (problem : SetProblem Γ) (atom : Atom JoinMeet.signature (Set Γ)) : Option (Pair problem)

Pair contributed by a meet atom; finite joins contribute no pair.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Fusion.Atom.meetPair? problem { op := Algebraic.JoinMeet.Op.join arity, arguments := arguments } = none

@[simp]

theorem Algebraic.Fusion.Atom.meetPair?_meet {Γ : Type u_1} (problem : SetProblem Γ) (arguments : Fin 2 → Set Γ) : meetPair? problem { op := JoinMeet.Op.meet, arguments := arguments } = some (Problem.restrict problem (arguments 0), Problem.restrict problem (arguments 1))

@[simp]

theorem Algebraic.Fusion.Atom.meetPair?_join {Γ : Type u_1} (problem : SetProblem Γ) (count : ℕ) (arguments : Fin count → Set Γ) : meetPair? problem { op := JoinMeet.Op.join count, arguments := arguments } = none

def Algebraic.Fusion.meetPairs {Γ : Type u_1} (problem : SetProblem Γ) (atoms : List (Atom JoinMeet.signature (Set Γ))) : List (Pair problem)

Retain the pairs from meet atoms.

Equations

• Algebraic.Fusion.meetPairs problem atoms = List.filterMap (Algebraic.Fusion.Atom.meetPair? problem) atoms

@[simp]

theorem Algebraic.Fusion.meetPairs_cons_meet {Γ : Type u_1} (problem : SetProblem Γ) (arguments : Fin 2 → Set Γ) (atoms : List (Atom JoinMeet.signature (Set Γ))) : meetPairs problem ({ op := JoinMeet.Op.meet, arguments := arguments } :: atoms) = (Problem.restrict problem (arguments 0), Problem.restrict problem (arguments 1)) :: meetPairs problem atoms

@[simp]

theorem Algebraic.Fusion.meetPairs_cons_join {Γ : Type u_1} (problem : SetProblem Γ) (count : ℕ) (arguments : Fin count → Set Γ) (atoms : List (Atom JoinMeet.signature (Set Γ))) : meetPairs problem ({ op := JoinMeet.Op.join count, arguments := arguments } :: atoms) = meetPairs problem atoms

theorem Algebraic.Fusion.meetPairs_length {Γ : Type u_1} (problem : SetProblem Γ) (atoms : List (Atom JoinMeet.signature (Set Γ))) : (meetPairs problem atoms).length = Atom.listCost atoms JoinMeet.meetCost

Retained pair count is exactly meet cost.

theorem Algebraic.Fusion.CyclicCircuit.atomAt_mono_joinMeet {n g : ℕ} {Γ : Type u_1} (circuit : CyclicCircuit JoinMeet.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 (JoinMeet.setInterpretation Γ) ⊆ (circuit.atomAt inputs upper gate).result (JoinMeet.setInterpretation Γ)

Finite-join/meet cyclic equations are monotone in their gate state.

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

Every least-fixed-point finite-join/meet construction yields a pair cover with one pair per meet equation.

Equations

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

theorem Algebraic.Fusion.pairCoverOfJoinMeetCyclic_cost {Γ : Type u_1} {g : ℕ} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (circuit : CyclicCircuit JoinMeet.signature problem.inputCount g) (constructs : circuit.Constructs (JoinMeet.setInterpretation Γ)) : (pairCoverOfJoinMeetCyclic problem admissible circuit constructs).cost = circuit.cost JoinMeet.meetCost

Extracted cover cost is exactly cyclic meet cost.

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

Pair-cover lower bounds apply to cyclic finite-join/meet circuits.

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

Least meet cost of a finite-join/meet cyclic construction. If no such construction exists, the dependent infimum is top.

Equations

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

theorem Algebraic.Fusion.joinMeetCyclicComplexity_le {Γ : Type u_1} {g : ℕ} (problem : SetProblem Γ) (circuit : CyclicCircuit JoinMeet.signature problem.inputCount g) (constructs : circuit.Constructs (JoinMeet.setInterpretation Γ)) : joinMeetCyclicComplexity problem ≤ ↑(circuit.cost JoinMeet.meetCost)

Every concrete cyclic construction upper-bounds cyclic meet complexity.

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

Pair-cover complexity is no larger than cyclic meet complexity.