Switching-lemma substrate -- proof internals

theorem Complexity.Switching.card_pathCode_internal (N queryCount : ℕ) : Fintype.card (PathCode N queryCount) = (2 * N) ^ queryCount

theorem Complexity.Switching.card_widthPathCode_internal (width queryCount : ℕ) : Fintype.card (WidthPathCode width queryCount) = (4 * (width + 1)) ^ queryCount

theorem Complexity.DNF.consistent_consistentPart_internal {N : ℕ} (formula : DNF N) : formula.consistentPart.Consistent

theorem Complexity.DNF.eval_consistentPart_internal {N : ℕ} (formula : DNF N) (input : BitString N) : formula.consistentPart.eval input = formula.eval input

theorem Complexity.DNF.width_consistentPart_le_internal {N : ℕ} (formula : DNF N) : formula.consistentPart.width ≤ formula.width

theorem Complexity.DNF.firstLiveTerm_reduced_internal {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) : Option.map Prod.snd (formula.firstLiveTerm restriction) = (restrict restriction formula).terms.head?

theorem Complexity.DNF.firstLiveTerm_spec_internal {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) (original reduced : List (Literal N)) (hfirst : formula.firstLiveTerm restriction = some (original, reduced)) : ∃ (before : List (List (Literal N))) (after : List (List (Literal N))), formula.terms = before ++ original :: after ∧ restrictTerm restriction original = some reduced ∧ ∀ term ∈ before, restrictTerm restriction term = none

theorem Complexity.DNF.firstLiveTerm_comp_internal {N : ℕ} (formula : DNF N) (first second : Restriction.On N) (original reduced final : List (Literal N)) (hfirst : formula.firstLiveTerm first = some (original, reduced)) (hsecond : restrictTerm second reduced = some final) : formula.firstLiveTerm (first.comp second) = some (original, final)

theorem Complexity.DNF.switchingDecisionTreeUnderAux_eq_internal {N : ℕ} (fuel : ℕ) (formula : DNF N) (restriction : Restriction.On N) : switchingDecisionTreeUnderAux fuel formula restriction = switchingDecisionTreeAux fuel (restrict restriction formula)

theorem Complexity.DNF.switchingDecisionTreeUnder_eq_internal {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) : formula.switchingDecisionTreeUnder restriction = (restrict restriction formula).switchingDecisionTree

theorem Complexity.DNF.vars_canonicalDecisionTreeAux_subset_internal {N : ℕ} (fuel : ℕ) (formula : DNF N) : (canonicalDecisionTreeAux fuel formula).vars ⊆ formula.vars

theorem Complexity.DNF.pathReadOnce_canonicalDecisionTreeAux_internal {N : ℕ} (fuel : ℕ) (formula : DNF N) : (canonicalDecisionTreeAux fuel formula).PathReadOnce

theorem Complexity.DNF.eval_canonicalDecisionTreeAux_internal {N : ℕ} (fuel : ℕ) (formula : DNF N) (hcard : formula.vars.card ≤ fuel) (input : BitString N) : DecisionTree.On.eval input (canonicalDecisionTreeAux fuel formula) = formula.eval input

theorem Complexity.DNF.depth_canonicalDecisionTreeAux_le_internal {N : ℕ} (fuel : ℕ) (formula : DNF N) : (canonicalDecisionTreeAux fuel formula).depth ≤ fuel

theorem Complexity.DNF.eval_canonicalDecisionTree_internal {N : ℕ} (formula : DNF N) (input : BitString N) : DecisionTree.On.eval input formula.canonicalDecisionTree = formula.eval input

theorem Complexity.DNF.depth_canonicalDecisionTree_le_vars_internal {N : ℕ} (formula : DNF N) : formula.canonicalDecisionTree.depth ≤ formula.vars.card

theorem Complexity.DNF.depth_canonicalDecisionTree_le_arity_internal {N : ℕ} (formula : DNF N) : formula.canonicalDecisionTree.depth ≤ N

theorem Complexity.DNF.vars_canonicalDecisionTree_subset_internal {N : ℕ} (formula : DNF N) : formula.canonicalDecisionTree.vars ⊆ formula.vars

theorem Complexity.DNF.pathReadOnce_canonicalDecisionTree_internal {N : ℕ} (formula : DNF N) : formula.canonicalDecisionTree.PathReadOnce

theorem Complexity.DNF.vars_switchingDecisionTreeAux_subset_internal {N : ℕ} (fuel : ℕ) (formula : DNF N) : (switchingDecisionTreeAux fuel formula).vars ⊆ formula.vars

theorem Complexity.DNF.pathReadOnce_switchingDecisionTreeAux_internal {N : ℕ} (fuel : ℕ) (formula : DNF N) : (switchingDecisionTreeAux fuel formula).PathReadOnce

