Wilf inequality for proper numerical semigroups with conductor at most four times multiplicity

-- Submission body for math30catalog-source23 (Wilf's inequality for numerical semigroups with c ≤ 4m).
-- Blueprint: experiments/astra/BLUEPRINT.md. Each `sorry` below is an open blueprint node.
-- Infrastructure lemmas (prefix w23_) come from audited sub-task fragments; see experiments/astra/merged/.

open Math30 Math30.Wilf
open scoped Pointwise

/-- A1: the least positive element is no larger than the conductor. -/
theorem w22_multiplicity_le_conductor (S : NumericalSemigroup) :
    S.multiplicity ≤ S.conductor :=
  S.multiplicity_le S.conductor_pos (S.conductor_spec _ (le_refl _))

theorem w22_conductor_eq_multiplicity (S : NumericalSemigroup)
    (h : S.conductor ≤ S.multiplicity) : S.conductor = S.multiplicity :=
  Nat.le_antisymm h (w22_multiplicity_le_conductor S)

/-- A2: the full conductor block belongs to the semigroup. -/
theorem w22_mem_of_conductor_le (S : NumericalSemigroup) {x : ℕ}
    (h : S.conductor ≤ x) : x ∈ S.carrier := S.conductor_spec x h

theorem w22_conductor_block_filter (S : NumericalSemigroup) :
    (@Finset.filter ℕ (fun x => x ∈ S.carrier) (Classical.decPred _)
      (Finset.Ico S.conductor (S.conductor + S.multiplicity))) = Finset.Ico S.conductor (S.conductor + S.multiplicity) := by
  classical
  apply Finset.filter_eq_self.mpr
  intro x hx
  exact S.conductor_spec x (Finset.mem_Ico.mp hx).1

/-- A3: primitives and the multiplicity. -/
theorem w22_primitives_subset (S : NumericalSemigroup) :
    S.primitiveElements ⊆ Finset.Ico S.multiplicity (S.conductor + S.multiplicity) := by
  intro x hx
  have hp := (S.mem_primitiveElements x).mp hx
  exact Finset.mem_Ico.mpr ⟨S.multiplicity_le hp.2.1 hp.1, S.primitive_lt hp⟩

theorem w22_multiplicity_mem_primitives (S : NumericalSemigroup) :
    S.multiplicity ∈ S.primitiveElements :=
  (S.mem_primitiveElements _).mpr S.multiplicity_isPrimitive

theorem w22_primitive_sub_multiplicity_not_mem (S : NumericalSemigroup) {x : ℕ}
    (hp : S.IsPrimitive x) (hne : x ≠ S.multiplicity) :
    x - S.multiplicity ∉ S.carrier := by
  intro hsub
  have hle := S.multiplicity_le hp.2.1 hp.1
  have hm := S.multiplicity_pos
  have hzero := hp.2.2 S.multiplicity (x - S.multiplicity) S.multiplicity_mem hsub (by omega)
  omega

/-- A4: primitive generation and positive decomposition. -/
theorem w22_generated_by_primitives (S : NumericalSemigroup) {x : ℕ}
    (hx : x ∈ S.carrier) : x ∈ AddSubmonoid.closure {n | S.IsPrimitive n} := by
  rw [S.closure_primitives]
  exact hx

theorem w22_primitive_or_decomposition (S : NumericalSemigroup) {x : ℕ}
    (hx : x ∈ S.carrier) (hpos : 0 < x) :
    S.IsPrimitive x ∨ ∃ y z, y ∈ S.carrier ∧ z ∈ S.carrier ∧
      0 < y ∧ 0 < z ∧ x = y + z := by
  classical
  by_cases hp : S.IsPrimitive x
  · exact Or.inl hp
  · right
    have hd : ¬ ∀ y z, y ∈ S.carrier → z ∈ S.carrier →
        x = y + z → y = 0 ∨ z = 0 := by
      intro hall
      exact hp ⟨hx, hpos, hall⟩
    push Not at hd
    obtain ⟨y, z, hy, hz, he, hy0, hz0⟩ := hd
    exact ⟨y, z, hy, hz, by omega, by omega, he⟩

/-- A4 in explicit finite-sum form, including zero as the empty sum. -/
theorem w22_sum_of_primitives (S : NumericalSemigroup) {x : ℕ}
    (hx : x ∈ S.carrier) :
    ∃ l : List ℕ, (∀ p ∈ l, S.IsPrimitive p) ∧ l.sum = x := by
  have hgen : ∀ x : ℕ, x ∈ S.carrier →
      ∃ l : List ℕ, (∀ p ∈ l, S.IsPrimitive p) ∧ l.sum = x := by
    intro x
    induction x using Nat.strong_induction_on with
    | h x ih =>
      intro hx
      by_cases hz : x = 0
      · subst x
        exact ⟨[], by simp, by simp⟩
      · rcases w22_primitive_or_decomposition S hx (by omega) with hp | ⟨a, b, ha, hb, hap, hbp, he⟩
        · exact ⟨[x], by simpa using hp, by simp⟩
        · obtain ⟨la, hla, hsa⟩ := ih a (by omega) ha
          obtain ⟨lb, hlb, hsb⟩ := ih b (by omega) hb
          refine ⟨la ++ lb, ?_, ?_⟩
          · intro p hp
            rcases List.mem_append.mp hp with hpa | hpb
            · exact hla p hpa
            · exact hlb p hpb
          · simpa only [List.sum_append, hsa, hsb] using he.symm
  exact hgen x hx

/-- A5: elements below twice the multiplicity are indecomposable. -/
theorem w22_primitive_of_lt_two_multiplicity (S : NumericalSemigroup) {x : ℕ}
    (hx : x ∈ S.carrier) (hpos : 0 < x) (hlt : x < 2 * S.multiplicity) :
    S.IsPrimitive x := by
  refine ⟨hx, hpos, ?_⟩
  intro a b ha hb he
  by_cases ha0 : a = 0
  · exact Or.inl ha0
  · by_cases hb0 : b = 0
    · exact Or.inr hb0
    · have hma := S.multiplicity_le (by omega : 0 < a) ha
      have hmb := S.multiplicity_le (by omega : 0 < b) hb
      omega

noncomputable def w22_leftPrimitives (S : NumericalSemigroup) : Finset ℕ :=
  S.primitiveElements.filter (fun x => x < S.conductor)

noncomputable def w22_rightPrimitives (S : NumericalSemigroup) : Finset ℕ :=
  S.primitiveElements.filter (fun x => S.conductor ≤ x)

/-- A6: zero together with all positive left elements. -/
theorem w22_leftElements_split (S : NumericalSemigroup) :
    S.leftElements = {0} ∪ (@Finset.filter ℕ (fun x => x ∈ S.carrier) (Classical.decPred _)
      (Finset.Ico 1 S.conductor)) := by
  classical
  ext x
  simp only [S.mem_leftElements, Finset.mem_union, Finset.mem_singleton,
    Finset.mem_filter, Finset.mem_Ico]
  have h0 := S.carrier.zero_mem
  have hc := S.conductor_pos
  constructor
  · rintro ⟨hlt, hx⟩
    by_cases hz : x = 0
    · exact Or.inl hz
    · exact Or.inr ⟨⟨by omega, hlt⟩, hx⟩
  · rintro (rfl | ⟨⟨_, hlt⟩, hx⟩)
    · exact ⟨hc, h0⟩
    · exact ⟨hlt, hx⟩

theorem w22_leftElements_eq_insert_primitives (S : NumericalSemigroup)
    (h : S.conductor ≤ 2 * S.multiplicity) :
    S.leftElements = insert 0 (w22_leftPrimitives S) := by
  classical
  ext x
  simp only [S.mem_leftElements, Finset.mem_insert, w22_leftPrimitives,
    Finset.mem_filter, S.mem_primitiveElements]
  constructor
  · rintro ⟨hlt, hx⟩
    by_cases hz : x = 0
    · exact Or.inl hz
    · exact Or.inr ⟨w22_primitive_of_lt_two_multiplicity S hx (by omega) (by omega), hlt⟩
  · rintro (rfl | ⟨hp, hlt⟩)
    · exact ⟨S.conductor_pos, S.carrier.zero_mem⟩
    · exact ⟨hlt, hp.1⟩

theorem w22_leftCount_eq (S : NumericalSemigroup)
    (h : S.conductor ≤ 2 * S.multiplicity) :
    S.leftCount = 1 + (w22_leftPrimitives S).card := by
  classical
  have h0 : 0 ∉ w22_leftPrimitives S := by
    simp only [w22_leftPrimitives, Finset.mem_filter, S.mem_primitiveElements]
    intro hp
    exact Nat.lt_irrefl 0 hp.1.2.1
  unfold NumericalSemigroup.leftCount
  rw [w22_leftElements_eq_insert_primitives S h, Finset.card_insert_of_notMem h0]
  omega

theorem w22_primitive_counts (S : NumericalSemigroup) :
    (w22_leftPrimitives S).card + (w22_rightPrimitives S).card = S.embeddingDimension := by
  classical
  simpa only [w22_leftPrimitives, w22_rightPrimitives, not_lt,
    NumericalSemigroup.embeddingDimension] using
    (Finset.card_filter_add_card_filter_not (s := S.primitiveElements) (fun x => x < S.conductor))

theorem w22_left_multiples (S : NumericalSemigroup) {q : ℕ}
    (h : ∀ k < q, k * S.multiplicity < S.conductor) :
    (Finset.range q).image (fun k => k * S.multiplicity) ⊆ S.leftElements := by
  classical
  intro x hx
  obtain ⟨k, hk, rfl⟩ := Finset.mem_image.mp hx
  refine (S.mem_leftElements _).mpr ⟨h k (Finset.mem_range.mp hk), ?_⟩
  simpa using S.carrier.nsmul_mem S.multiplicity_mem k

theorem w22_leftCount_ge_multiples (S : NumericalSemigroup) {q : ℕ}
    (h : ∀ k < q, k * S.multiplicity < S.conductor) : q ≤ S.leftCount := by
  classical
  have hm := S.multiplicity_pos
  have hinj : Function.Injective (fun k : ℕ => k * S.multiplicity) := by
    intro a b hab
    nlinarith
  have hc := Finset.card_le_card (w22_left_multiples S h)
  rw [Finset.card_image_of_injective _ hinj, Finset.card_range] at hc
  exact hc

theorem w22_ceil_conductor_le_leftCount (S : NumericalSemigroup) :
    (S.conductor + S.multiplicity - 1) / S.multiplicity ≤ S.leftCount := by
  apply w22_leftCount_ge_multiples
  intro k hk
  have hm := S.multiplicity_pos
  have hc := S.conductor_pos
  have hd := Nat.div_mul_le_self (S.conductor + S.multiplicity - 1) S.multiplicity
  have hs : S.conductor + S.multiplicity - 1 + 1 = S.conductor + S.multiplicity := by omega
  have hkq := Nat.mul_le_mul_right S.multiplicity (Nat.succ_le_of_lt hk)
  nlinarith

theorem w22_ordinary_mem_iff (S : NumericalSemigroup)
    (h : S.conductor ≤ S.multiplicity) (x : ℕ) :
    x ∈ S.carrier ↔ x = 0 ∨ S.multiplicity ≤ x := by
  constructor
  · intro hx
    by_cases hz : x = 0
    · exact Or.inl hz
    · exact Or.inr (S.multiplicity_le (by omega) hx)
  · rintro (rfl | hmx)
    · exact S.carrier.zero_mem
    · exact S.conductor_spec x (le_trans h hmx)

/-- The ordinary case, including its exact invariant values. -/
theorem w22_ordinary_invariants (S : NumericalSemigroup)
    (h : S.conductor ≤ S.multiplicity) :
    S.conductor = S.multiplicity ∧ S.leftCount = 1 ∧ S.embeddingDimension = S.multiplicity := by
  classical
  have he := w22_conductor_eq_multiplicity S h
  have hl : S.leftElements = {0} := by
    ext x
    simp only [S.mem_leftElements, Finset.mem_singleton]
    constructor
    · rintro ⟨hlt, hx⟩
      by_contra hx0
      have hm := S.multiplicity_le (by omega : 0 < x) hx
      omega
    · intro hx0
      subst x
      exact ⟨S.conductor_pos, S.carrier.zero_mem⟩
  have hp : S.primitiveElements = Finset.Ico S.multiplicity (2 * S.multiplicity) := by
    ext x
    simp only [S.mem_primitiveElements, Finset.mem_Ico]
    constructor
    · intro hx
      have hle := S.multiplicity_le hx.2.1 hx.1
      have hlt := S.primitive_lt hx
      exact ⟨hle, by omega⟩
    · rintro ⟨hle, hlt⟩
      exact w22_primitive_of_lt_two_multiplicity S
        (S.conductor_spec x (by omega)) (lt_of_lt_of_le S.multiplicity_pos hle) hlt
  refine ⟨he, ?_, ?_⟩
  · simp [NumericalSemigroup.leftCount, hl]
  · simp [NumericalSemigroup.embeddingDimension, hp, Nat.two_mul]

/-- Every decomposable element of the conductor block is a sum of two left primitives. -/
theorem w22_block_coverage (S : NumericalSemigroup)
    (h : S.conductor ≤ 2 * S.multiplicity) :
    Finset.Ico S.conductor (S.conductor + S.multiplicity) ⊆
      w22_rightPrimitives S ∪ (w22_leftPrimitives S).sym2.image Sym2.add := by
  classical
  intro x hx
  obtain ⟨hc, hlt⟩ := Finset.mem_Ico.mp hx
  have hxS := S.conductor_spec x hc
  have hpos : 0 < x := lt_of_lt_of_le S.conductor_pos hc
  rcases w22_primitive_or_decomposition S hxS hpos with hp | ⟨a, b, ha, hb, hap, hbp, he⟩
  · apply Finset.mem_union_left
    exact Finset.mem_filter.mpr ⟨(S.mem_primitiveElements x).mpr hp, hc⟩
  · have hma := S.multiplicity_le hap ha
    have hmb := S.multiplicity_le hbp hb
    have hal : a < S.conductor := by omega
    have hbl : b < S.conductor := by omega
    have hpa := w22_primitive_of_lt_two_multiplicity S ha hap (by omega)
    have hpb := w22_primitive_of_lt_two_multiplicity S hb hbp (by omega)
    apply Finset.mem_union_right
    apply Finset.mem_image.mpr
    refine ⟨Sym2.mk a b, ?_, ?_⟩
    · exact Finset.mk_mem_sym2_iff.mpr
        ⟨Finset.mem_filter.mpr ⟨(S.mem_primitiveElements a).mpr hpa, hal⟩,
         Finset.mem_filter.mpr ⟨(S.mem_primitiveElements b).mpr hpb, hbl⟩⟩
    · simpa using he.symm

theorem w22_kaplan_count (S : NumericalSemigroup)
    (h : S.conductor ≤ 2 * S.multiplicity) :
    S.multiplicity ≤ (w22_rightPrimitives S).card +
      ((w22_leftPrimitives S).card + 1).choose 2 := by
  classical
  have hb := Finset.card_le_card (w22_block_coverage S h)
  have hu := Finset.card_union_le (w22_rightPrimitives S)
    ((w22_leftPrimitives S).sym2.image Sym2.add)
  have hi := Finset.card_image_le (s := (w22_leftPrimitives S).sym2) (f := Sym2.add)
  rw [Finset.card_sym2] at hi
  have hc : (Finset.Ico S.conductor (S.conductor + S.multiplicity)).card = S.multiplicity := by
    simp
  omega

theorem w22_two_mul_choose (n : ℕ) : 2 * (n + 1).choose 2 = n * (n + 1) := by
  have h := Nat.add_one_mul_choose_eq n 1
  simpa [Nat.mul_comm] using h.symm

/-- Kaplan's theorem: conductor at most twice the multiplicity implies Wilf. -/
theorem w22_kaplan (S : NumericalSemigroup) (h : S.conductor ≤ 2 * S.multiplicity) :
    S.SatisfiesWilf := by
  classical
  unfold NumericalSemigroup.SatisfiesWilf
  by_cases hc : S.conductor ≤ S.multiplicity
  · obtain ⟨he, hl, hp⟩ := w22_ordinary_invariants S hc
    rw [he, hl, hp, Nat.mul_one]
  · have hmc : S.multiplicity < S.conductor := by omega
    let n := (w22_leftPrimitives S).card
    let r := (w22_rightPrimitives S).card
    have hn : 1 ≤ n := by
      have hm : S.multiplicity ∈ w22_leftPrimitives S :=
        Finset.mem_filter.mpr ⟨w22_multiplicity_mem_primitives S, hmc⟩
      have hp := Finset.card_pos.mpr ⟨S.multiplicity, hm⟩
      exact hp
    have he : n + r = S.embeddingDimension := w22_primitive_counts S
    have hl : S.leftCount = 1 + n := w22_leftCount_eq S h
    have hb : S.multiplicity ≤ r + (n + 1).choose 2 := w22_kaplan_count S h
    have ht := w22_two_mul_choose n
    have hr : 0 ≤ r * (n - 1) := Nat.zero_le _
    have hn1 : n - 1 + 1 = n := by omega
    rw [hl, ← he]
    nlinarith


/-- A7: a residue always occurs, by cofiniteness. -/
theorem w22_exists_residue (S : NumericalSemigroup) (i : Fin S.multiplicity) :
    ∃ x : ℕ, x ∈ S.carrier ∧ x % S.multiplicity = i.val := by
  refine ⟨S.conductor * S.multiplicity + i.val, ?_, ?_⟩
  · apply S.conductor_spec
    have hm := S.multiplicity_pos
    nlinarith
  · simp [Nat.add_mod, Nat.mod_eq_of_lt i.isLt]

noncomputable def w22_apery (S : NumericalSemigroup) (i : Fin S.multiplicity) : ℕ := by
  classical
  exact Nat.find (w22_exists_residue S i)

theorem w22_apery_mem (S : NumericalSemigroup) (i : Fin S.multiplicity) :
    w22_apery S i ∈ S.carrier := by
  classical
  exact (Nat.find_spec (w22_exists_residue S i)).1

theorem w22_apery_mod (S : NumericalSemigroup) (i : Fin S.multiplicity) :
    w22_apery S i % S.multiplicity = i.val := by
  classical
  exact (Nat.find_spec (w22_exists_residue S i)).2

theorem w22_apery_min (S : NumericalSemigroup) (i : Fin S.multiplicity) {x : ℕ}
    (hx : x ∈ S.carrier) (hi : x % S.multiplicity = i.val) : w22_apery S i ≤ x := by
  classical
  exact Nat.find_min' (w22_exists_residue S i) ⟨hx, hi⟩

theorem w22_apery_lt (S : NumericalSemigroup) (i : Fin S.multiplicity) :
    w22_apery S i < S.conductor + S.multiplicity := by
  by_contra hlt
  have hc := S.conductor_pos
  have hm := S.multiplicity_pos
  have hsub : w22_apery S i - S.multiplicity ∈ S.carrier :=
    S.conductor_spec _ (by omega)
  have he : w22_apery S i - S.multiplicity + S.multiplicity = w22_apery S i := by omega
  have hr : (w22_apery S i - S.multiplicity) % S.multiplicity = i.val := by
    calc
      _ = (w22_apery S i - S.multiplicity + S.multiplicity) % S.multiplicity :=
        (Nat.add_mod_right _ _).symm
      _ = i.val := by rw [he, w22_apery_mod]
  have hmin := w22_apery_min S i hsub hr
  omega

/-- An element above the residue's Apéry representative is in the semigroup. -/
theorem w22_mem_of_apery_le (S : NumericalSemigroup) (i : Fin S.multiplicity) {x : ℕ}
    (hi : x % S.multiplicity = i.val) (hle : w22_apery S i ≤ x) : x ∈ S.carrier := by
  have hdiv := Nat.div_le_div_right (c := S.multiplicity) hle
  have hw := Nat.div_add_mod (w22_apery S i) S.multiplicity
  have hx := Nat.div_add_mod x S.multiplicity
  have hr := w22_apery_mod S i
  have hd : x / S.multiplicity - w22_apery S i / S.multiplicity +
      w22_apery S i / S.multiplicity = x / S.multiplicity := by omega
  have he : x = w22_apery S i +
      (x / S.multiplicity - w22_apery S i / S.multiplicity) * S.multiplicity := by
    nlinarith
  rw [he]
  apply S.carrier.add_mem (w22_apery_mem S i)
  simpa using S.carrier.nsmul_mem S.multiplicity_mem
    (x / S.multiplicity - w22_apery S i / S.multiplicity)

theorem w22_frobenius_not_mem (S : NumericalSemigroup) :
    S.conductor - 1 ∉ S.carrier := by
  intro hmem
  have hc := S.conductor_pos
  have hthreshold : S.IsConductor (S.conductor - 1) := by
    intro x hx
    by_cases he : x = S.conductor - 1
    · simpa [he] using hmem
    · exact S.conductor_spec x (by omega)
  have hle := S.conductor_le hthreshold
  omega

noncomputable def w22_aperyMax (S : NumericalSemigroup) : ℕ :=
  Finset.univ.sup (w22_apery S)

theorem w22_aperyMax_lt (S : NumericalSemigroup) :
    w22_aperyMax S < S.conductor + S.multiplicity := by
  unfold w22_aperyMax
  apply (Finset.sup_lt_iff (show (0 : ℕ) < S.conductor + S.multiplicity from
    by have := S.conductor_pos; omega)).mpr
  intro i _
  exact w22_apery_lt S i

theorem w22_aperyMax_eq (S : NumericalSemigroup) :
    w22_aperyMax S = S.conductor + S.multiplicity - 1 := by
  let f := S.conductor - 1
  let i : Fin S.multiplicity := ⟨f % S.multiplicity, Nat.mod_lt _ S.multiplicity_pos⟩
  have hr : w22_apery S i % S.multiplicity = f % S.multiplicity := w22_apery_mod S i
  have hgt : f < w22_apery S i := by
    by_contra h
    have hmem := w22_mem_of_apery_le S i rfl (by omega)
    exact w22_frobenius_not_mem S hmem
  have hf := Nat.div_add_mod f S.multiplicity
  have hw := Nat.div_add_mod (w22_apery S i) S.multiplicity
  have hq : f / S.multiplicity < w22_apery S i / S.multiplicity := by
    have hm := S.multiplicity_pos
    nlinarith
  have hstep : f + S.multiplicity ≤ w22_apery S i := by
    have hm := S.multiplicity_pos
    nlinarith
  have hmax : w22_apery S i ≤ w22_aperyMax S :=
    Finset.le_sup (f := w22_apery S) (Finset.mem_univ i)
  have hlt := w22_aperyMax_lt S
  have hc := S.conductor_pos
  dsimp [f] at hstep
  omega

theorem w22_conductor_from_apery (S : NumericalSemigroup) :
    S.conductor = w22_aperyMax S - S.multiplicity + 1 := by
  rw [w22_aperyMax_eq]
  have hc := S.conductor_pos
  omega


/-- A8: residue-wise arithmetic progressions, with a finite counting domain. -/
theorem w22_apery_decomposition (S : NumericalSemigroup) (i : Fin S.multiplicity) {x : ℕ}
    (hx : x ∈ S.carrier) (hi : x % S.multiplicity = i.val) :
    ∃ k : ℕ, k ≤ x ∧ x = w22_apery S i + k * S.multiplicity := by
  have hle := w22_apery_min S i hx hi
  have hdiv := Nat.div_le_div_right (c := S.multiplicity) hle
  have hw := Nat.div_add_mod (w22_apery S i) S.multiplicity
  have hxx := Nat.div_add_mod x S.multiplicity
  have hr := w22_apery_mod S i
  let k := x / S.multiplicity - w22_apery S i / S.multiplicity
  have hd : k + w22_apery S i / S.multiplicity = x / S.multiplicity := by
    dsimp [k]
    omega
  have he : x = w22_apery S i + k * S.multiplicity := by nlinarith
  refine ⟨k, ?_, he⟩
  have hm := S.multiplicity_pos
  nlinarith

noncomputable def w22_aperyLeftCount (S : NumericalSemigroup) (i : Fin S.multiplicity) : ℕ :=
  ((Finset.range S.conductor).filter
    (fun k => w22_apery S i + k * S.multiplicity < S.conductor)).card

theorem w22_aperyLeftCount_eq_fiber (S : NumericalSemigroup) (i : Fin S.multiplicity) :
    w22_aperyLeftCount S i =
      (S.leftElements.filter (fun x => x % S.multiplicity = i.val)).card := by
  classical
  unfold w22_aperyLeftCount
  apply Finset.card_bij (fun k _ => w22_apery S i + k * S.multiplicity)
  · intro k hk
    have hlt := (Finset.mem_filter.mp hk).2
    refine Finset.mem_filter.mpr ⟨(S.mem_leftElements _).mpr ⟨hlt, ?_⟩, ?_⟩
    · apply S.carrier.add_mem (w22_apery_mem S i)
      simpa using S.carrier.nsmul_mem S.multiplicity_mem k
    · simp [Nat.add_mod, w22_apery_mod, Nat.mod_eq_of_lt i.isLt]
  · intro a ha b hb hab
    have hm := S.multiplicity_pos
    nlinarith
  · intro x hx
    obtain ⟨hxL, hi⟩ := Finset.mem_filter.mp hx
    obtain ⟨hlt, hxS⟩ := (S.mem_leftElements x).mp hxL
    obtain ⟨k, hk, he⟩ := w22_apery_decomposition S i hxS hi
    refine ⟨k, Finset.mem_filter.mpr ⟨Finset.mem_range.mpr (by omega), ?_⟩, he.symm⟩
    simpa only [← he] using hlt

theorem w22_leftCount_apery_sum (S : NumericalSemigroup) :
    S.leftCount = ∑ i : Fin S.multiplicity, w22_aperyLeftCount S i := by
  classical
  let residue := fun x : ℕ => (⟨x % S.multiplicity, Nat.mod_lt x S.multiplicity_pos⟩ : Fin S.multiplicity)
  have hmap : Set.MapsTo residue (S.leftElements : Set ℕ)
      (↑(Finset.univ : Finset (Fin S.multiplicity))) := by
    intro x hx
    exact Finset.mem_univ _
  have hcard := Finset.card_eq_sum_card_fiberwise hmap
  unfold NumericalSemigroup.leftCount
  rw [hcard]
  apply Finset.sum_congr rfl
  intro i hi
  rw [w22_aperyLeftCount_eq_fiber]
  congr 1


noncomputable def w23_q (S : NumericalSemigroup) : ℕ :=
  (S.conductor - 1) / S.multiplicity + 1

noncomputable def w23_rho (S : NumericalSemigroup) : ℕ :=
  w23_q S * S.multiplicity - S.conductor

lemma w23_q_bounds (S : NumericalSemigroup) :
    (w23_q S - 1) * S.multiplicity < S.conductor ∧
    S.conductor ≤ w23_q S * S.multiplicity := by