Switching-lemma substrate -- definitions

Two decision-tree constructions are provided. The elementary canonical tree queries one variable at a time. The switching tree instead queries every currently free variable of the first surviving term before it either accepts or continues. This complete-block construction is the one needed by the standard switching-lemma encoding.

The explicit fuel is a proof-engineering device. The public construction starts with the number of variables in the DNF, and its correctness proof shows that each recursive query removes its variable from support.

@[reducible, inline]

abbrev Complexity.Switching.PathCode (N queryCount : ℕ) : Type

Auxiliary information carried by the elementary deepest-path encoding: the queried input coordinate and chosen branch bit at each path position.

Equations

• Complexity.Switching.PathCode N queryCount = ((Fin queryCount → Fin N) × (Fin queryCount → Bool))

@[reducible, inline]

abbrev Complexity.Switching.WidthPathCode (width queryCount : ℕ) : Type

Per-query advice for a width-sensitive switching encoding: a bounded literal position, the original path bit, and an end-of-phase marker.

Equations

• Complexity.Switching.WidthPathCode width queryCount = (Fin queryCount → Fin (width + 1) × Bool × Bool)

def Complexity.DNF.TermConsistent {N : ℕ} (term : List (Literal N)) : Prop

A term is consistent when repeated occurrences of one variable always have the same polarity. Contradictory terms must be removed or excluded before using their polarities as a satisfying assignment.

Equations

• Complexity.DNF.TermConsistent term = ∀ left ∈ term, ∀ right ∈ term, left.var = right.var → left.polarity = right.polarity

def Complexity.DNF.Consistent {N : ℕ} (formula : DNF N) : Prop

Every term in the DNF is internally consistent.

Equations

• formula.Consistent = ∀ term ∈ formula.terms, Complexity.DNF.TermConsistent term

noncomputable def Complexity.DNF.consistentPart {N : ℕ} (formula : DNF N) : DNF N

Remove contradictory DNF terms. Such terms are identically false, so this semantic cleanup does not change the represented function.

Equations

• formula.consistentPart = { terms := List.filter (fun (term : List (Complexity.Literal N)) => decide (Complexity.DNF.TermConsistent term)) formula.terms }

def Complexity.DNF.firstLiveTerm {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) : Option (List (Literal N) × List (Literal N))

The first original term that survives a restriction, paired with its reduced list of free literals. Keeping the original term supplies the provenance needed by width-sensitive switching encodings.

Equations

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

def Complexity.DNF.canonicalDecisionTreeAux {N : ℕ} : ℕ → DNF N → DecisionTree.On N

Fuelled canonical decision tree for a DNF.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DNF.canonicalDecisionTreeAux 0 x✝ = Complexity.DecisionTree.On.leaf (x✝.eval fun (x : Fin N) => false)
• Complexity.DNF.canonicalDecisionTreeAux n.succ { terms := [] } = Complexity.DecisionTree.On.leaf false
• Complexity.DNF.canonicalDecisionTreeAux n.succ { terms := [] :: tail } = Complexity.DecisionTree.On.leaf true

def Complexity.DNF.canonicalDecisionTree {N : ℕ} (formula : DNF N) : DecisionTree.On N

The canonical finite decision tree for a DNF.

Equations

• formula.canonicalDecisionTree = Complexity.DNF.canonicalDecisionTreeAux formula.vars.card formula

noncomputable def Complexity.DNF.switchingDecisionTreeAux {N : ℕ} : ℕ → DNF N → DecisionTree.On N

Fuelled block decision tree used by the switching lemma.

For the first surviving term, this tree queries every distinct variable in one complete block. A satisfying block ends at true; every other block restricts the DNF and continues with one less unit of fuel.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DNF.switchingDecisionTreeAux 0 x✝ = Complexity.DecisionTree.On.leaf (x✝.eval fun (x : Fin N) => false)
• Complexity.DNF.switchingDecisionTreeAux n.succ { terms := [] } = Complexity.DecisionTree.On.leaf false
• Complexity.DNF.switchingDecisionTreeAux n.succ { terms := [] :: tail } = Complexity.DecisionTree.On.leaf true

