Fusion for universally quantified Boolean circuits

A conondeterministic circuit for f accepts a primary assignment exactly when it accepts that assignment for every auxiliary assignment. On a false primary assignment, classical choice selects one rejecting auxiliary assignment. A semi-ultrafilter above a true assignment then fuses those selected auxiliary assignments coordinate by coordinate.

This produces a SemifilterPullback from the verifier's literal problem to the literal problem for f. Consequently every lower bound for semi-ultrafilter pair covers of f applies, with no loss, to the verifier's number of AND gates.

def Algebraic.Fusion.Conondeterministic.combine {n a : ℕ} (primary : Fin n → Bool) (auxiliary : Fin a → Bool) : Fin (n + a) → Bool

Concatenate a primary and an auxiliary Boolean assignment.

Equations

• Algebraic.Fusion.Conondeterministic.combine primary auxiliary i = Fin.addCases primary auxiliary i

@[simp]

theorem Algebraic.Fusion.Conondeterministic.combine_castAdd {n a : ℕ} (primary : Fin n → Bool) (auxiliary : Fin a → Bool) (input : Fin n) : combine primary auxiliary (Fin.castAdd a input) = primary input

@[simp]

theorem Algebraic.Fusion.Conondeterministic.combine_natAdd {n a : ℕ} (primary : Fin n → Bool) (auxiliary : Fin a → Bool) (input : Fin a) : combine primary auxiliary (Fin.natAdd n input) = auxiliary input

def Algebraic.Fusion.Conondeterministic.verifierFunction {n a : ℕ} (circuit : Circuit AndOr.signature (n + a + (n + a)) 1) (assignment : Fin (n + a) → Bool) : Bool

The Boolean function computed by a verifier circuit on a combined assignment, with negations available only as input literals.

Equations

• Algebraic.Fusion.Conondeterministic.verifierFunction circuit assignment = circuit.eval Algebraic.AndOr.boolInterpretation (Algebraic.Fusion.literalInput assignment) 0

def Algebraic.Fusion.Conondeterministic.UniversallyComputes {n a : ℕ} (circuit : Circuit AndOr.signature (n + a + (n + a)) 1) (function : (Fin n → Bool) → Bool) : Prop

A verifier universally computes function when a primary input is true exactly if every auxiliary completion is accepted.

Equations

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