theorem Complexity.DNF.eval_switchingDecisionTreeAux_internal {N : ℕ} (fuel : ℕ) (formula : DNF N) (hcard : formula.vars.card ≤ fuel) (input : BitString N) : DecisionTree.On.eval input (switchingDecisionTreeAux fuel formula) = formula.eval input

theorem Complexity.DNF.eval_switchingDecisionTree_internal {N : ℕ} (formula : DNF N) (input : BitString N) : DecisionTree.On.eval input formula.switchingDecisionTree = formula.eval input

theorem Complexity.DNF.vars_switchingDecisionTree_subset_internal {N : ℕ} (formula : DNF N) : formula.switchingDecisionTree.vars ⊆ formula.vars

theorem Complexity.DNF.pathReadOnce_switchingDecisionTree_internal {N : ℕ} (formula : DNF N) : formula.switchingDecisionTree.PathReadOnce

theorem Complexity.DNF.depth_switchingDecisionTree_le_vars_internal {N : ℕ} (formula : DNF N) : formula.switchingDecisionTree.depth ≤ formula.vars.card

theorem Complexity.DNF.depth_switchingDecisionTree_le_arity_internal {N : ℕ} (formula : DNF N) : formula.switchingDecisionTree.depth ≤ N

theorem Complexity.DNF.switchingBad_width_encoding_bound_internal {N : ℕ} (formula : DNF N) (hconsistent : formula.Consistent) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

theorem Complexity.DNF.switchingBad_consistentPart_width_encoding_bound_internal {N : ℕ} (formula : DNF N) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.consistentPart.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

theorem Complexity.DNF.switchingBad_arity_encoding_bound_internal {N : ℕ} (formula : DNF N) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (2 * N) ^ queryCount

theorem Complexity.CNF.consistent_consistentPart_internal {N : ℕ} (formula : CNF N) : formula.consistentPart.Consistent

theorem Complexity.CNF.eval_consistentPart_internal {N : ℕ} (formula : CNF N) (input : BitString N) : formula.consistentPart.eval input = formula.eval input

theorem Complexity.CNF.width_consistentPart_le_internal {N : ℕ} (formula : CNF N) : formula.consistentPart.width ≤ formula.width

theorem Complexity.CNF.switchingDecisionTreeUnder_eq_internal {N : ℕ} (formula : CNF N) (restriction : Restriction.On N) : formula.switchingDecisionTreeUnder restriction = (restrict restriction formula).switchingDecisionTree

theorem Complexity.CNF.switchingBad_eq_neg_internal {N : ℕ} (formula : CNF N) (queryCount : ℕ) (restriction : Restriction.On N) : formula.switchingBad queryCount restriction ↔ formula.neg.switchingBad queryCount restriction

theorem Complexity.CNF.switchingBad_width_encoding_bound_internal {N : ℕ} (formula : CNF N) (hconsistent : formula.Consistent) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

theorem Complexity.CNF.switchingBad_consistentPart_width_encoding_bound_internal {N : ℕ} (formula : CNF N) (q queryCount : ℕ) : RandomRestriction.eventCount q (formula.consistentPart.switchingBad queryCount) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

theorem Complexity.CNF.eval_canonicalDecisionTree_internal {N : ℕ} (formula : CNF N) (input : BitString N) : DecisionTree.On.eval input formula.canonicalDecisionTree = formula.eval input

theorem Complexity.CNF.depth_canonicalDecisionTree_le_vars_internal {N : ℕ} (formula : CNF N) : formula.canonicalDecisionTree.depth ≤ formula.vars.card

theorem Complexity.CNF.depth_canonicalDecisionTree_le_arity_internal {N : ℕ} (formula : CNF N) : formula.canonicalDecisionTree.depth ≤ N

theorem Complexity.CNF.eval_switchingDecisionTree_internal {N : ℕ} (formula : CNF N) (input : BitString N) : DecisionTree.On.eval input formula.switchingDecisionTree = formula.eval input

theorem Complexity.CNF.vars_switchingDecisionTree_subset_internal {N : ℕ} (formula : CNF N) : formula.switchingDecisionTree.vars ⊆ formula.vars

theorem Complexity.CNF.pathReadOnce_switchingDecisionTree_internal {N : ℕ} (formula : CNF N) : formula.switchingDecisionTree.PathReadOnce

theorem Complexity.CNF.depth_switchingDecisionTree_le_vars_internal {N : ℕ} (formula : CNF N) : formula.switchingDecisionTree.depth ≤ formula.vars.card

theorem Complexity.CNF.depth_switchingDecisionTree_le_arity_internal {N : ℕ} (formula : CNF N) : formula.switchingDecisionTree.depth ≤ N