noncomputable def Complexity.DNF.switchingDecisionTree {N : ℕ} (formula : DNF N) : DecisionTree.On N

The canonical complete-block tree used in switching arguments.

Equations

• formula.switchingDecisionTree = Complexity.DNF.switchingDecisionTreeAux formula.vars.card formula

noncomputable def Complexity.DNF.switchingDecisionTreeUnderAux {N : ℕ} : ℕ → DNF N → Restriction.On N → DecisionTree.On N

Fuelled complete-block switching tree that retains the original DNF and accumulates a restriction separately. This is extensionally the same tree as first simplifying the DNF, but it preserves original-term provenance.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.DNF.switchingDecisionTreeUnderAux 0 x✝¹ x✝ = Complexity.DecisionTree.On.leaf (x✝¹.eval (x✝.applyTo fun (x : Fin N) => false))

noncomputable def Complexity.DNF.switchingDecisionTreeUnder {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) : DecisionTree.On N

Complete-block switching tree for an original DNF under an accumulated restriction, with enough fuel for every surviving variable.

Equations

• formula.switchingDecisionTreeUnder restriction = Complexity.DNF.switchingDecisionTreeUnderAux (Complexity.DNF.restrict restriction formula).vars.card formula restriction

noncomputable def Complexity.DNF.switchingBad {N : ℕ} (formula : DNF N) (queryCount : ℕ) (restriction : Restriction.On N) : Prop

The bad event bounded by the switching lemma: after applying the decoded random restriction, the complete-block DNF switching tree still has depth at least queryCount.

Equations

• formula.switchingBad queryCount restriction = (queryCount ≤ (formula.switchingDecisionTreeUnder restriction).depth)

@[implicit_reducible]

noncomputable instance Complexity.DNF.switchingBadDecidable {N : ℕ} (formula : DNF N) (queryCount : ℕ) : DecidablePred (formula.switchingBad queryCount)

Equations

• formula.switchingBadDecidable queryCount restriction = id inferInstance

def Complexity.CNF.Consistent {N : ℕ} (formula : CNF N) : Prop

A CNF is consistent when no clause is tautological. Equivalently, every term in its De Morgan dual DNF is internally consistent.

Equations

• formula.Consistent = formula.neg.Consistent

noncomputable def Complexity.CNF.consistentPart {N : ℕ} (formula : CNF N) : CNF N

Delete tautological CNF clauses by cleaning the contradictory terms in the De Morgan dual. This preserves the represented function.

Equations

• formula.consistentPart = formula.neg.consistentPart.neg

def Complexity.CNF.canonicalDecisionTree {N : ℕ} (formula : CNF N) : DecisionTree.On N

The canonical decision tree for a CNF, obtained by the De Morgan dual DNF and leaf complementation.

Equations

• formula.canonicalDecisionTree = formula.neg.canonicalDecisionTree.neg

noncomputable def Complexity.CNF.switchingDecisionTree {N : ℕ} (formula : CNF N) : DecisionTree.On N

The complete-block switching tree for a CNF, obtained from its De Morgan dual DNF by complementing the leaves.

Equations

• formula.switchingDecisionTree = formula.neg.switchingDecisionTree.neg

noncomputable def Complexity.CNF.switchingDecisionTreeUnder {N : ℕ} (formula : CNF N) (restriction : Restriction.On N) : DecisionTree.On N

Complete-block switching tree for a CNF under an accumulated restriction, obtained by dualizing the provenance-preserving DNF construction.

Equations

• formula.switchingDecisionTreeUnder restriction = (formula.neg.switchingDecisionTreeUnder restriction).neg

noncomputable def Complexity.CNF.switchingBad {N : ℕ} (formula : CNF N) (queryCount : ℕ) (restriction : Restriction.On N) : Prop

The CNF bad event for the switching lemma.

Equations

• formula.switchingBad queryCount restriction = (queryCount ≤ (formula.switchingDecisionTreeUnder restriction).depth)

@[implicit_reducible]

noncomputable instance Complexity.CNF.switchingBadDecidable {N : ℕ} (formula : CNF N) (queryCount : ℕ) : DecidablePred (formula.switchingBad queryCount)

Equations

• formula.switchingBadDecidable queryCount restriction = id inferInstance