Compiling fusion covers to cyclic circuits

For a finite set problem, this module turns the generated pair closure into a finite cyclic system. There is one gate for every subset of the target complement, one meet gate for every listed fusion pair, and one bottom gate. All generator and upward-closure rules are collected by free finite joins.

The sole semantic side condition is that the input generators cover the ambient type. It supplies the universal-set seed without assuming a free top constant. The resulting circuit has exactly one charged meet for every pair.

def Algebraic.Fusion.Problem.GeneratorsCover {Γ : Type u_1} (problem : SetProblem Γ) : Prop

Every ambient point occurs in at least one input generator.

Equations

• Algebraic.Fusion.Problem.GeneratorsCover problem = ∀ (point : Γ), ∃ (input : Fin problem.inputCount), point ∈ problem.inputs input

@[instance_reducible]

noncomputable def Algebraic.Fusion.PairClosureCompiler.subsetFintype {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] : Fintype (Set (Problem.Outside problem))

A fixed finite presentation of the subset-indexed closure gates.

Equations

• Algebraic.Fusion.PairClosureCompiler.subsetFintype problem = Fintype.ofFinite (Set (Algebraic.Fusion.Problem.Outside problem))

noncomputable def Algebraic.Fusion.PairClosureCompiler.subsetCount {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] : ℕ

Number of subset-indexed closure gates.

Equations

• Algebraic.Fusion.PairClosureCompiler.subsetCount problem = Fintype.card (Set (Algebraic.Fusion.Problem.Outside problem))

noncomputable def Algebraic.Fusion.PairClosureCompiler.subsetEquiv {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] : Set (Problem.Outside problem) ≃ Fin (subsetCount problem)

Canonical chosen numbering of subset-indexed closure gates.

Equations