theorem Algebraic.Fusion.Conondeterministic.exists_rejectingAuxiliary {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (counterexample : Problem.Outside (literalProblem function)) : ∃ (auxiliary : Fin a → Bool), verifierFunction circuit (combine (↑counterexample) auxiliary) = false

Every false primary assignment has a rejecting auxiliary completion.

noncomputable def Algebraic.Fusion.Conondeterministic.rejectingAuxiliary {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (counterexample : Problem.Outside (literalProblem function)) : Fin a → Bool

A selected rejecting auxiliary completion for each false primary input.

Equations

• Algebraic.Fusion.Conondeterministic.rejectingAuxiliary computes counterexample = Classical.choose ⋯

@[simp]

theorem Algebraic.Fusion.Conondeterministic.verifierFunction_rejectingAuxiliary {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (counterexample : Problem.Outside (literalProblem function)) : verifierFunction circuit (combine (↑counterexample) (rejectingAuxiliary computes counterexample)) = false

noncomputable def Algebraic.Fusion.Conondeterministic.counterexampleMap {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) : Problem.Outside (literalProblem function) → Fin (n + a) → Bool

Map a false primary assignment to its selected rejecting verifier input.

Equations

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

@[simp]

theorem Algebraic.Fusion.Conondeterministic.counterexampleMap_castAdd {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (counterexample : Problem.Outside (literalProblem function)) (input : Fin n) : counterexampleMap computes counterexample (Fin.castAdd a input) = ↑counterexample input

@[simp]

theorem Algebraic.Fusion.Conondeterministic.counterexampleMap_natAdd {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (counterexample : Problem.Outside (literalProblem function)) (input : Fin a) : counterexampleMap computes counterexample (Fin.natAdd n input) = rejectingAuxiliary computes counterexample input

def Algebraic.Fusion.Conondeterministic.positiveAuxiliarySet {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (input : Fin a) : Set (Problem.Outside (literalProblem function))

False primary inputs whose selected rejection sets one auxiliary coordinate to true.

Equations

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

theorem Algebraic.Fusion.Conondeterministic.positiveAuxiliarySet_compl {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (input : Fin a) : (positiveAuxiliarySet computes input)ᶜ = {counterexample : Problem.Outside (literalProblem function) | rejectingAuxiliary computes counterexample input = false}

noncomputable def Algebraic.Fusion.Conondeterministic.fusedAuxiliary {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (witness : SemifilterWitness (literalProblem function) SemifilterClass.ultra) : Fin a → Bool

Auxiliary reference values obtained by asking the semi-ultrafilter which side of each selected auxiliary coordinate it accepts.

Equations

• Algebraic.Fusion.Conondeterministic.fusedAuxiliary computes witness input = if Algebraic.Fusion.Conondeterministic.positiveAuxiliarySet computes input ∈ witness.filter then true else false

noncomputable def Algebraic.Fusion.Conondeterministic.referencePoint {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (witness : SemifilterWitness (literalProblem function) SemifilterClass.ultra) : Fin (n + a) → Bool

The verifier reference point: the true primary point together with the coordinatewise semi-ultrafilter fusion of selected rejecting assignments.

Equations

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

@[simp]

theorem Algebraic.Fusion.Conondeterministic.referencePoint_castAdd {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (witness : SemifilterWitness (literalProblem function) SemifilterClass.ultra) (input : Fin n) : referencePoint computes witness (Fin.castAdd a input) = witness.point input

@[simp]

theorem Algebraic.Fusion.Conondeterministic.referencePoint_natAdd {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (witness : SemifilterWitness (literalProblem function) SemifilterClass.ultra) (input : Fin a) : referencePoint computes witness (Fin.natAdd n input) = fusedAuxiliary computes witness input

theorem Algebraic.Fusion.Conondeterministic.positiveAuxiliarySet_mem_of_fused_eq_true {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (witness : SemifilterWitness (literalProblem function) SemifilterClass.ultra) (input : Fin a) (equal : fusedAuxiliary computes witness input = true) : positiveAuxiliarySet computes input ∈ witness.filter

theorem Algebraic.Fusion.Conondeterministic.compl_positiveAuxiliarySet_mem_of_fused_eq_false {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (witness : SemifilterWitness (literalProblem function) SemifilterClass.ultra) (input : Fin a) (equal : fusedAuxiliary computes witness input = false) : (positiveAuxiliarySet computes input)ᶜ ∈ witness.filter

theorem Algebraic.Fusion.Conondeterministic.referencePoint_mem_target {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (witness : SemifilterWitness (literalProblem function) SemifilterClass.ultra) : referencePoint computes witness ∈ (literalProblem (verifierFunction circuit)).target

Every fused reference assignment is accepted by the verifier.

theorem Algebraic.Fusion.Conondeterministic.counterexampleMap_not_mem_target {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (counterexample : Problem.Outside (literalProblem function)) : counterexampleMap computes counterexample ∉ (literalProblem (verifierFunction circuit)).target

Selected counterexample assignments lie outside the verifier target.

theorem Algebraic.Fusion.Conondeterministic.input_sound {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) (witness : SemifilterWitness (literalProblem function) SemifilterClass.ultra) (literal : Fin (n + a + (n + a))) : referencePoint computes witness ∈ (literalProblem (verifierFunction circuit)).inputs literal → counterexampleMap computes ⁻¹' (literalProblem (verifierFunction circuit)).inputs literal ∈ witness.filter

Soundness of every verifier literal under the counterexample pullback.

noncomputable def Algebraic.Fusion.Conondeterministic.pullback {n a : ℕ} {function : (Fin n → Bool) → Bool} {circuit : Circuit AndOr.signature (n + a + (n + a)) 1} (computes : UniversallyComputes circuit function) : SemifilterPullback (literalProblem function) (literalProblem (verifierFunction circuit)) SemifilterClass.ultra

The canonical semi-ultrafilter pullback associated with a universally computing verifier.

Equations

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

theorem Algebraic.Fusion.Conondeterministic.constructs_verifierProblem {n a : ℕ} (circuit : Circuit AndOr.signature (n + a + (n + a)) 1) : Problem.Constructs (literalProblem (verifierFunction circuit)) circuit (AndOr.setInterpretation (Fin (n + a) → Bool))

A verifier circuit constructs its own literal set problem.

theorem Algebraic.Fusion.Conondeterministic.and_lowerBound {n L a : ℕ} {function : (Fin n → Bool) → Bool} (coverLowerBound : ∀ (cover : PairCover (literalProblem function) SemifilterClass.ultra), L ≤ cover.cost) (circuit : Circuit AndOr.signature (n + a + (n + a)) 1) (computes : UniversallyComputes circuit function) : L ≤ circuit.cost AndOr.andCost

Every lower bound for semi-ultrafilter covers of function transfers without loss to a universally computing verifier circuit.