Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Cyclic.Complete

Exact fusion completeness for binary cyclic circuits #

This module composes the subset-closure compiler with finite-join lowering. For finite set problems whose generators cover the ambient type, a pair cover therefore yields an ordinary binary AND/OR least-fixed-point circuit with exactly one AND per pair. Together with cover extraction, this identifies the two complexity measures exactly.

source
noncomputable def Algebraic.Fusion.binaryCircuitOfPairCover {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] (cover : PairCover problem) :
CyclicCircuit AndOr.signature problem.inputCount (JoinMeetLowering.gateCount (PairClosureCompiler.circuit problem (cover.pairs SemifilterClass.all)))

Binary cyclic circuit compiled from a pair cover.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Algebraic.Fusion.binaryConstructsOfPairCover {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] (generatorsCover : Problem.GeneratorsCover problem) (cover : PairCover problem) :
    (binaryCircuitOfPairCover problem cover).Constructs (AndOr.setInterpretation Γ)

    Proof-carrying binary cyclic construction compiled from a pair cover.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.Fusion.binaryCircuitOfPairCover_cost {Γ : Type u_1} (problem : SetProblem Γ) [Finite Γ] (cover : PairCover problem) :
      (binaryCircuitOfPairCover problem cover).cost AndOr.andCost = cover.cost

      The binary compiler charges exactly one AND for every pair occurrence.

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

      Under the explicit finiteness and generator-coverage hypotheses, binary cyclic AND complexity is no larger than pair-cover complexity.

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

      Exact modern fusion characterization using the ordinary binary AND/OR cyclic model.