From 6982088c66d3a84774832fcfd34d256677aaedfd Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Thu, 29 Oct 2026 14:50:10 -0400 Subject: [PATCH] refactor(List): reuse core maximum bounds in sparse counters Remove the four duplicate Nat maximum-fold helpers from SparsePolyCounter and migrate all clients, including the private test copy, to the core nonempty-list maximum API. Retained declarations, algorithm definitions, resource bounds and source credit are unchanged. AI assistance: Codex worker codex-worker-list-foldl-max-1647 implemented and self-reviewed this refactor under coordinator codex-coord-20261029-1732. Validation: all six scripts/check.sh gates, source hygiene, changed-file lints, tidy surface and diff checks passed on the committed source tree. --- .../BoundedIncidenceCounter.lean | 10 ++- .../BoundedIncidenceExactness.lean | 3 +- .../BoundedIncidenceSemantics.lean | 5 +- .../BoundedIncidenceStepCert.lean | 8 +- .../BooleanAnalysis/SparsePolyCounter.lean | 77 ++++++++++--------- .../CNF/BranchedSparseCNFCounter.lean | 4 +- .../BoundedIncidenceExactness.lean | 28 +++---- 7 files changed, 77 insertions(+), 58 deletions(-) diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean index 82a2b1db0..ad972a107 100644 --- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean +++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceCounter.lean @@ -1341,9 +1341,15 @@ public theorem exists_boundedIncidenceBranchCertificate_time_bound simp only [Rat.cast_natCast, Rat.cast_mul, Rat.cast_ofNat, ReplacementParams.cast_tauRat] at hrat_r exact (Nat.cast_le.mpr hc_le).trans hrat_r - · unfold d_max maxAllGroupDim; refine foldl_max_le (Nat.zero_le _) fun x hx => ?_ + · unfold d_max maxAllGroupDim + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨Nat.zero_le _, fun x hx => ?_⟩ obtain ⟨t, ht_mem, rfl⟩ := List.mem_map.mp hx; have ht : t < Q := List.mem_range.mp ht_mem - unfold maxGroupDim; refine foldl_max_le (Nat.zero_le _) fun y hy => ?_ + unfold maxGroupDim + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨Nat.zero_le _, fun y hy => ?_⟩ obtain ⟨g, hg_mem, rfl⟩ := List.mem_map.mp hy; have hg : g < r := List.mem_range.mp hg_mem refine (Nat.min_le_right _ _).trans ?_; have hgrp := (href.2.2.1 ⟨t, ht⟩ ⟨g, hg⟩).2.1 dsimp only [data, mkDesignPair, mkDesignFromScheds, prepScheduleParams, diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean index 2a6675a80..5866d1a2e 100644 --- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean +++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean @@ -1090,7 +1090,8 @@ theorem evalBoundedIncidenceBranch_eq_rootCount {N₀_branch n' : ℕ} let P_eq : Fin eqs'.length → Finset (Finset (Fin n')) := fun f => HeavyBranchFold.toFinsetEquation n' eqs'[f] have hk_list : ∀ eq ∈ eqs', ∀ m ∈ eq, m.length ≤ k' := fun eq heq m hm => - le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_flatten.mpr ⟨eq, heq, hm⟩)) + List.le_max_of_mem + (List.mem_cons_of_mem _ (List.mem_map_of_mem (List.mem_flatten.mpr ⟨eq, heq, hm⟩))) have hk_fin : ∀ f ∈ (univ : Finset (Fin eqs'.length)), ∀ M ∈ P_eq f, #M ≤ k' := by intro f _ M hM simp only [P_eq, HeavyBranchFold.toFinsetEquation, List.mem_toFinset, List.mem_map] at hM diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean index 573698f9c..29e740a9d 100644 --- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean +++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceSemantics.lean @@ -472,7 +472,8 @@ private theorem varIncidence_listScopeFamily_augScopes_le (n' : ℕ) (eqs' : Lis ← (List.ofFn_eq_map.symm.trans (List.ofFn_getElem (xs := scopes))), List.countP_map] exact List.countP_congr fun i _ => by simp only [Function.comp_apply, Fin.getElem_fin] rw [hdeg] - exact le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_range.mpr v.isLt)) + exact List.le_max_of_mem (l := 0 :: (List.range n').map (varDegree · eqs')) + (List.mem_cons_of_mem 0 (List.mem_map_of_mem (List.mem_range.mpr v.isLt))) private theorem card_listScopeFamily_augScopes_le (n' : ℕ) (eqs' : List (List (List ℕ))) : let augScopes := withNeutralScopesList (eqs'.map equationVars) n' @@ -489,7 +490,7 @@ private theorem card_listScopeFamily_augScopes_le (n' : ℕ) (eqs' : List (List have hsc := listScopeFamily_map_equationVars n' eqs' ⟨g.1, hg⟩ change listScopeFamily n' scopes g = _ at hsc rw [hsc, card_equationScope_toFinsetEquation, branchMaxFactorWidth] - exact le_foldl_max_of_mem (List.mem_map_of_mem (List.getElem_mem hg)) + exact List.le_max_of_mem (List.mem_cons_of_mem _ (List.mem_map_of_mem (List.getElem_mem hg))) · dsimp only [withNeutralScope] rw [card_singleton] exact one_le_branchMaxFactorWidth n' eqs' diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean index be24fe4a5..c9f377b3c 100644 --- a/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean +++ b/Complexity/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceStepCert.lean @@ -579,12 +579,16 @@ def maxAllGroupDim (n' Q_u r_u : ℕ) (varGroups : List (List (List ℕ))) : ℕ private theorem min_length_le_maxGroupDim {n' r_u g : ℕ} {vGroups_t : List (List ℕ)} (hg : g < r_u) : min (2 * n') (vGroups_t.getD g []).length ≤ maxGroupDim n' r_u vGroups_t := - le_foldl_max_of_mem (List.mem_map.mpr ⟨g, List.mem_range.mpr hg, rfl⟩) + List.le_max_of_mem + (l := 0 :: (List.range r_u).map (fun g => min (2 * n') (vGroups_t.getD g []).length)) + (List.mem_cons_of_mem _ (List.mem_map.mpr ⟨g, List.mem_range.mpr hg, rfl⟩)) private theorem maxGroupDim_le_maxAllGroupDim {n' Q_u r_u t : ℕ} {varGroups : List (List (List ℕ))} (ht : t < Q_u) : maxGroupDim n' r_u (varGroups.getD t []) ≤ maxAllGroupDim n' Q_u r_u varGroups := - le_foldl_max_of_mem (List.mem_map.mpr ⟨t, List.mem_range.mpr ht, rfl⟩) + List.le_max_of_mem + (l := 0 :: (List.range Q_u).map (fun t => maxGroupDim n' r_u (varGroups.getD t []))) + (List.mem_cons_of_mem _ (List.mem_map.mpr ⟨t, List.mem_range.mpr ht, rfl⟩)) private theorem foldl_optAddJet_spec (J ℓ j M : ℕ) (f : ℕ → Option JetRows) (hf : ∀ i < j, ∀ y, f i = some y → ∀ j' < J, ∀ u' < ℓ, (rowEntry y j' u').natAbs ≤ M) : diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean index d6fb6e70b..3c6cf02a5 100644 --- a/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean +++ b/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean @@ -219,23 +219,6 @@ def branchNeutralScope (n' : ℕ) (eqs' : List (List (List ℕ))) : Fin eqs'.length ⊕ Fin n' → Finset (Fin n') := withNeutralScope fun i => equationScope (HeavyBranchFold.toFinsetEquation n' eqs'[i]) -theorem foldl_max_le_iff {l : List ℕ} {init B : ℕ} : - l.foldl max init ≤ B ↔ init ≤ B ∧ ∀ x ∈ l, x ≤ B := by - induction l generalizing init with - | nil => simp only [List.foldl_nil, List.not_mem_nil, IsEmpty.forall_iff, implies_true, and_true] - | cons a as ih => - simp only [List.foldl_cons, ih, Nat.max_le, List.mem_cons, forall_eq_or_imp, and_assoc] - -theorem foldl_max_le {l : List ℕ} {init B : ℕ} (hinit : init ≤ B) (hl : ∀ x ∈ l, x ≤ B) : - l.foldl max init ≤ B := - foldl_max_le_iff.mpr ⟨hinit, hl⟩ - -theorem le_foldl_max_init (init : ℕ) (l : List ℕ) : init ≤ l.foldl max init := - (foldl_max_le_iff.mp le_rfl).1 - -theorem le_foldl_max_of_mem {init : ℕ} {l : List ℕ} {x : ℕ} (hx : x ∈ l) : - x ≤ l.foldl max init := (foldl_max_le_iff.mp le_rfl).2 x hx - theorem checkVarsLt_eq_true_iff {n : ℕ} {sys : List (List (List ℕ))} : checkVarsLt n sys = true ↔ ∀ eq ∈ sys, ∀ m ∈ eq, ∀ v ∈ m, v < n := by simp only [checkVarsLt, List.all_eq_true, decide_eq_true_eq] @@ -309,11 +292,14 @@ theorem card_equationScope_toFinsetEquation (n : ℕ) (eq : List (List ℕ)) : theorem length_mem_le_sysMaxDegree {sys : List (List (List ℕ))} {eq : List (List ℕ)} (heq : eq ∈ sys) {m : List ℕ} (hm : m ∈ eq) : m.length ≤ sysMaxDegree sys := - le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_flatten.mpr ⟨eq, heq, hm⟩)) + List.le_max_of_mem + (List.mem_cons_of_mem _ (List.mem_map_of_mem (List.mem_flatten.mpr ⟨eq, heq, hm⟩))) theorem sysMaxDegree_le_iff {sys : List (List (List ℕ))} {k : ℕ} : sysMaxDegree sys ≤ k ↔ ∀ eq ∈ sys, ∀ m ∈ eq, m.length ≤ k := by - simp only [sysMaxDegree, foldl_max_le_iff, Nat.zero_le, true_and, List.mem_map, List.mem_flatten] + change (0 :: sys.flatten.map List.length).max (by simp) ≤ k ↔ _ + simp only [List.max_le_iff, List.mem_cons, forall_eq_or_imp, Nat.zero_le, true_and, + List.mem_map, List.mem_flatten] exact ⟨fun h eq heq m hm => h m.length ⟨m, ⟨eq, heq, hm⟩, rfl⟩, fun h _ ⟨m, ⟨eq, heq, hm⟩, hm_eq⟩ => hm_eq ▸ h eq heq m hm⟩ @@ -321,7 +307,7 @@ theorem one_le_branchMaxFactorIncidence (n' : ℕ) (eqs' : List (List (List ℕ) 1 ≤ branchMaxFactorIncidence n' eqs' := Nat.succ_pos _ theorem one_le_branchMaxFactorWidth (n' : ℕ) (eqs' : List (List (List ℕ))) : - 1 ≤ branchMaxFactorWidth n' eqs' := le_foldl_max_init 1 _ + 1 ≤ branchMaxFactorWidth n' eqs' := List.le_max_of_mem List.mem_cons_self theorem le_branchAugmentedIncidence (n' : ℕ) (eqs' : List (List (List ℕ))) : n' ≤ branchAugmentedIncidence n' eqs' := Nat.le_add_left _ _ @@ -362,14 +348,17 @@ theorem varIncidence_branchNeutralScope_le (n' : ℕ) (eqs' : List (List (List (branchNeutralScope n' eqs') v ≤ _ rw [← withNeutralFactors_univ, branchNeutralScope, varIncidence_withNeutralFactors, varIncidence_toFinsetEquation_eq_varDegree, branchMaxFactorIncidence] - exact Nat.succ_le_succ (le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_range.mpr v.isLt))) + apply Nat.succ_le_succ + exact List.le_max_of_mem (l := 0 :: (List.range n').map (varDegree · eqs')) + (List.mem_cons_of_mem 0 (List.mem_map_of_mem (List.mem_range.mpr v.isLt))) theorem card_branchNeutralScope_le (n' : ℕ) (eqs' : List (List (List ℕ))) (f : Fin eqs'.length ⊕ Fin n') : #(branchNeutralScope n' eqs' f) ≤ branchMaxFactorWidth n' eqs' := card_withNeutralScope_le (one_le_branchMaxFactorWidth n' eqs') (fun i : Fin eqs'.length => (card_equationScope_toFinsetEquation n' eqs'[i]).trans_le - (le_foldl_max_of_mem (List.mem_map_of_mem (List.getElem_mem i.isLt)))) f + (List.le_max_of_mem + (List.mem_cons_of_mem _ (List.mem_map_of_mem (List.getElem_mem i.isLt))))) f theorem branchAugmentedIncidence_le_mul (n' : ℕ) (eqs' : List (List (List ℕ))) : branchAugmentedIncidence n' eqs' ≤ branchMaxFactorIncidence n' eqs' * n' := by @@ -377,7 +366,8 @@ theorem branchAugmentedIncidence_le_mul (n' : ℕ) (eqs' : List (List (List ℕ) (scope := fun i => equationScope (HeavyBranchFold.toFinsetEquation n' eqs'[i])) (b₀ := ((List.range n').map fun v => varDegree v eqs').foldl max 0) (fun v => (varIncidence_toFinsetEquation_eq_varDegree n' eqs' v).trans_le - (le_foldl_max_of_mem (List.mem_map_of_mem (List.mem_range.mpr v.isLt)))) + (List.le_max_of_mem (l := 0 :: (List.range n').map (varDegree · eqs')) + (List.mem_cons_of_mem 0 (List.mem_map_of_mem (List.mem_range.mpr v.isLt))))) rw [withNeutralFactors_univ, ← branchNeutralScope, Fintype.card_fin, ← branchMaxFactorIncidence, totalIncidence] at hle rwa [← sum_card_branchNeutralScope] @@ -511,7 +501,9 @@ private theorem unaryFoldMax (init : ℕ) : id' (const init) (by fun_prop) (B := fun l => init + (encList encUnary l).length) ((PolyBounded.const init).add .self) (fun l i _ => ?_) simp only [encUnary_apply, List.length_replicate] - refine foldl_max_le_iff.mpr ⟨Nat.le_add_right _ _, fun x hx => ?_⟩ + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨Nat.le_add_right _ _, fun x hx => ?_⟩ have hsz := SizedListEncoding.length_elem_le (encA := encUnary) (encL := encList encUnary) l x (List.mem_of_mem_take hx) simp only [encUnary_apply, List.length_replicate] at hsz; omega @@ -844,17 +836,23 @@ theorem reduced_branch_invariants {N₀_top : ℕ} {inp : SparseSystemInput} {va have hS_half := hS_le.trans (Nat.div_le_div_left hs2 (by omega)) have hvd' := HeavyBranchFold.prepareBranch_reduced_varDegree_le hS_nd hSn (fun u hun huS => HeavyBranchFold.varDegree_le_of_not_mem_heavyVarList hun huS) hred - have hb' : branchMaxFactorIncidence n' sys' ≤ inp.2.1.2.2 + 1 := - Nat.succ_le_succ (foldl_max_le_iff.mpr ⟨Nat.zero_le _, fun x hx => by - obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hx; exact hvd' v (List.mem_range.mp hv)⟩) - have hw' : branchMaxFactorWidth n' sys' ≤ branchMaxFactorWidth inp.1 inp.2.2 := - foldl_max_le_iff.mpr ⟨one_le_branchMaxFactorWidth inp.1 inp.2.2, fun x hx => by - obtain ⟨eq', heq', rfl⟩ := List.mem_map.mp hx - obtain ⟨eq₀, heq₀, _, hsc⟩ := - (HeavyBranchFold.prepareBranch_reduced_length_le hred).2 eq' heq' - rw [scopeWidthOn_eq_length_equationVars (hvars' eq' heq')] - exact (hsc.trans_eq (scopeWidthOn_eq_length_equationVars (hvars eq₀ heq₀)).symm).trans - (le_foldl_max_of_mem (List.mem_map_of_mem heq₀))⟩ + have hb' : branchMaxFactorIncidence n' sys' ≤ inp.2.1.2.2 + 1 := by + apply Nat.succ_le_succ + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨Nat.zero_le _, fun x hx => ?_⟩ + obtain ⟨v, hv, rfl⟩ := List.mem_map.mp hx + exact hvd' v (List.mem_range.mp hv) + have hw' : branchMaxFactorWidth n' sys' ≤ branchMaxFactorWidth inp.1 inp.2.2 := by + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨one_le_branchMaxFactorWidth inp.1 inp.2.2, fun x hx => ?_⟩ + obtain ⟨eq', heq', rfl⟩ := List.mem_map.mp hx + obtain ⟨eq₀, heq₀, _, hsc⟩ := + (HeavyBranchFold.prepareBranch_reduced_length_le hred).2 eq' heq' + rw [scopeWidthOn_eq_length_equationVars (hvars' eq' heq')] + exact (hsc.trans_eq (scopeWidthOn_eq_length_equationVars (hvars eq₀ heq₀)).symm).trans + (List.le_max_of_mem (List.mem_cons_of_mem _ (List.mem_map_of_mem heq₀))) exact ⟨hn'_eq, by omega, hcan', hvars', HeavyBranchFold.prepareBranch_reduced_degree_le hdeg hred, hb', hw'⟩ @@ -947,14 +945,19 @@ private theorem le_maxReducedCost (cost : ℕ × List (List (List ℕ)) → ℕ) (hred : HeavyBranchFold.prepareBranch inp.1 inp.2.1 (lowBits inp.2.1.length idx) inp.2.2 = .reduced n' sys') : cost (n', sys') ≤ maxReducedCost cost inp := by unfold maxReducedCost - refine le_foldl_max_of_mem (List.mem_map.mpr ⟨idx, List.mem_range.mpr hidx, ?_⟩); rw [hred] + refine List.le_max_of_mem + (List.mem_cons_of_mem _ (List.mem_map.mpr ⟨idx, List.mem_range.mpr hidx, ?_⟩)) + rw [hred] theorem maxReducedCost_le {cost : ℕ × List (List (List ℕ)) → ℕ} {inp : HeavyBranchFold.BranchInput} {B : ℕ} (hB : ∀ idx < 2 ^ inp.2.1.length, ∀ n' sys', HeavyBranchFold.prepareBranch inp.1 inp.2.1 (lowBits inp.2.1.length idx) inp.2.2 = .reduced n' sys' → cost (n', sys') ≤ B) : maxReducedCost cost inp ≤ B := by - unfold maxReducedCost; refine foldl_max_le_iff.mpr ⟨Nat.zero_le B, fun x hx => ?_⟩ + unfold maxReducedCost + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨Nat.zero_le B, fun x hx => ?_⟩ obtain ⟨idx, hidx, rfl⟩ := List.mem_map.mp hx cases hout : HeavyBranchFold.prepareBranch inp.1 inp.2.1 (lowBits inp.2.1.length idx) inp.2.2 with | contradiction | tautology _ => exact Nat.zero_le B diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean index 0e9d4fa9f..a09c43261 100644 --- a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean +++ b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean @@ -566,7 +566,9 @@ private theorem compiled_system_incidence_bounds (k C_B β_B : ℕ) : Nat.pow_le_pow_right hlam1 (by omega) have hw_le : branchMaxFactorWidth N sys ≤ C_inc * lam ^ (2 * β_B + 4) := by unfold branchMaxFactorWidth - refine foldl_max_le (Nat.mul_pos (by dsimp only [C_inc]; omega) hpow1) fun w hw => ?_ + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨Nat.mul_pos (by dsimp only [C_inc]; omega) hpow1, fun w hw => ?_⟩ obtain ⟨eq, heq, rfl⟩ := List.mem_map.mp hw have h1 := (hsc_all eq heq).trans (hT_le.trans (Nat.mul_le_mul_left _ hpow_step)) dsimp only [C_inc]; nlinarith diff --git a/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean b/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean index 79db39677..29fb9106f 100644 --- a/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean +++ b/ComplexityTests/Computability/PolyTime/BooleanAnalysis/BoundedIncidenceExactness.lean @@ -75,13 +75,6 @@ example : simp only [← countSystemExhaustive_eq_rootCount] decide +kernel -private theorem foldl_max_le_of_all {B : ℕ} : - ∀ (init : ℕ) (l : List ℕ), init ≤ B → (∀ x ∈ l, x ≤ B) → l.foldl max init ≤ B - | _, [], hi, _ => hi - | init, a :: as, hi, hall => - foldl_max_le_of_all (max init a) as (Nat.max_le.mpr ⟨hi, hall a List.mem_cons_self⟩) - fun x hx => hall x (List.mem_cons_of_mem a hx) - /-- Nonvacuous feasible witnesses for `evalBoundedIncidenceBranch_eq_rootCount`: there exists a concrete dimension `n' ≥ 20` on which both `(n', [])` and the nonlinear quadratic system `(n', [[[0, 1], []]])` pass `checkBranchFeasible 0` and execute the non-fallback branch evaluator @@ -98,9 +91,13 @@ example : ∃ n' : ℕ, 20 ≤ n' ∧ have hlam : 2 ≤ Nat.clog 2 N₁ := (show 2 = Nat.clog 2 (2 ^ 2) from (Nat.clog_pow 2 2 Nat.one_lt_two).symm).trans_le (Nat.clog_mono_right 2 (by omega)) - have hb0 : branchMaxFactorIncidence N₁ [] ≤ 2 := - Nat.succ_le_succ (foldl_max_le_of_all 0 _ (Nat.zero_le 1) fun x hx => by - obtain ⟨_, _, rfl⟩ := List.mem_map.mp hx; exact Nat.zero_le 1) + have hb0 : branchMaxFactorIncidence N₁ [] ≤ 2 := by + apply Nat.succ_le_succ + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨Nat.zero_le 1, fun x hx => ?_⟩ + obtain ⟨_, _, rfl⟩ := List.mem_map.mp hx + exact Nat.zero_le 1 have hfeas0 : checkBranchFeasible 0 (N₁, []) = true := (hth le_rfl (by simp only [List.not_mem_nil, IsEmpty.forall_iff, implies_true]) (by simp only [List.not_mem_nil, IsEmpty.forall_iff, implies_true]) @@ -109,9 +106,14 @@ example : ∃ n' : ℕ, 20 ≤ n' ∧ checkVarsLt_eq_true_iff.mp (by decide +kernel) have hvars1 : ∀ eq ∈ ([[[0, 1], []]] : List (List (List ℕ))), ∀ m ∈ eq, ∀ v ∈ m, v < N₁ := fun eq heq m hm v hv => (hvars2 eq heq m hm v hv).trans_le (by omega) - have hb1 : branchMaxFactorIncidence N₁ [[[0, 1], []]] ≤ 2 := - Nat.succ_le_succ (foldl_max_le_of_all 0 _ (Nat.zero_le 1) fun x hx => by - obtain ⟨_, _, rfl⟩ := List.mem_map.mp hx; unfold varDegree; exact List.countP_le_length) + have hb1 : branchMaxFactorIncidence N₁ [[[0, 1], []]] ≤ 2 := by + apply Nat.succ_le_succ + refine (List.max_le_iff (l := _ :: _) (by simp)).mpr ?_ + simp only [List.mem_cons, forall_eq_or_imp] + refine ⟨Nat.zero_le 1, fun x hx => ?_⟩ + obtain ⟨_, _, rfl⟩ := List.mem_map.mp hx + unfold varDegree + exact List.countP_le_length have hw1 : branchMaxFactorWidth N₁ [[[0, 1], []]] = 2 := by unfold branchMaxFactorWidth simp only [List.map_cons, List.map_nil, List.foldl_cons, List.foldl_nil]