Boolean interfaces to set-theoretic fusion

An AND/OR circuit over subsets can be evaluated pointwise as a Boolean circuit. This file packages that correspondence in both directions and gives canonical set problems for positive variables and for positive/negative literals.

The literal construction deliberately models negations at the inputs. It does not silently identify arbitrary internal-NOT De Morgan circuits with bottom-negation circuits; such a conversion belongs in a separate translation module together with its explicit cost bound.

@[reducible, inline]

noncomputable abbrev Algebraic.Fusion.Problem.membershipInput {Γ : Type u_1} (problem : SetProblem Γ) (point : Γ) : Fin problem.inputCount → Bool

Pointwise Boolean values of the generators in a set problem.

Equations

• Algebraic.Fusion.Problem.membershipInput problem point input = Algebraic.AndOr.membership point (problem.inputs input)

@[simp]

theorem Algebraic.Fusion.Problem.membershipInput_apply {Γ : Type u_1} (problem : SetProblem Γ) (point : Γ) (input : Fin problem.inputCount) : membershipInput problem point input = AndOr.membership point (problem.inputs input)

def Algebraic.Fusion.Problem.ComputesMembership {Γ : Type u_1} (problem : SetProblem Γ) (circuit : Circuit AndOr.signature problem.inputCount 1) : Prop

A Boolean circuit computes the pointwise membership function of a set problem.

Equations

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

theorem Algebraic.Fusion.Problem.computesMembership_iff_constructs {Γ : Type u_1} (problem : SetProblem Γ) (circuit : Circuit AndOr.signature problem.inputCount 1) : ComputesMembership problem circuit ↔ Constructs problem circuit (AndOr.setInterpretation Γ)

Pointwise Boolean computation is equivalent to constructing the target set from the generator sets.

theorem Algebraic.Fusion.pairCover_lowerBound_of_computesMembership {Γ : Type u_1} {L : ℕ} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (coverLowerBound : ∀ (cover : PairCover problem admissible), L ≤ cover.cost) (circuit : Circuit AndOr.signature problem.inputCount 1) (computes : Problem.ComputesMembership problem circuit) : L ≤ circuit.cost AndOr.andCost

A pair-cover lower bound applies directly to a circuit computing the pointwise membership function.

theorem Algebraic.Fusion.pairCoverComplexity_le_cost_of_computesMembership {Γ : Type u_1} (problem : SetProblem Γ) (admissible : SemifilterClass problem) (circuit : Circuit AndOr.signature problem.inputCount 1) (computes : Problem.ComputesMembership problem circuit) : pairCoverComplexity problem admissible ≤ ↑(circuit.cost AndOr.andCost)

Pair-cover complexity lower-bounds pointwise Boolean computation.

@[reducible, inline]

abbrev Algebraic.Fusion.monotoneProblem {n : ℕ} (function : (Fin n → Bool) → Bool) : SetProblem (Fin n → Bool)

The set problem generated by the positive input variables of a Boolean function.

Equations

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

@[simp]

theorem Algebraic.Fusion.monotoneProblem_membershipInput {n : ℕ} (function : (Fin n → Bool) → Bool) (assignment : Fin n → Bool) : Problem.membershipInput (monotoneProblem function) assignment = assignment

theorem Algebraic.Fusion.monotoneProblem_target_membership {n : ℕ} (function : (Fin n → Bool) → Bool) (assignment : Fin n → Bool) : AndOr.membership assignment (monotoneProblem function).target = function assignment