• Algebraic.Fusion.PairClosureCompiler.subsetEquiv problem = Fintype.equivFin (Set (Algebraic.Fusion.Problem.Outside problem))

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.PairClosureCompiler.gateCount {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : ℕ

Total gate count: closure gates, pair gates, and one bottom gate.

Equations

• Algebraic.Fusion.PairClosureCompiler.gateCount problem pairs = Algebraic.Fusion.PairClosureCompiler.subsetCount problem + (pairs.length + 1)

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.PairClosureCompiler.sourceCount {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : ℕ

Total join arity used at every closure gate. Invalid candidate sources are redirected to the bottom gate.

Equations

• Algebraic.Fusion.PairClosureCompiler.sourceCount problem pairs = problem.inputCount + (Algebraic.Fusion.PairClosureCompiler.subsetCount problem + pairs.length)

noncomputable def Algebraic.Fusion.PairClosureCompiler.inputSlot {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (input : Fin problem.inputCount) : Fin (sourceCount problem pairs)

Slot occupied by an input among the candidate closure sources.

Equations

• Algebraic.Fusion.PairClosureCompiler.inputSlot problem pairs input = Fin.castAdd (Algebraic.Fusion.PairClosureCompiler.subsetCount problem + pairs.length) input

noncomputable def Algebraic.Fusion.PairClosureCompiler.closureSlot {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) : Fin (sourceCount problem pairs)

Slot occupied by a lower closure gate among the candidate sources.

Equations

• Algebraic.Fusion.PairClosureCompiler.closureSlot problem pairs set = Fin.natAdd problem.inputCount (Fin.castAdd pairs.length ((Algebraic.Fusion.PairClosureCompiler.subsetEquiv problem) set))

noncomputable def Algebraic.Fusion.PairClosureCompiler.pairSlot {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : Fin (sourceCount problem pairs)

Slot occupied by a pair gate among the candidate closure sources.

Equations

• Algebraic.Fusion.PairClosureCompiler.pairSlot problem pairs index = Fin.natAdd problem.inputCount (Fin.natAdd (Algebraic.Fusion.PairClosureCompiler.subsetCount problem) index)

noncomputable def Algebraic.Fusion.PairClosureCompiler.closureGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) : Fin (gateCount problem pairs)

Gate carrying the generated state at a specified subset.

Equations

• Algebraic.Fusion.PairClosureCompiler.closureGate problem pairs set = Fin.castAdd (pairs.length + 1) ((Algebraic.Fusion.PairClosureCompiler.subsetEquiv problem) set)

noncomputable def Algebraic.Fusion.PairClosureCompiler.pairGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : Fin (gateCount problem pairs)

Meet gate associated with one occurrence in the pair list.

Equations

• Algebraic.Fusion.PairClosureCompiler.pairGate problem pairs index = Fin.natAdd (Algebraic.Fusion.PairClosureCompiler.subsetCount problem) index.castSucc

noncomputable def Algebraic.Fusion.PairClosureCompiler.bottomGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : Fin (gateCount problem pairs)

Dedicated nullary-join gate carrying the empty set.

Equations

• Algebraic.Fusion.PairClosureCompiler.bottomGate problem pairs = Fin.natAdd (Algebraic.Fusion.PairClosureCompiler.subsetCount problem) (Fin.last pairs.length)

noncomputable def Algebraic.Fusion.PairClosureCompiler.gateWire {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (gate : Fin (gateCount problem pairs)) : Wire problem.inputCount (gateCount problem pairs)

Turn a gate index into a wire.

Equations

• Algebraic.Fusion.PairClosureCompiler.gateWire problem pairs gate = Cslib.Circuits.Wire.gate gate

noncomputable def Algebraic.Fusion.PairClosureCompiler.inputSource {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) (input : Fin problem.inputCount) : Wire problem.inputCount (gateCount problem pairs)

A candidate input source is active at set exactly when its restriction is contained in set.

Equations

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

noncomputable def Algebraic.Fusion.PairClosureCompiler.closureSource {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) (lowerIndex : Fin (subsetCount problem)) : Wire problem.inputCount (gateCount problem pairs)

A candidate closure source is active exactly along an upward-closure edge.

Equations

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

noncomputable def Algebraic.Fusion.PairClosureCompiler.pairSource {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) (index : Fin pairs.length) : Wire problem.inputCount (gateCount problem pairs)

A candidate pair source is active at the gate indexed by the pair's intersection.

Equations

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

noncomputable def Algebraic.Fusion.PairClosureCompiler.sourceWire {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) (source : Fin (sourceCount problem pairs)) : Wire problem.inputCount (gateCount problem pairs)

All possible sources of one subset-indexed closure equation.

Equations

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

noncomputable def Algebraic.Fusion.PairClosureCompiler.closureLine {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) : Line JoinMeet.signature problem.inputCount (gateCount problem pairs)

Free join equation collecting every rule that can derive set.

Equations

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

noncomputable def Algebraic.Fusion.PairClosureCompiler.pairLine {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : Line JoinMeet.signature problem.inputCount (gateCount problem pairs)

Charged meet equation implementing one fusion rule.

Equations

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

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.pairLine_wire_zero {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : (pairLine problem pairs index).wires 0 = gateWire problem pairs (closureGate problem pairs (pairs.get index).1)

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.pairLine_wire_one {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : (pairLine problem pairs index).wires 1 = gateWire problem pairs (closureGate problem pairs (pairs.get index).2)

noncomputable def Algebraic.Fusion.PairClosureCompiler.bottomLine {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : Line JoinMeet.signature problem.inputCount (gateCount problem pairs)

Nullary join equation supplying bottom to inactive source slots.

Equations

• Algebraic.Fusion.PairClosureCompiler.bottomLine problem pairs = { op := Algebraic.JoinMeet.Op.join 0, wires := Fin.elim0 }

noncomputable def Algebraic.Fusion.PairClosureCompiler.circuit {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : CyclicCircuit JoinMeet.signature problem.inputCount (gateCount problem pairs)

The cyclic finite-join/meet circuit compiled from a pair list.

Equations

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

noncomputable def Algebraic.Fusion.PairClosureCompiler.values {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : Fin (gateCount problem pairs) → Set Γ

Intended semantic values of the compiled equations.

Equations

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

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.values_closureGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) : values problem pairs (closureGate problem pairs set) = PairClosure.generatedState problem pairs set

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.values_pairGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : values problem pairs (pairGate problem pairs index) = PairClosure.generatedState problem pairs (pairs.get index).1 ∩ PairClosure.generatedState problem pairs (pairs.get index).2

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.values_bottomGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : values problem pairs (bottomGate problem pairs) = ∅

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.circuit_line_closureGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (set : Set (Problem.Outside problem)) : (circuit problem pairs).lines (closureGate problem pairs set) = closureLine problem pairs set

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.circuit_line_pairGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : (circuit problem pairs).lines (pairGate problem pairs index) = pairLine problem pairs index

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.circuit_line_bottomGate {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : (circuit problem pairs).lines (bottomGate problem pairs) = bottomLine problem pairs

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.circuit_output {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : (circuit problem pairs).output = closureGate problem pairs ∅

theorem Algebraic.Fusion.PairClosureCompiler.closure_result_eq_generatedState {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) (set : Set (Problem.Outside problem)) : ((circuit problem pairs).atomAt problem.inputs (values problem pairs) (closureGate problem pairs set)).result (JoinMeet.setInterpretation Γ) = PairClosure.generatedState problem pairs set

Each compiled closure equation evaluates to the corresponding generated state.

theorem Algebraic.Fusion.PairClosureCompiler.pair_result_eq_values {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : ((circuit problem pairs).atomAt problem.inputs (values problem pairs) (pairGate problem pairs index)).result (JoinMeet.setInterpretation Γ) = values problem pairs (pairGate problem pairs index)

Each compiled pair equation evaluates to the intersection represented by its charged meet gate.

theorem Algebraic.Fusion.PairClosureCompiler.bottom_result_eq_values {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : ((circuit problem pairs).atomAt problem.inputs (values problem pairs) (bottomGate problem pairs)).result (JoinMeet.setInterpretation Γ) = values problem pairs (bottomGate problem pairs)

The dedicated nullary join equation evaluates to bottom.

theorem Algebraic.Fusion.PairClosureCompiler.values_fixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) (gate : Fin (gateCount problem pairs)) : values problem pairs gate = ((circuit problem pairs).atomAt problem.inputs (values problem pairs) gate).result (JoinMeet.setInterpretation Γ)

The generated closure state satisfies every compiled cyclic equation.

theorem Algebraic.Fusion.PairClosureCompiler.source_subset_of_prefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (candidate : Fin (gateCount problem pairs) → Set Γ) (prefixed : (circuit problem pairs).IsPrefixed (JoinMeet.setInterpretation Γ) problem.inputs candidate) (set : Set (Problem.Outside problem)) (source : Fin (sourceCount problem pairs)) : Wire.elim problem.inputs candidate (sourceWire problem pairs set source) ⊆ candidate (closureGate problem pairs set)

Every candidate source lies below its closure gate in any pre-fixed state of the compiled circuit.

theorem Algebraic.Fusion.PairClosureCompiler.input_subset_of_prefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (candidate : Fin (gateCount problem pairs) → Set Γ) (prefixed : (circuit problem pairs).IsPrefixed (JoinMeet.setInterpretation Γ) problem.inputs candidate) (input : Fin problem.inputCount) (set : Set (Problem.Outside problem)) (active : Problem.restrict problem (problem.inputs input) ⊆ set) : problem.inputs input ⊆ candidate (closureGate problem pairs set)

An active generator edge lies below its closure gate in every pre-fixed state.

theorem Algebraic.Fusion.PairClosureCompiler.closure_subset_of_prefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (candidate : Fin (gateCount problem pairs) → Set Γ) (prefixed : (circuit problem pairs).IsPrefixed (JoinMeet.setInterpretation Γ) problem.inputs candidate) {lower upper : Set (Problem.Outside problem)} (active : lower ⊆ upper) : candidate (closureGate problem pairs lower) ⊆ candidate (closureGate problem pairs upper)

An active upward edge lies below its closure gate in every pre-fixed state.

theorem Algebraic.Fusion.PairClosureCompiler.pair_subset_closure_of_prefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (candidate : Fin (gateCount problem pairs) → Set Γ) (prefixed : (circuit problem pairs).IsPrefixed (JoinMeet.setInterpretation Γ) problem.inputs candidate) (index : Fin pairs.length) : candidate (pairGate problem pairs index) ⊆ candidate (closureGate problem pairs ((pairs.get index).1 ∩ (pairs.get index).2))

The active source of a pair intersection lies below the corresponding closure gate in every pre-fixed state.

theorem Algebraic.Fusion.PairClosureCompiler.inter_subset_pair_of_prefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (candidate : Fin (gateCount problem pairs) → Set Γ) (prefixed : (circuit problem pairs).IsPrefixed (JoinMeet.setInterpretation Γ) problem.inputs candidate) (index : Fin pairs.length) : candidate (closureGate problem pairs (pairs.get index).1) ∩ candidate (closureGate problem pairs (pairs.get index).2) ⊆ candidate (pairGate problem pairs index)

A pair equation forces the meet of its two closure values into its pair gate in every pre-fixed state.

theorem Algebraic.Fusion.PairClosureCompiler.pairClosure_prefixed_of_circuit_prefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) (candidate : Fin (gateCount problem pairs) → Set Γ) (prefixed : (circuit problem pairs).IsPrefixed (JoinMeet.setInterpretation Γ) problem.inputs candidate) : PairClosure.IsPrefixed problem pairs fun (set : Set (Problem.Outside problem)) => candidate (closureGate problem pairs set)

Restricting any pre-fixed circuit state to its closure gates gives a state closed under all abstract pair-closure rules.

theorem Algebraic.Fusion.PairClosureCompiler.generatedState_subset_of_prefixed {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) (candidate : Fin (gateCount problem pairs) → Set Γ) (prefixed : (circuit problem pairs).IsPrefixed (JoinMeet.setInterpretation Γ) problem.inputs candidate) (set : Set (Problem.Outside problem)) : PairClosure.generatedState problem pairs set ⊆ candidate (closureGate problem pairs set)

The intended closure value lies below the corresponding gate of every pre-fixed circuit state.

theorem Algebraic.Fusion.PairClosureCompiler.values_least {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) (candidate : Fin (gateCount problem pairs) → Set Γ) (prefixed : (circuit problem pairs).IsPrefixed (JoinMeet.setInterpretation Γ) problem.inputs candidate) (gate : Fin (gateCount problem pairs)) : values problem pairs gate ⊆ candidate gate

The intended values form the least pre-fixed state of the compiled cyclic system.

noncomputable def Algebraic.Fusion.PairClosureCompiler.constructsOfPairCover {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) (cover : PairCover problem) : (circuit problem (cover.pairs SemifilterClass.all)).Constructs (JoinMeet.setInterpretation Γ)

A pair cover compiles to a proof-carrying least-fixed-point construction of the target.

Equations

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

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.lineCost_closureIndex {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin (subsetCount problem)) : JoinMeet.meetCost ((circuit problem pairs).lines (Fin.castAdd (pairs.length + 1) index)).op = 0

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.lineCost_closureIndex_castLE {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin (subsetCount problem)) (bound : subsetCount problem ≤ gateCount problem pairs) : JoinMeet.meetCost ((circuit problem pairs).lines (Fin.castLE bound index)).op = 0

theorem Algebraic.Fusion.PairClosureCompiler.lineCost_pairIndex {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : JoinMeet.meetCost ((circuit problem pairs).lines (pairGate problem pairs index)).op = 1

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.lineCost_pairIndex_natAdd {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] (index : Fin pairs.length) : JoinMeet.meetCost ((circuit problem pairs).lines (Fin.natAdd (subsetCount problem) index.castSucc)).op = 1

theorem Algebraic.Fusion.PairClosureCompiler.lineCost_bottomIndex {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : JoinMeet.meetCost ((circuit problem pairs).lines (bottomGate problem pairs)).op = 0

theorem Algebraic.Fusion.PairClosureCompiler.lineCost_bottomIndex_natAdd {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : JoinMeet.meetCost ((circuit problem pairs).lines (Fin.natAdd (subsetCount problem) (Fin.last pairs.length))).op = 0

@[simp]

theorem Algebraic.Fusion.PairClosureCompiler.lineCost_lastIndex {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : JoinMeet.meetCost ((circuit problem pairs).lines (Fin.last (subsetCount problem + pairs.length))).op = 0

theorem Algebraic.Fusion.PairClosureCompiler.circuit_cost {Γ : Type u_1} (problem : SetProblem Γ) (pairs : List (Pair problem)) [Finite Γ] : (circuit problem pairs).cost JoinMeet.meetCost = pairs.length

The compiled circuit charges exactly one meet for each pair occurrence.

theorem Algebraic.Fusion.joinMeetCyclicComplexity_le_pairCoverComplexity {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) : joinMeetCyclicComplexity problem ≤ pairCoverComplexity problem

Under finite ambient support and covered generators, cyclic meet complexity is no larger than pair-cover complexity.

theorem Algebraic.Fusion.pairCoverComplexity_eq_joinMeetCyclicComplexity {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) : pairCoverComplexity problem = joinMeetCyclicComplexity problem

Modern fusion completeness for finite covered set problems: pair-cover complexity is exactly least-fixed-point cyclic meet complexity.