"""Van Eck's sequence: zero/novelty accounting and a deep census.

Evidence produced by this instrument is exact integer computation.  The
identity checked here is also immediate from the recurrence: apart from the
initial a(0)=0, a zero occurs exactly one step after a first occurrence.
"""

from array import array
from argparse import ArgumentParser
from math import log, sqrt


def census(size: int, checkpoints: list[int]) -> list[tuple[int, int, int, int]]:
    if size < 1:
        raise ValueError("size must be positive")

    # Every term is at most its index, so a dense 32-bit last-seen table is
    # sufficient for the ranges used here.
    last = array("i", [-1]) * (size + 1)
    value = 0
    zeros = 1
    lagged_distinct = 0  # D(N-1), with N=1 initially
    last_zero = 0
    max_zero_gap = 0
    wanted = set(checkpoints)
    rows = []

    if 1 in wanted:
        rows.append((1, zeros, lagged_distinct, max_zero_gap))

    for i in range(1, size):
        # Extend the lagged prefix through a(i-1).  Its first occurrences
        # are in exact bijection with subsequent zeros.
        if last[value] == -1:
            lagged_distinct += 1
        previous = last[value]
        last[value] = i - 1
        value = 0 if previous == -1 else (i - 1) - previous
        if value == 0:
            zeros += 1
            gap = i - last_zero
            if gap > max_zero_gap:
                max_zero_gap = gap
            last_zero = i

        terms = i + 1
        assert zeros == 1 + lagged_distinct
        if terms in wanted:
            rows.append((terms, zeros, lagged_distinct, max_zero_gap))

    return rows


def main() -> None:
    parser = ArgumentParser()
    parser.add_argument("--terms", type=int, default=20_000_000)
    args = parser.parse_args()
    checkpoints = [n for n in (100_000, 500_000, 1_000_000, 2_000_000,
                                5_000_000, 10_000_000, 20_000_000,
                                50_000_000) if n <= args.terms]

    print("PROVED by recurrence; assertion-checked at every term through",
          f"{args.terms:,}", ": Z(N) = 1 + D(N-1)")
    print("terms | zeros | D(N-1) | zero share | share*sqrt(ln N) | max zero gap")
    for terms, zeros, lagged_distinct, gap in census(args.terms, checkpoints):
        share = zeros / terms
        print(f"{terms:>10,} | {zeros:>8,} | {lagged_distinct:>8,} |"
              f" {share:>10.7f} | {share * sqrt(log(terms)):>16.7f} |"
              f" {gap:>12,}")


if __name__ == "__main__":
    main()