theorem Algebraic.Fusion.monotoneProblem_computesMembership_iff {n : ℕ} (function : (Fin n → Bool) → Bool) (circuit : Circuit AndOr.signature n 1) : Problem.ComputesMembership (monotoneProblem function) circuit ↔ ∀ (assignment : Fin n → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function assignment

Constructing the positive-generator set problem is exactly computing the Boolean function with an AND/OR circuit.

theorem Algebraic.Fusion.monotone_pairCover_lowerBound {n L : ℕ} (function : (Fin n → Bool) → Bool) (admissible : SemifilterClass (monotoneProblem function)) (coverLowerBound : ∀ (cover : PairCover (monotoneProblem function) admissible), L ≤ cover.cost) (circuit : Circuit AndOr.signature n 1) (computes : ∀ (assignment : Fin n → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function assignment) : L ≤ circuit.cost AndOr.andCost

A semi-filter cover bound for the positive-generator problem transfers directly to a monotone AND/OR circuit lower bound.

theorem Algebraic.Fusion.monotone_pairCoverComplexity_le_cost {n : ℕ} (function : (Fin n → Bool) → Bool) (admissible : SemifilterClass (monotoneProblem function)) (circuit : Circuit AndOr.signature n 1) (computes : ∀ (assignment : Fin n → Bool), circuit.eval AndOr.boolInterpretation assignment 0 = function assignment) : pairCoverComplexity (monotoneProblem function) admissible ≤ ↑(circuit.cost AndOr.andCost)

Positive-generator pair-cover complexity lower-bounds monotone AND/OR computation.

def Algebraic.Fusion.literalInput {n : ℕ} (assignment : Fin n → Bool) : Fin (n + n) → Bool

Literal values associated with an assignment: positive variables first, then their negations.

Equations

• Algebraic.Fusion.literalInput assignment i = Fin.addCases assignment (fun (input : Fin n) => !assignment input) i

@[reducible, inline]

abbrev Algebraic.Fusion.literalProblem {n : ℕ} (function : (Fin n → Bool) → Bool) : SetProblem (Fin n → Bool)

The set problem generated by both positive and negative literals of a Boolean function.

Equations

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

theorem Algebraic.Fusion.literalProblem_inputs_castAdd {n : ℕ} (function : (Fin n → Bool) → Bool) (input : Fin n) : (literalProblem function).inputs (Fin.castAdd n input) = {assignment : Fin n → Bool | assignment input = true}

theorem Algebraic.Fusion.literalProblem_inputs_natAdd {n : ℕ} (function : (Fin n → Bool) → Bool) (input : Fin n) : (literalProblem function).inputs (Fin.natAdd n input) = {assignment : Fin n → Bool | assignment input = false}

theorem Algebraic.Fusion.literalInput_natAdd {n : ℕ} (assignment : Fin n → Bool) (input : Fin n) : literalInput assignment (Fin.natAdd n input) = !assignment input

@[simp]

theorem Algebraic.Fusion.literalInput_castAdd {n : ℕ} (assignment : Fin n → Bool) (input : Fin n) : literalInput assignment (Fin.castAdd n input) = assignment input

@[simp]

theorem Algebraic.Fusion.literalProblem_membershipInput {n : ℕ} (function : (Fin n → Bool) → Bool) (assignment : Fin n → Bool) : Problem.membershipInput (literalProblem function) assignment = literalInput assignment

theorem Algebraic.Fusion.literalProblem_target_membership {n : ℕ} (function : (Fin n → Bool) → Bool) (assignment : Fin n → Bool) : AndOr.membership assignment (literalProblem function).target = function assignment

theorem Algebraic.Fusion.literalProblem_computesMembership_iff {n : ℕ} (function : (Fin n → Bool) → Bool) (circuit : Circuit AndOr.signature (n + n) 1) : Problem.ComputesMembership (literalProblem function) circuit ↔ ∀ (assignment : Fin n → Bool), circuit.eval AndOr.boolInterpretation (literalInput assignment) 0 = function assignment

Constructing the literal-generator set problem is exactly computing the function from its positive and negative literal values.

theorem Algebraic.Fusion.literal_pairCover_lowerBound {n L : ℕ} (function : (Fin n → Bool) → Bool) (admissible : SemifilterClass (literalProblem function)) (coverLowerBound : ∀ (cover : PairCover (literalProblem function) admissible), L ≤ cover.cost) (circuit : Circuit AndOr.signature (n + n) 1) (computes : ∀ (assignment : Fin n → Bool), circuit.eval AndOr.boolInterpretation (literalInput assignment) 0 = function assignment) : L ≤ circuit.cost AndOr.andCost

A semi-filter cover bound for the literal-generator problem transfers directly to an AND/OR-over-literals circuit lower bound.

theorem Algebraic.Fusion.literal_pairCoverComplexity_le_cost {n : ℕ} (function : (Fin n → Bool) → Bool) (admissible : SemifilterClass (literalProblem function)) (circuit : Circuit AndOr.signature (n + n) 1) (computes : ∀ (assignment : Fin n → Bool), circuit.eval AndOr.boolInterpretation (literalInput assignment) 0 = function assignment) : pairCoverComplexity (literalProblem function) admissible ≤ ↑(circuit.cost AndOr.andCost)

Literal-generator pair-cover complexity lower-bounds AND/OR computation over positive and negative input literals.