the assay office / record
No Thirty-Second Row
Written 2026-09-06. Claims re-read against their sources on 2026-10-01: 217 checked, 210 confirmed, 4 wrong, 0 unverifiable, 3 true when written and overtaken since (dated, not corrected). By the assay line (research/assay-line/tier-a-1001/), Codex fixer directed by claude-assaying-codex-0929; source record by Codex, checked by Codex.
This was the directed 2026-10-01 triage pass for no-thirty-second-row: the fixer re-read the evidence for all seven items in research/assay-line/tier-a-1001/no-thirty-second-row/triage.json and retained the 210 CONFIRMED claims already re-read by the Codex source checker in N2-codex.md. Notes prefixed "N2 check" describe that earlier checker's evidence and runs, not new runs by this fixer. The two MINOR claims count toward wrong; their fixes have no page correction lines. This record covers the directed work list and those confirmations, not a fresh disposition of the remaining OBSERVED and UNVERIFIABLE entries in the pilot report.
Claims
- WRONG X1: On every five points the signs obey the three-term Grassmann-Plücker relations, and a table obeying them all is a rank-3 chirotope.
https://refubium.fu-berlin.de/bitstream/handle/fub188/42643/Dissertation_Bergold.pdf?sequence=3 : Re-read Bergold, Definition 2.2.15 and Theorem 2.2.16 (p. 19), in the saved primary text: the three-term replacement there assumes a uniform alternating map. Re-ran the 15-element alternating counterexample with only 012 and 345 positive: all 15015 five-point/pivot relations pass, but all three basis-exchange candidates vanish. research/orchard-15/chiro/chirosat.py:8-34 supplies matroid support via the PTS. The page now states that condition; this finding does not invalidate the SAT certificate. - STALE X2: The drat-trim-checked proofs total 10.6 GB; the 5393 sub-case proofs came to 314 GB in all (at most 75 MB each) and were not kept.
git show 9b112ed892:research/orchard-15/chiro/AUDIT-15-32.md; git show 9b112ed892:research/orchard-15/chiro/results/depth2-c3-summary.txt : Re-read the 2026-09-05 ledger and the cube-3 update dated 2026-09-06 06:01Z in research/orchard-15/chiro/AUDIT-15-32.md. The six earlier displayed sizes sum to 10583353777 bytes; adding the verified 8980523963-byte proof gives 19563877740 bytes, rounded to 19.6 GB. The retained depth2-c3-summary.txt gives 5393 children and 314327464929 bytes. The caption now names the displayed subtotal and one Updated line dates the change shared by X2, X6 and X7. - MINOR X3: As a control, the census of the (13, 23) solutions was re-run without any symmetry breaking: it found exactly the 184,320 labelled models that one class with four leave-free points and a trivial automorphism group predicts, every one of them that class.
git show 9b112ed892:research/orchard-15/realize/nolex/RESULT.md : Re-read research/orchard-15/realize/nolex/RESULT.md: the canonical row and sign anchors remained while lex-leader constraints were removed. The 184320 count is supported. The page now says without lex-leader symmetry breaking. MINOR, recorded here without a page correction line. - MINOR X4: To reproduce cube k: python3 research/orchard-15/chiro/exist.py 15 32 --backend cadical --cubes --cube-index k --drat-trim <path>, twenty-six minutes for cube 0 on four cores and about two hours for cube 3, then compare the CNF hash with the ledger.
git show 9b112ed892:research/orchard-15/chiro/AUDIT-15-32.md; reader-check.txt : Re-read research/orchard-15/chiro/AUDIT-15-32.md: cube 0 cadical took 26 minutes on the cloud worker; cube 3 cadical took 18004 seconds to solve, and its successful drat-trim recheck took 45331.519 seconds. The 7198-second solve used kissat. exist.py imports pysat.card and pysat.solvers and launches a separate cadical executable; the saved reader-check.txt records ModuleNotFoundError for pysat. The page now names Python 3.11 or 3.12, python-sat 1.9.dev15, cadical on the executable path and drat-trim, with solve and check times separated. MINOR, recorded here without a page correction line. - WRONG X5: The sequences behind this page are published as open data and code: the b-files, the engine that produced them and the verifier that checks it, together with a per-term account of what has been recomputed and what has not.
https://raw.githubusercontent.com/artwasteland/Maths/main/orchard-15/README.md; https://api.github.com/repos/artwasteland/Maths/git/trees/main?recursive=1 : Re-fetched the public orchard README and full GitHub tree on 2026-10-01. Tree ba1c76fd4abbd776315621ab85b7381e05352985 has truncated=false and 268 orchard paths, including exist.py and control-verdicts.jsonl, with no orchard numerical b-file. The same filename search finds labeled-chip-firing/oversight/oeis/labeled-chip-firing/b282901.txt. The saved Zenodo listing and README agree. The director corrected scripts/link-maths-repo.mjs for this page and regenerated only this footer. The replacement names the code, verification records and exact-coordinate data actually present. A dated Corrected line records the earlier false promise. - STALE X6: There the 200-terabyte refutation of a colouring; here a 10.6-gigabyte refutation of a planting, cut into four cubes and checked by the same kind of independent checker, with cake_lpr's machine-verified yes on top.
https://arxiv.org/abs/1605.00723; git show 9b112ed892:research/orchard-15/chiro/AUDIT-15-32.md : Re-read the Heule, Kullmann and Marek primary abstract at arXiv:1605.00723, which describes a proof of almost 200 terabytes. The orchard quantity is the same stale displayed subtotal as X2. The related-page note now says 19.6 gigabytes of proofs in the displayed ledger. The single Updated line dates the earlier six-size subtotal to 2026-09-05 and the added proof verification to 2026-09-06. - STALE X7: The drat-trim-checked proofs total 10.6 GB
research/orchard-15/chiro/AUDIT-15-32.md; public/strata/no-thirty-second-row/index.html : Duplicate source-record entry for the caption subtotal in X2. Independently summed all seven displayed proof sizes to 19563877740 bytes. The layer verifier no longer excludes the 8980523963-byte cadical proof. One page Updated line covers X2, X6 and X7, mirrored once in the markdown body. - CONFIRMED The best planting known has thirty-one rows, and since 1974 the open question has been whether a thirty-second is possible.
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg : N2 check: entry 1 (intro-best-history): Table I, p. 399, row "15 31 32 31 35" puts the real lower and upper bounds at 31 and 32. Visually read the scan; the image is readable despite the source tool saying NOT FOUND. OEIS still quotes "31 or 32". - CONFIRMED John Jackson's Rational Amusement for Winter Evenings (1821) asks for nine trees in ten rows of three
https://proofwiki.org/wiki/Orchard_Planting_Problem/Historical_Note; https://arxiv.org/pdf/1208.4714; https://books.google.com/books?id=0Qc3VEIxwCYC : N2 check: entry 4 (jackson): The historical transcription says "Your aid I want, nine trees to plant / In rows just half a score; / And let there be in each row three." Green and Tao p. 3 reproduces Jackson and identifies the 1821 book; the Google Books catalogue independently confirms author, title and 1821. - CONFIRMED Sylvester played with it in the 1860s
https://arxiv.org/pdf/1208.4714 : N2 check: entry 5 (sylvester): Green and Tao p. 3: "This was first formally posed by Sylvester [34] in 1868". The date falls in the stated decade. - CONFIRMED in 1974 Burr, Grünbaum and Sloane made it a function.
https://neilsloane.com/doc/ORCHARD/hp_scanDS_63519353959.jpg : N2 check: entry 6 (bgs-function): BGS p. 397 defines t(p) as "the maximal value of t possible in any (p, t)-arrangement." The first-page imprint is 1974. This supports their use of a function, without establishing historical priority for that notation. - CONFIRMED Write t3(n) for the largest number of lines through exactly three of n points in the plane.
https://oeis.org/A003035/internal : N2 check: entry 7 (definition): OEIS title: "Maximal number of 3-tree rows in n-tree orchard problem." BGS p. 397 explicitly requires exactly three points on a line. - CONFIRMED Points on a cubic curve give a planting with ⌊n(n−3)/6⌋ + 1 rows
https://arxiv.org/pdf/1208.4714 : N2 check: entry 8 (cubic-lower): Green and Tao Proposition 2.6, pp. 18-19, gives the cyclic-subgroup construction and the formula floor(n(n-3)/6)+1. The cyclic group was also counted directly for the displayed n values. - CONFIRMED three points of a cubic are collinear exactly when they sum to zero in the curve's group
https://arxiv.org/pdf/1208.4714 : N2 check: entry 9 (cubic-group): Green and Tao p. 15: "P ⊕ Q ⊕ R = O if and only if P, Q, R are collinear." This is the group law on the nonsingular cubic used in the construction. - CONFIRMED a cyclic subgroup of order n has that many zero-sum triples.
https://arxiv.org/pdf/1208.4714 : N2 check: entry 10 (cyclic-triples): Green and Tao Proposition 2.6, pp. 18-19, gives the cyclic-subgroup construction and the formula floor(n(n-3)/6)+1. The cyclic group was also counted directly for the displayed n values. - CONFIRMED Four small cases beat the formula (n = 7, 11, 16 and 19)
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg : N2 check: entry 11 (sporadics): BGS Table I has lower bounds (7,6), (11,16), (16,37), (19,52). The corresponding cubic values are 5,15,35,51, and the Kelly-Moser ceilings are 6,16,37,54. All arithmetic was independently recomputed. - CONFIRMED Green and Tao proved in 2013 that nothing else ever does, once n is enormous.
https://arxiv.org/pdf/1208.4714 : N2 check: entry 12 (green-tao): Green and Tao Theorem 1.3 says "Suppose that n ⩾ n0 for some sufficiently large absolute constant n0" and gives the stated maximum. The arXiv version is dated 28 Mar 2013; its publication is Discrete Comput. Geom. 50 (2013). - CONFIRMED In between, the values had to be found one at a time.
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg : N2 check: entry 13 (between): BGS Table I marks 1,1,2,4,6,7,10,12,16,19 as known exact values for p=3 through 12. Theorems 5 and following supply the small upper bounds; no assertion that every earlier example was first discovered by these authors is needed. - CONFIRMED Burr, Grünbaum and Sloane settled every n up to 12.
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg : N2 check: entry 14 (through-twelve): BGS Table I marks 1,1,2,4,6,7,10,12,16,19 as known exact values for p=3 through 12. Theorems 5 and following supply the small upper bounds; no assertion that every earlier example was first discovered by these authors is needed. - CONFIRMED At 15 they proved 31 ≤ t3(15) ≤ 32
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg : N2 check: entry 17 (fifteen-bounds): Table I, p. 399, row "15 31 32 31 35" puts the real lower and upper bounds at 31 and 32. Visually read the scan; the image is readable despite the source tool saying NOT FOUND. OEIS still quotes "31 or 32". - CONFIRMED Sloane's comment on A003035 reads "31 or 32"
https://oeis.org/A003035/internal : N2 check: entry 18 (sloane-quote): OEIS retains Sloane's dated comment "It is known that a(15) is 31 or 32, a(16)=37 and a(17) is 40, 41 or 42." The 1974 lower/upper bounds also appear in BGS Table I. - CONFIRMED Friedman's table says the same
https://erich-friedman.github.io/packing/trees/ : N2 check: entry 19 (friedman-table): Friedman's k=3 row contains "26-27", "31-32", "37" at n=14,15,16 respectively. The n=15 attribution is exact. - CONFIRMED Here is the planting with thirty-one rows.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 21 (planting-shown): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED Every tree is a real point with exact algebraic coordinates
git show 9b112ed892:research/orchard-15/realize/REPORT.md : N2 check: entry 22 (exact-points): The realization report gives "alpha^8 - 28 alpha^6 + 134 alpha^4 - 92 alpha^2 + 1" and interval "(47/10,24/5)". The pinned exact checker returned "all 455 determinants and all point pairs verified exactly". The page separately discloses its rounded rendering. - CONFIRMED the rows are recounted in your browser.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 23 (recount): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED The trees are numbered 0 to 14 and a row is any three whose numbers add to a multiple of 15
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 24 (row-rule): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED that is the cubic-curve construction of Burr, Grünbaum and Sloane
https://neilsloane.com/doc/ORCHARD/hp_scanDS_63519353959.jpg; https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg; https://oeis.org/A003035/internal : N2 check: entry 25 (row-attribution): The OEIS excerpt attributes its illustrated zero-sum variant to Ed Pegg, not to BGS. The underlying cubic construction is nevertheless supported by BGS pp. 397 and 399, Theorem 1, and by Green and Tao Proposition 2.6. Correct the source selection, not the mathematical attribution. - CONFIRMED it gives 31 rows, with three trees standing on seven rows and twelve on six.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 26 (row-incidences): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED Drag any tree and watch its rows die: a row is an exact coincidence, and there is no slack in it.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 27 (screen-caption-0): The handlers recompute after movement and reset with "pts = EXACT.map(function (p) { return [p[0], p[1]]; });". The pinned verifier confirms moving tree 3 breaks its six rows and preserves the other 25. Exactness describes the underlying certificate; the displayed coordinates and tolerance are explicitly approximate. - CONFIRMED Replant restores the exact planting.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 28 (screen-caption-1): The handlers recompute after movement and reset with "pts = EXACT.map(function (p) { return [p[0], p[1]]; });". The pinned verifier confirms moving tree 3 breaks its six rows and preserves the other 25. Exactness describes the underlying certificate; the displayed coordinates and tolerance are explicitly approximate. - CONFIRMED The count in the browser uses floating-point coordinates and a tolerance; the exact check, 455 determinants in the number field Q(α) with α8 − 28α6 + 134α4 − 92α2 + 1 = 0, is in the repository.
git show 9b112ed892:research/orchard-15/realize/REPORT.md : N2 check: entry 29 (screen-caption-2): The realization report gives "alpha^8 - 28 alpha^6 + 134 alpha^4 - 92 alpha^2 + 1" and interval "(47/10,24/5)". The pinned exact checker returned "all 455 determinants and all point pairs verified exactly". The page separately discloses its rounded rendering. - CONFIRMED Showing that is not a matter of trying plantings, which are uncountable, but of two reductions and one very large search.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 31 (body-5-1): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED Fifteen trees make 105 pairs.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 32 (pair-budget-0): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED A row of three uses three pairs, so thirty-two rows use 96 and leave 9.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 33 (pair-budget-1): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED Now a theorem from 1958 enters.
https://www.cambridge.org/core/services/aop-cambridge-core/content/view/C2BBECD090CBA344F80C4B28AA45F2E3/S0008414X00045302a.pdf/div-class-title-on-the-number-of-ordinary-lines-determined-by-span-class-italic-n-span-points-div.pdf : N2 check: entry 34 (pair-budget-2): Kelly and Moser, Theorem 3.6, gives m >= 3n/7. Figures 3.1 and 3.2 attain m=3,4 for n=7,8. The paper is Canad. J. Math. 10 (1958), 210-219. - CONFIRMED Kelly and Moser proved that among n points not all on one line, at least 3n/7 lines pass through exactly two of them (Sylvester's "ordinary lines"; the bound is tight at n = 7).
https://www.cambridge.org/core/services/aop-cambridge-core/content/view/C2BBECD090CBA344F80C4B28AA45F2E3/S0008414X00045302a.pdf/div-class-title-on-the-number-of-ordinary-lines-determined-by-span-class-italic-n-span-points-div.pdf : N2 check: entry 35 (pair-budget-3): Kelly and Moser, Theorem 3.6, gives m >= 3n/7. Figures 3.1 and 3.2 attain m=3,4 for n=7,8. The paper is Canad. J. Math. 10 (1958), 210-219. - CONFIRMED For fifteen points that is at least 7 ordinary lines, and each of them is one of the leftover pairs.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 36 (pair-budget-4): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED So the 9 leftover pairs must contain 7 ordinary lines, which already rules out a row of four (it would eat six pairs of its own and leave three).
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 37 (pair-budget-5): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED Every leftover pair is an ordinary line, and the thirty-two rows form a partial Steiner triple system on 15 points whose uncovered graph has nine edges with every degree even.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 38 (pair-budget-6): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED That is a finite combinatorial object, and a small one.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 39 (pair-budget-7): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED Sylvester's "ordinary lines"
https://www.cambridge.org/core/services/aop-cambridge-core/content/view/C2BBECD090CBA344F80C4B28AA45F2E3/S0008414X00045302a.pdf/div-class-title-on-the-number-of-ordinary-lines-determined-by-span-class-italic-n-span-points-div.pdf : N2 check: entry 40 (ordinary-quote): The paper is titled "ON THE NUMBER OF ORDINARY LINES DETERMINED BY n POINTS" by L. M. Kelly and W. O. J. Moser, 1958. Its introduction connects the ordinary-line problem to Sylvester. This is terminology, not a claimed verbatim sentence by Sylvester. - CONFIRMED Run the same arithmetic for any n.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 41 (body-7-0): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED The pair budget alone gives an upper bound; the cubic construction gives a lower bound; the orchard problem is the gap between them.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 42 (body-7-1): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED pairs of trees 105 n(n−1)/2
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 43 (calculator-label-8): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED ordinary lines forced 7 ⌈3n/7⌉, Kelly-Moser
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 44 (calculator-label-9): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED rows the budget allows 32 ⌊(pairs − ordinary)/3⌋
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 45 (calculator-label-10): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED rows the cubic gives 31 ⌊n(n−3)/6⌋ + 1
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 46 (calculator-label-11): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED At n = 7, 11 and 16 the budget is spent exactly: a planting achieves the ceiling, and those are three of the four values that beat the cubic formula.
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg : N2 check: entry 47 (body-12-0): BGS Table I has lower bounds (7,6), (11,16), (16,37), (19,52). The corresponding cubic values are 5,15,35,51, and the Kelly-Moser ceilings are 6,16,37,54. All arithmetic was independently recomputed. - CONFIRMED At n = 19 a planting with 52 rows beats the formula's 51 without reaching the ceiling of 54.
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg : N2 check: entry 48 (body-12-1): BGS Table I has lower bounds (7,6), (11,16), (16,37), (19,52). The corresponding cubic values are 5,15,35,51, and the Kelly-Moser ceilings are 6,16,37,54. All arithmetic was independently recomputed. - CONFIRMED Everywhere else the gap between formula and ceiling had to be closed by hand, or has not been.
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg : N2 check: entry 49 (body-12-2): BGS Table I has lower bounds (7,6), (11,16), (16,37), (19,52). The corresponding cubic values are 5,15,35,51, and the Kelly-Moser ceilings are 6,16,37,54. All arithmetic was independently recomputed. The page itself identifies n=9 as the case where the elementary bounds already agree; this general sentence describes the remaining gaps. - CONFIRMED The second reduction turns geometry into a table of signs.
git show 9b112ed892:research/orchard-15/chiro/REPORT-EXIST.md : N2 check: entry 50 (signs-0): REPORT-EXIST lists sign variables, alternation, tie clauses, pair disjointness and a fixed matroid support. The reduction from a point set to determinant signs and the finite Boolean encoding are described explicitly. - CONFIRMED Any planting of fifteen points determines, for each of the 455 triples, whether the three points turn anticlockwise, clockwise, or lie on a line: a +, a − or a 0.
git show 9b112ed892:research/orchard-15/chiro/chirosat.py : N2 check: entry 51 (signs-1): chirosat.py states "Neither variable means zero" and obtains ordered signs using "the parity of the sorting permutation". The 15-point triple count is 15*14*13/6=455; determinant zero means collinearity. - CONFIRMED The table is not arbitrary.
git show 9b112ed892:research/orchard-15/chiro/REPORT-EXIST.md : N2 check: entry 52 (signs-2): REPORT-EXIST lists sign variables, alternation, tie clauses, pair disjointness and a fixed matroid support. The reduction from a point set to determinant signs and the finite Boolean encoding are described explicitly. - CONFIRMED Not every chirotope comes from points, but every one comes from a planting of the projective plane by pseudolines (Folkman and Lawrence, 1978), curves that behave like lines in every combinatorial respect.
https://www.sciencedirect.com/science/article/pii/0095895678900394; https://www.math.ucdavis.edu/~deloera/MISC/LA-BIBLIO/trunk/BlandLasVergnas.pdf (PDF page 16 onward) : N2 check: entry 54 (signs-4): The publisher abstract says a "topological representation theorem for oriented matroids is proven". The primary paper, pp. 199-236, was independently opened in a scanned university-hosted copy after the publisher returned HTTP 403. Its first page confirms Folkman, Lawrence, title, journal volume 25 and 1978; rank three gives the pseudoline representation. - CONFIRMED Rows are the zeros of the table.
git show 9b112ed892:research/orchard-15/chiro/chirosat.py : N2 check: entry 55 (signs-5): chirosat.py states "Neither variable means zero" and obtains ordered signs using "the parity of the sorting permutation". The 15-point triple count is 15*14*13/6=455; determinant zero means collinearity. - CONFIRMED Is there a table of 455 signs, satisfying every Grassmann-Plücker relation, whose zeros are exactly a 32-block partial triple system with a 9-edge even leave?
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 56 (boolean-1): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED If not, then no pseudoline planting has 32 rows, and since straight lines are pseudolines, no real planting does either.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 57 (boolean-2): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED Kelly-Moser holds for pseudolines too (Kelly and Rottenberg, 1972), so the pair budget survives the translation.
https://msp.org/pjm/1972/40-3/pjm-v40-n3-p10-p.pdf : N2 check: entry 58 (boolean-3): Kelly and Rottenberg p. 617 says their reasoning proves "the analogous result for pseudoline arrangements". Theorem 3.6 supplies the 3n/7 bound. The real projective plane and non-pencil hypotheses are the ones used here. - CONFIRMED The question is finite.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 59 (boolean-4): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED Some tree stands on no ordinary line at all (there are at least six such), so call it tree 0 and fix its seven rows in a canonical form: {0, 1, 2}, {0, 3, 4}, and so on to {0, 13, 14}.
git show 9b112ed892:research/orchard-15/chiro/REPORT-EXIST.md : N2 check: entry 63 (cubes-0): Lemma 5 gives "6 for (15,32)" minimum-leave points. Independently, nine even-degree leave edges touch at most nine of fifteen vertices, leaving at least six of degree zero and hence seven triples through each. - CONFIRMED Tree 1 then sits on the row {0, 1, 2}, and its remaining six rows pair the twelve trees 3 to 14 into six pairs that avoid tree 0's pairs: 6040 ways.
git show 9b112ed892:research/orchard-15/chiro/independent/README.md : N2 check: entry 64 (cubes-1): The independent orbit record gives "6,040 configurations" and "exactly 4 orbits of sizes 120, 1440, 640, 3840". Recreated count-by-cycle-type.py printed "total 6040 {(4, 4, 4): 120, (8, 4): 1440, (6, 6): 640, (12,): 3840}". Also 2^6*6!=46080. - CONFIRMED The symmetries that keep tree 0's rows and tree 1 in place, permuting those six pairs and swapping the two trees within any of them, form a group of order 46,080, and under it the 6040 ways fall into four classes, of sizes 120, 1440, 640 and 3840.
git show 9b112ed892:research/orchard-15/chiro/independent/README.md : N2 check: entry 65 (cubes-2): The independent orbit record gives "6,040 configurations" and "exactly 4 orbits of sizes 120, 1440, 640, 3840". Recreated count-by-cycle-type.py printed "total 6040 {(4, 4, 4): 120, (8, 4): 1440, (6, 6): 640, (12,): 3840}". Also 2^6*6!=46080. - CONFIRMED an independent program that replays the trace against the original CNF and accepts only when the empty clause is reached
https://raw.githubusercontent.com/marijnheule/drat-trim/master/README.md : N2 check: entry 73 (drat-function): The drat-trim README says "DRAT-trim validates that the proof is a certificate of unsatisfiability of the formula." Its description requires derivation of the empty clause. The checker consumes the original CNF and proof independently of the solver. - CONFIRMED a checker whose own correctness is a machine-verified theorem in HOL4
https://cakeml.org/tacas21.pdf : N2 check: entry 74 (cake-hol4): The cake_lpr paper, Appendix A, says "The correctness theorem for cake_lpr verified in HOL4 is shown in Fig. 6." The paper includes the binary-code extraction guarantee and LRAT compatibility. - CONFIRMED That the counting argument is right (it is a page).
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 88 (sceptic-1): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED At thirteen trees the pair budget allows 24 rows and the cubic gives 22.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 95 (below-1): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED a question Kühne, Szemberg and Tutaj-Gasińska left open in 2024
https://arxiv.org/pdf/2401.14766 : N2 check: entry 102 (kuhne-question): Kühne, Szemberg and Tutaj-Gasińska, p. 2: "it remains open whether there exists arrangements with" followed by "13 lines and 24 triple points". The page correctly limits the new answer to the reals and uses projective duality. - CONFIRMED they asked about arbitrary fields
https://arxiv.org/pdf/2401.14766 : N2 check: entry 103 (kuhne-arbitrary): The paper explicitly studies the question "with no restriction on the underlying field." Its complex and positive-characteristic examples cannot contradict a real-plane result. - CONFIRMED Not done: the general problem, which Green and Tao settled only for astronomically large n; sixteen, seventeen and beyond still have a gap between formula and budget, except where a sporadic planting closes it.
https://arxiv.org/pdf/1208.4714 : N2 check: entry 106 (limits-2): Green and Tao p. 3 says a bound could be computed but "it would be of double exponential type" and they do not compute a numerical n0. This supports the page's qualification about how large. - CONFIRMED S. A. Burr, B. Grünbaum and N. J. A. Sloane, The orchard problem, Geometriae Dedicata 2 (1974) 397-424: the function, the cubic construction, the pair-counting Theorem 4 and the exact values through n = 12.
https://neilsloane.com/doc/ORCHARD/orchard.html; https://neilsloane.com/doc/ORCHARD/scan_635195735_1.jpg : N2 check: entry 110 (citation-0): The author-hosted scan identifies S. A. Burr, B. Grünbaum, N. J. A. Sloane, "Geometriae Dedicata, 2 (1974), 397-424." Theorem 1 gives the cubic lower bound; Table I gives exact values through 12; Theorem 4 on p. 409 is the pair-counting bound. - CONFIRMED L. M. Kelly and W. O. J. Moser, On the number of ordinary lines determined by n points, Canad. J. Math. 10 (1958).
https://www.cambridge.org/core/services/aop-cambridge-core/content/view/C2BBECD090CBA344F80C4B28AA45F2E3/S0008414X00045302a.pdf/div-class-title-on-the-number-of-ordinary-lines-determined-by-span-class-italic-n-span-points-div.pdf : N2 check: entry 111 (citation-1): The paper is titled "ON THE NUMBER OF ORDINARY LINES DETERMINED BY n POINTS" by L. M. Kelly and W. O. J. Moser, 1958. Its introduction connects the ordinary-line problem to Sylvester. This is terminology, not a claimed verbatim sentence by Sylvester. - CONFIRMED L. M. Kelly and R. Rottenberg (1972) for the pseudoline version.
https://msp.org/pjm/1972/40-3/pjm-v40-n3-p10-p.pdf : N2 check: entry 112 (citation-2): The primary paper is headed "SIMPLE POINTS IN PSEUDOLINE ARRANGEMENTS" and names L. M. Kelly and R. Rottenberg. It is Pacific J. Math. 40(3), 1972. Theorem 3.6 gives the claimed extension. - CONFIRMED J. Folkman and J. Lawrence, Oriented matroids, J. Combin. Theory B 25 (1978).
https://www.sciencedirect.com/science/article/pii/0095895678900394; https://www.math.ucdavis.edu/~deloera/MISC/LA-BIBLIO/trunk/BlandLasVergnas.pdf (PDF page 16 onward) : N2 check: entry 113 (citation-3): The publisher abstract says a "topological representation theorem for oriented matroids is proven". The primary paper, pp. 199-236, was independently opened in a scanned university-hosted copy after the publisher returned HTTP 403. Its first page confirms Folkman, Lawrence, title, journal volume 25 and 1978; rank three gives the pseudoline representation. - CONFIRMED B. Green and T. Tao, On sets defining few ordinary lines, Discrete Comput. Geom. 50 (2013).
https://arxiv.org/pdf/1208.4714 : N2 check: entry 114 (citation-4): Green and Tao Theorem 1.3 says "Suppose that n ⩾ n0 for some sufficiently large absolute constant n0" and gives the stated maximum. The arXiv version is dated 28 Mar 2013; its publication is Discrete Comput. Geom. 50 (2013). - CONFIRMED L. Kühne, T. Szemberg and H. Tutaj-Gasińska, arXiv:2401.14766 (2024), for the (13, 24) question.
https://arxiv.org/pdf/2401.14766 : N2 check: entry 115 (citation-5): The arXiv paper is headed "LINE ARRANGEMENTS WITH MANY TRIPLE POINTS" and names Lukas Kühne, Tomasz Szemberg and Halszka Tutaj-Gasińska. It is arXiv:2401.14766, 2024; the open question is on p. 2. - CONFIRMED The catalogue entry is OEIS A003035.
https://oeis.org/A003035/internal : N2 check: entry 116 (citation-6): OEIS title: "Maximal number of 3-tree rows in n-tree orchard problem." BGS p. 397 explicitly requires exactly three points on a line. - CONFIRMED research/orchard-15/RESULT-15-32.md (the theorem and the reduction)
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 117 (repo-reference-result): The recorded theorem says "No configuration of 15 points in the real plane has 32 lines through exactly three points." The ledger records four verified UNSAT cases and four cake_lpr acceptances. The CNF regeneration and exact lower-bound check were recreated here; the multi-hour SAT refutations were not rerun. - CONFIRMED research/orchard-15/chiro/exist.py (the CNF generator, with the chirotope axioms in its comments)
git show 9b112ed892:research/orchard-15/chiro/exist.py : N2 check: entry 118 (repo-reference-generator): The pinned file starts "Existence SAT for orchard partial Steiner triple systems" and spells out the sign variables, chirotope base, pair clauses, exact block count and symmetry constraints. It is the generator used by the successful four-CNF regeneration. - CONFIRMED research/orchard-15/chiro/cnfcheck.py (the audit of each cube file)
git show 9b112ed892:research/orchard-15/chiro/cnfcheck.py : N2 check: entry 119 (repo-reference-cnfchecker): The audit script states it checks the "header", "unit clauses" and "lex-leader clauses" against the intended cube. The recorded audit describes those checks, not a formal proof of the generator. - CONFIRMED research/orchard-15/chiro/REPORT-EXIST.md (the nine lemmas)
git show 9b112ed892:research/orchard-15/chiro/REPORT-EXIST.md : N2 check: entry 121 (repo-reference-cubeconstruction): Lemma 7 proves the orbit representatives cover all row-1 configurations. Lemma 8 restricts lex leaders to the subgroup fixing the selected rows. The four generated CNFs were recreated; this is the documented construction, not a claim that the Python generator is formally verified. - CONFIRMED research/orchard-15/realize/realize.py with its blind checker research/orchard-15/realize/check_realization.py (the stage that finds exact coordinates or proves there are none).
git show 9b112ed892:research/orchard-15/realize/realize.py : N2 check: entry 122 (repo-realizer): The realizer starts "Decide exact real realizability of contract PTS instances when certified." The separate checker reconstructs the certificate from the PTS. The Pegg certificate was accepted independently here. - CONFIRMED Checkers: drat-trim at commit 2e3b2dc0, run with its compiled time limit lifted so that a silent timeout cannot pass as a verdict, and cake_lpr.
git show 9b112ed892:research/orchard-15/chiro/AUDIT-15-32.md : N2 check: entry 124 (checker-version): The audit hazards section records "TIMEOUT 40000 s at 2e3b2dc0" and the repair to reject "TIMEOUT / NOT VERIFIED". The compiled limit is lifted by the documented run flag; the historical checker versions are in the ledger. - CONFIRMED The certificate is a chain, and the chain has links that are not formally verified: the counting reduction is a human proof (one page, refereed adversarially, not machine-checked), the CNF generator is audited but not proven correct, and drat-trim is a trusted program. cake_lpr removes the last of those for all four cubes.
git show 9b112ed892:research/orchard-15/chiro/AUDIT-15-32.md : N2 check: entry 126 (body-27-0): The audit records that the mathematics "was attacked by a five-referee panel on 2026-09-05 and held" and that the serious findings concerned the certificate protocol. This is a supported report of that review, not independent proof that a referee could never find a problem. - CONFIRMED The planting on screen is drawn from rounded coordinates after a projective squeeze and counted with a tolerance, so it demonstrates the 31 rows rather than certifying them; the exact certificate is the field-arithmetic check in research/orchard-15/realize/check_realization.py.
git show 9b112ed892:research/orchard-15/realize/REPORT.md; git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 127 (body-27-1): The record attached an LRAT-ledger excerpt to the rendering claim; the realization report, HTML and exact checker are the relevant sources. The realization report gives "alpha^8 - 28 alpha^6 + 134 alpha^4 - 92 alpha^2 + 1" and interval "(47/10,24/5)". The pinned exact checker returned "all 455 determinants and all point pairs verified exactly". The page separately discloses its rounded rendering. The handlers recompute after movement and reset with "pts = EXACT.map(function (p) { return [p[0], p[1]]; });". The pinned verifier confirms moving tree 3 breaks its six rows and preserves the other 25. Exactness describes the underlying certificate; the displayed coordinates and tolerance are explicitly approximate. - CONFIRMED Nothing is claimed for fields other than the reals except where the text says so.
git show 9b112ed892:research/orchard-15/realize/independent/README.md; git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 128 (body-27-2): The record attached only a checker docstring to the scope disclaimer; the independent algebra report and page supply the relevant evidence. The checker distinguishes real, no-realization and unknown. The independent realizer report separately states the all-fields result for (13,23); the page explicitly makes that exception, so the scope disclaimer is consistent. - CONFIRMED The certificate is a chain, and the chain has links that are not formally verified: the counting reduction is a human proof (one page, refereed adversarially, not machine-checked), the CNF generator is audited but not proven correct, and drat-trim is a trusted program.
git show 9b112ed892:research/orchard-15/chiro/AUDIT-15-32.md : N2 check: entry 129 (trust-chain): The audit records that the mathematics "was attacked by a five-referee panel on 2026-09-05 and held" and that the serious findings concerned the certificate protocol. This is a supported report of that review, not independent proof that a referee could never find a problem. - CONFIRMED This layer's check opens this page in a real browser and drives it.
git show 9b112ed892:research/no-thirty-second-row/verify-no-thirty-second-row.mjs : N2 check: entry 133 (browser-check): The pinned verifier imports Playwright and uses page.goto(), mouse movement and slider events on a local file. It also checks numbers independently. This run skipped Playwright because it is unavailable; that does not contradict the recorded earlier browser run. - CONFIRMED research/no-thirty-second-row/verify-no-thirty-second-row.mjs, research/orchard-15/chiro/cnf-audit/verify_driver.py
git show 9b112ed892:research/no-thirty-second-row/verify-no-thirty-second-row.mjs : N2 check: entry 136 (check-script-citation): Both named files exist at the pinned commit. The page verifier failure and skipped browser run are recorded below. The pinned verifier imports Playwright and uses page.goto(), mouse movement and slider events on a local file. It also checks numbers independently. This run skipped Playwright because it is unavailable; that does not contradict the recorded earlier browser run. - CONFIRMED Deposited, and citable by DOI: 10.5281/zenodo.22468969
https://zenodo.org/api/records/22468969 : N2 check: entry 138 (deposit-citation): The Zenodo API returns DOI "10.5281/zenodo.22468969", the orchard theorem title, publication date 2026-09-14 and an 8,814,056-byte orchard-15.zip. This is a published deposit. Crossref's 404 is not evidence against a Zenodo DOI. - CONFIRMED The orchard problem asks how many straight rows of exactly three trees you can plant with n trees.
https://oeis.org/A003035/internal : N2 check: entry 139 (frontmatter-dek-0): OEIS title: "Maximal number of 3-tree rows in n-tree orchard problem." BGS p. 397 explicitly requires exactly three points on a line. - CONFIRMED For fifteen trees the best planting known has 31 rows, and since Burr, Grünbaum and Sloane proved 31 or 32 in 1974 nobody has closed the gap: the OEIS entry still says 31 or 32.
https://oeis.org/A003035/internal : N2 check: entry 140 (frontmatter-dek-1): OEIS retains Sloane's dated comment "It is known that a(15) is 31 or 32, a(16)=37 and a(17) is 40, 41 or 42." The 1974 lower/upper bounds also appear in BGS Table I. - CONFIRMED Two reductions turn the question finite: a pair budget with the Kelly-Moser ordinary-line bound shows 32 rows would form a partial Steiner triple system with a nine-edge even leave, and the chirotope axioms turn any planting into a table of 455 signs obeying the Grassmann-Plücker relations.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 142 (frontmatter-dek-3): The reduction records "32 three-point lines cover 96 of the 105 point pairs" and "ceil(3*15/7) = 7". Independently: 105-96=9, a four-point line consumes six pairs, and 2r3+r2=14 forces even leave degree. The encoding applies these conditions to a finite 455-triple support. - CONFIRMED The 31-row planting is drawn live from exact algebraic coordinates: hover a tree to light its rows, drag one to watch them die, and run the pair budget for any n to see where the gap between the cubic formula and the counting ceiling still stands.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 145 (frontmatter-dek-6): The phrase "for any n" describes the formula; the actual slider is explicitly labelled with a 7-to-24 input range. The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED The orchard problem asks how many rows of exactly three trees can be planted with a given number of trees.
https://oeis.org/A003035/internal : N2 check: entry 147 (frontmatter-plain-0): OEIS title: "Maximal number of 3-tree rows in n-tree orchard problem." BGS p. 397 explicitly requires exactly three points on a line. - CONFIRMED For fifteen trees the answer has been 31 or 32 since 1974.
https://oeis.org/A003035/internal : N2 check: entry 148 (frontmatter-plain-1): OEIS retains Sloane's dated comment "It is known that a(15) is 31 or 32, a(16)=37 and a(17) is 40, 41 or 42." The 1974 lower/upper bounds also appear in BGS Table I. - CONFIRMED 15 trees · 31 rows · hover, drag, count
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 161 (orchard-label): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED Fifteen trees and the thirty-one straight rows through exactly three of them. Hover a tree to light its rows; drag a tree to break them.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 163 (orchard-accessible-description): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED rows of exactly three 31
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 164 (initial-rows-of-exactly-three): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED rows of four or more 0
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 165 (initial-rows-of-four-or-more): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED two-tree lines 12
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 166 (initial-two-tree-lines): The page code enumerates zero-sum triples with "(i + j + k) % 15 === 0" and computes collinearity from the screen coordinates. Recreated tally: 31 three-tree lines, 0 lines of four or more, 12 two-tree lines; all 31 triples agree with the independently enumerated set. - CONFIRMED Self-check failed: the rows counted on screen are not the 31 zero-sum triples. The coordinates or the tolerance are wrong; trust the repository, not this picture.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 167 (self-check-message): The render() self-check requires 31 triples, no four-point line, and every triple in rowKey. This run found precisely that set, so the diagnostic remains silent under the stated conditions. - CONFIRMED replanted: the exact planting, 31 rows
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 168 (replant-message): The handlers recompute after movement and reset with "pts = EXACT.map(function (p) { return [p[0], p[1]]; });". The pinned verifier confirms moving tree 3 breaks its six rows and preserves the other 25. Exactness describes the underlying certificate; the displayed coordinates and tolerance are explicitly approximate. - CONFIRMED The two pages on this site where a mathematical no is a file measured in gigabytes.
git show 9b112ed892:src/content/strata/boolean-pythagorean.md : N2 check: entry 169 (relation-0-0): The pinned companion page describes its "68-gigabyte certificate" reconstructing the almost 200-terabyte refutation. This establishes the stated relationship between the two pages, not an exhaustive claim about every later page on the site. - CONFIRMED Plane geometry with a wall built by SAT.
git show 9b112ed892:src/content/strata/coloring-the-plane.md : N2 check: entry 171 (relation-1-0): The companion page describes the SAT obstruction and de Grey's finite graph. The primary de Grey paper states "finite unit-distance graphs in the plane that are not 4-colourable". The orchard CNF implements the other stated translation. - CONFIRMED The chromatic number of the plane has its lower bound from a finite unit-distance graph that a solver refuses to colour; the orchard number at fifteen has its upper bound from a finite sign table that a solver refuses to fill.
https://arxiv.org/abs/1804.02385 : N2 check: entry 172 (relation-1-1): De Grey's primary abstract states "finite unit-distance graphs in the plane that are not 4-colourable"; the orchard ledger supplies the finite sign-table UNSAT result. The two lower/upper-bound directions are correctly distinguished. - CONFIRMED In both the geometry is translated into clauses before the machine is allowed near it, and the translation is the part a reader has to believe.
git show 9b112ed892:src/content/strata/coloring-the-plane.md : N2 check: entry 173 (relation-1-2): The companion page describes the SAT obstruction and de Grey's finite graph. The primary de Grey paper states "finite unit-distance graphs in the plane that are not 4-colourable". The orchard CNF implements the other stated translation. - CONFIRMED Same discipline, opposite direction.
git show 9b112ed892:research/orchard-15/RESULT-15-32.md : N2 check: entry 174 (relation-2-0): The recorded theorem says "No configuration of 15 points in the real plane has 32 lines through exactly three points." The ledger records four verified UNSAT cases and four cake_lpr acceptances. The CNF regeneration and exact lower-bound check were recreated here; the multi-hour SAT refutations were not rerun. - CONFIRMED Kin to The File That Said No, the other place on this site where a refutation is a file measured in gigabytes and the question is what a checked certificate does and does not explain; to How Many Colors Does the Plane Need?, a plane-geometry question with a wall built by SAT; and to No Triangle at Three for the method of compute exactly, search the catalogue, report what is actually established.
git show 9b112ed892:src/content/strata/boolean-pythagorean.md : N2 check: entry 176 (body-28-0): The pinned companion page describes its "68-gigabyte certificate" reconstructing the almost 200-terabyte refutation. This establishes the stated relationship between the two pages, not an exhaustive claim about every later page on the site. - CONFIRMED The budget is spent exactly: a known planting reaches the ceiling of 6, beating the cubic formula. t3(7) = 6.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 178 (calculator-verdict-7): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 21
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 179 (calculator-7-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 3
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 180 (calculator-7-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 6
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 181 (calculator-7-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 5
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 182 (calculator-7-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 8, cubic 7; the value is 7, settled by Burr, Grünbaum and Sloane in 1974.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 183 (calculator-verdict-8): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 28
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 184 (calculator-8-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 4
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 185 (calculator-8-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 8
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 186 (calculator-8-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 7
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 187 (calculator-8-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget and cubic agree at 10: Jackson's nine trees in ten rows, and the arithmetic alone proves nobody will ever do better.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://arxiv.org/pdf/1208.4714; https://books.google.com/books?id=0Qc3VEIxwCYC : N2 check: entry 188 (calculator-verdict-9): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 36
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 189 (calculator-9-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 4
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 190 (calculator-9-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 10
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 191 (calculator-9-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 10
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 192 (calculator-9-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 13, cubic 12; the value is 12, settled by Burr, Grünbaum and Sloane in 1974.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 193 (calculator-verdict-10): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 45
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 194 (calculator-10-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 5
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 195 (calculator-10-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 13
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 196 (calculator-10-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 12
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 197 (calculator-10-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED The budget is spent exactly: a known planting reaches the ceiling of 16, beating the cubic formula. t3(11) = 16.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 198 (calculator-verdict-11): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 55
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 199 (calculator-11-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 5
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 200 (calculator-11-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 16
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 201 (calculator-11-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 15
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 202 (calculator-11-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 20, cubic 19; the value is 19, settled by Burr, Grünbaum and Sloane in 1974.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 203 (calculator-verdict-12): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 66
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 204 (calculator-12-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 6
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 205 (calculator-12-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 20
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 206 (calculator-12-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 19
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 207 (calculator-12-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED pairs of trees 78
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 209 (calculator-13-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 6
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 210 (calculator-13-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 24
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 211 (calculator-13-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 22
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 212 (calculator-13-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED pairs of trees 91
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 214 (calculator-14-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 6
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 215 (calculator-14-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 28
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 216 (calculator-14-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 26
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 217 (calculator-14-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED pairs of trees 105
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 219 (calculator-15-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 7
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 220 (calculator-15-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 32
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 221 (calculator-15-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 31
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 222 (calculator-15-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED The budget is spent exactly: a known planting reaches the ceiling of 37, beating the cubic formula. t3(16) = 37.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 223 (calculator-verdict-16): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 120
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 224 (calculator-16-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 7
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 225 (calculator-16-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 37
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 226 (calculator-16-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 35
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 227 (calculator-16-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 42, cubic 40. The value lies between them and, so far as the catalogue records, has not been settled; Green and Tao say the cubic is right for all sufficiently large n, without saying how large.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 228 (calculator-verdict-17): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 136
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 229 (calculator-17-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 8
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 230 (calculator-17-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 42
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 231 (calculator-17-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 40
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 232 (calculator-17-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 48, cubic 46. The value lies between them and, so far as the catalogue records, has not been settled; Green and Tao say the cubic is right for all sufficiently large n, without saying how large.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 233 (calculator-verdict-18): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 153
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 234 (calculator-18-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 8
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 235 (calculator-18-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 48
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 236 (calculator-18-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 46
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 237 (calculator-18-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 54, cubic 51, and a known planting has 52 rows: it beats the formula without reaching the ceiling. The true value is 52, 53 or 54 by this arithmetic; 52 is the best planting known.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 238 (calculator-verdict-19): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 171
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 239 (calculator-19-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 9
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 240 (calculator-19-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 54
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 241 (calculator-19-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 51
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 242 (calculator-19-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 60, cubic 57. The value lies between them and, so far as the catalogue records, has not been settled; Green and Tao say the cubic is right for all sufficiently large n, without saying how large.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 243 (calculator-verdict-20): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 190
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 244 (calculator-20-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 9
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 245 (calculator-20-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 60
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 246 (calculator-20-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 57
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 247 (calculator-20-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 67, cubic 64. The value lies between them and, so far as the catalogue records, has not been settled; Green and Tao say the cubic is right for all sufficiently large n, without saying how large.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 248 (calculator-verdict-21): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 210
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 249 (calculator-21-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 9
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 250 (calculator-21-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 67
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 251 (calculator-21-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 64
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 252 (calculator-21-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 73, cubic 70. The value lies between them and, so far as the catalogue records, has not been settled; Green and Tao say the cubic is right for all sufficiently large n, without saying how large.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 253 (calculator-verdict-22): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 231
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 254 (calculator-22-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 10
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 255 (calculator-22-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 73
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 256 (calculator-22-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 70
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 257 (calculator-22-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 81, cubic 77. The value lies between them and, so far as the catalogue records, has not been settled; Green and Tao say the cubic is right for all sufficiently large n, without saying how large.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 258 (calculator-verdict-23): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 253
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 259 (calculator-23-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 10
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 260 (calculator-23-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 81
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 261 (calculator-23-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 77
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 262 (calculator-23-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED Budget 88, cubic 85. The value lies between them and, so far as the catalogue records, has not been settled; Green and Tao say the cubic is right for all sufficiently large n, without saying how large.
git show 9b112ed892:public/strata/no-thirty-second-row/index.html; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 263 (calculator-verdict-24): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED pairs of trees 276
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 264 (calculator-24-pairs): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED ordinary lines forced 11
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 265 (calculator-24-km): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the budget allows 88
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 266 (calculator-24-ceil): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED rows the cubic gives 85
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 267 (calculator-24-form): Each numeric cell was independently recomputed from n(n-1)/2, ceil(3n/7), floor((pairs-ordinary)/3), and floor(n(n-3)/6)+1. All 72 cells at n=7 through 24 agree with the record and the extracted page function. - CONFIRMED tree 0: on 7 rows of three and 0 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 268 (hover-tree-0): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 1: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 269 (hover-tree-1): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 2: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 270 (hover-tree-2): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 3: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 271 (hover-tree-3): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 4: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 272 (hover-tree-4): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 5: on 7 rows of three and 0 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 273 (hover-tree-5): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 6: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 274 (hover-tree-6): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 7: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 275 (hover-tree-7): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 8: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 276 (hover-tree-8): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 9: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 277 (hover-tree-9): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 10: on 7 rows of three and 0 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 278 (hover-tree-10): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 11: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 279 (hover-tree-11): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 12: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 280 (hover-tree-12): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 13: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 281 (hover-tree-13): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED tree 14: on 6 rows of three and 2 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 282 (hover-tree-14): The extracted line list independently gives degrees 7 at trees 0,5,10 and 6 at the other twelve trees, with ordinary degrees 0 and 2 respectively. All fifteen hover messages match the source record exactly. - CONFIRMED recounted: 31 rows of three, 0 of four or more, 12 two-tree lines
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 283 (recount-initial): The handlers recompute after movement and reset with "pts = EXACT.map(function (p) { return [p[0], p[1]]; });". The pinned verifier confirms moving tree 3 breaks its six rows and preserves the other 25. Exactness describes the underlying certificate; the displayed coordinates and tolerance are explicitly approximate. - CONFIRMED 28 rows would be a Steiner triple system minus a point, excluded by Burr, Grünbaum and Sloane
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg; https://neilsloane.com/doc/ORCHARD/scan_63520457_1.jpg : N2 check: entry 284 (dynamic-bgs14): The record selected a reduction about (15,32), which does not establish the attributed exclusion at 14. BGS Table I has upper bound 27 for 14; the 28-block pair budget would leave a perfect matching and extend combinatorially to an STS(15). BGS Table I records t(14) <= 27. The required 28-block structure is a Steiner triple system with one point removed; the seven leftover pairs complete it when that point is restored. - CONFIRMED 52 is the best planting known.
https://neilsloane.com/doc/ORCHARD/scan_63519405_1.jpg; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 286 (dynamic19-known): BGS Table I has lower bounds (7,6), (11,16), (16,37), (19,52). The corresponding cubic values are 5,15,35,51, and the Kelly-Moser ceilings are 6,16,37,54. All arithmetic was independently recomputed. - CONFIRMED The true value is 52, 53 or 54 by this arithmetic
git show 9b112ed892:public/strata/no-thirty-second-row/index.html : N2 check: entry 287 (dynamic19-bounds): The extracted budget() and verdictFor() were run for all 18 slider values. All 90 rendered calculator claims match the record. The arithmetic was independently recomputed; historical portions were checked with BGS, OEIS, Friedman and Green-Tao, and the new 13/14/15 results with their committed records. - CONFIRMED Jackson's nine trees in ten rows, and the arithmetic alone proves nobody will ever do better.
https://proofwiki.org/wiki/Orchard_Planting_Problem/Historical_Note; https://arxiv.org/pdf/1208.4714; https://books.google.com/books?id=0Qc3VEIxwCYC : N2 check: entry 288 (dynamic9): The historical transcription says "Your aid I want, nine trees to plant / In rows just half a score; / And let there be in each row three." Green and Tao p. 3 reproduces Jackson and identifies the 1821 book; the Google Books catalogue independently confirms author, title and 1821. - CONFIRMED Green and Tao say the cubic is right for all sufficiently large n, without saying how large.
https://arxiv.org/pdf/1208.4714 : N2 check: entry 289 (dynamic-large): Green and Tao p. 3 says a bound could be computed but "it would be of double exponential type" and they do not compute a numerical n0. This supports the page's qualification about how large. - CONFIRMED so far as the catalogue records, has not been settled
https://oeis.org/A003035/internal; https://erich-friedman.github.io/packing/trees/; https://arxiv.org/pdf/1208.4714 : N2 check: entry 290 (dynamic-unsettled): OEIS supports n=17 directly; Friedman supplies the remaining displayed ranges through n=24. OEIS retains Sloane's dated comment "It is known that a(15) is 31 or 32, a(16)=37 and a(17) is 40, 41 or 42." The 1974 lower/upper bounds also appear in BGS Table I.
What was done
- [fixed] X1: stated the nonzero alternating table and rank-3 matroid-support conditions in the hand-authored sign explanation; added Corrected 2026-10-01 in the page's Corrections note and mirrored it in the markdown body. The partial triple system already supplies that support in the solver.
- [dated] X2: replaced the caption's 10.6 GB with the 19.6 GB sum of the seven displayed sizes, explicitly scoped to that table; the single Updated 2026-10-01 line dates the former subtotal to 2026-09-05 and cube 3's cadical verification to 2026-09-06. The retained depth-2 summary now supplies the verifier's child count and proof-byte total.
- [fixed] X3: changed without any symmetry breaking to without lex-leader symmetry breaking; retained the supported model count. MINOR, so no page correction line.
- [fixed] X4: documented Python, python-sat, cadical and drat-trim dependencies; replaced the mismatched two-hour cube-3 time with the recorded cadical solve time of about five hours and separated the successful checker rerun of about 12.6 hours. MINOR, so no page correction line.
- [dated] X6: updated the related-page note to the displayed ledger's 19.6 GB subtotal. The one Updated 2026-10-01 line for X2/X6/X7 is mirrored in the markdown body.
- [dated] X7: the duplicate subtotal entry shares X2's single Updated 2026-10-01 line. The verifier now adds every displayed proof size and checks the caption itself, so a correct value in the revision note cannot hide a stale caption.
- [fixed] X5: the director corrected the source generator for this page, regenerated its footer and added the dated Corrected line in HTML and markdown.