Exact value s(76) = 9 (k = 9 of the k² − 5 series): registration request (external certificate)

Credit name. Benjamin Greff.

Claim. s(76) = 9. The upper bound is the 9 × 9 grid. What is new is the lower bound: packing/frontier/n-076.md records the case as open, at 8.965 (wand125). This is the case k = 9 of the k² − 5 series, after wand125's s(59) = 8 (#280), and it sits next to wand125's s(77) = 9 (#279).

Certificate. A mixed cover in Evan Daniel's "mixed 1" format at side exactly 9:

41,633 weighted points and 9,744 axis-parallel segments; coordinates X/8000, weights w/(4·10⁸)
total 3788361049/50000000 = 75.76722098 < 76
exactly D4-invariant
cover/s76_cover_v5.txt.gz, SHA-256 of the unpacked file b6a1214b99f00e5dd136d74c8d87bccd178df38a1063b2c7be90517eb2b862b2

It is in https://github.com/bengreff/s76-certificate at commit 1cb924fa2fb7e8e30d8ddeb9b5e0dfcfae4f9f1f. The logs and per-root records of every run below are in records/, and SHA256SUMS covers all files in the tree.

Checking. All checkers are Evan Daniel's, unchanged, from evand/square-packing at b91d70b6ed314624c1434b628a9c7bf9a132c743. verify.sh fetches them and checks the SHA-256 of zmx2.rs, zm_mixed.py, zeromargin.py and mixed_cover.py.

step	checker, arithmetic	region	result	cost
format, weights ≥ 0, atoms in [0,9]², exact total	`tools/check_total.py` (Python `Fraction`, stdlib only)	whole file	`3788361049/50000000 < 76`	seconds
D4 invariance	`zmx2 d4` (exact integers)	whole file	invariant	seconds
covering	`zmx2 cert --d4` (outward-rounded binary64)	8,100 roots, 1/10 × 1/10 × 1/8 in u	14,672,104 boxes; 8,096 roots certified; 18 boxes uncertified in 4 roots; none capped	275–297 CPU-s
covering	`zm_mixed.py cert --d4 --cert-mode --disj --chain-from 0 --pitch 1/20 --ubins 16 --depth 24` (exact rationals)	the 4 roots, split into 64 roots of 1/20 × 1/20 × 1/32	4,950 boxes, max depth 15, 0 uncertified	about 23 CPU-min
coverage	`tools/check_coverage.py` (`Fraction`, stdlib only)	—	the 8,100 zmx2 roots tile the region; the 64 zm_mixed roots tile the 4 remaining ones exactly (containment plus equal volume); every zm_mixed record has `UNCERT 0`, an empty `unc` list and the cover's SHA-256 in its header	seconds

The four zmx2 roots are listed in records/zmx2/failing_roots.txt. The composite check reads the root boxes as exact fractions from the records, not from printed decimals.

sh verify.sh <new dir> [threads] reruns all of it from a fresh clone. A clean replay took 9 min 13 s wall on 4 threads of an i7-14700K (WSL2, rustc 1.99.0, Python 3.11); the toolchain and zmx2 binary hash are in records/toolchain.txt. As a control, changing one weight by 1/(4·10⁸) makes zmx2 d4 refuse the cover with exit status 2, which stops verify.sh.

In progress. A second pass runs zm_mixed alone over the whole D4 region: 129,600 roots of 1/20 × 1/20 × 1/32, the same flags. At the time of writing, 42,000 roots are done with 0 uncertified. It should finish within a day. I will add its records and manifest to the repository and post the commit here. verify.sh --full-zm runs it.

What the checkers share. zmx2 and zm_mixed are both Evan Daniel's, and both use the D4 reduction to centres in [0, 9/2]² and u = tan(θ/2) ∈ [0, 1/2]. zmx2 alone decides 8,096 roots and zm_mixed alone decides the other 4, so no root rests on both. The full zm_mixed pass, when done, puts the whole region under the exact-rational checker. I wrote no covering checker, only the two stdlib scripts that check the total and the tiling.

Lean. lean/S76Lower.lean builds on Evan Daniel's Sqpack at 1718a58 (Lean v4.33.1):

theorem s76_eq_9 (hcov : S76Cover) : minSide 76 = 9
-- depends on axioms: [propext, Classical.choice, Quot.sound]

The data facts are kernel-checked by decide +kernel on S76T/Pts.lean, which is generated from the cover by lean/mk_s76_lean.py: no duplicate atoms, exact D4 invariance, and total < 76. S76Cover is the covering statement (CovM on the D4 fundamental region) and is a hypothesis, not proved in Lean. The build summary is in lean/build_summary.txt.

Not done.

The covering statement is not formalized.
The full zm_mixed pass is unfinished (see above).
There has been no review outside this project.

Lineage and credit.

Evan Daniel (MIT): the weighted-cover method at margin zero, the mixed format, the checkers, and the Lean library (le_minSide_mixed, CovM).
wand125 (MIT): the four corner regions [0, 2.5)² and their images are wand125's s(59) = 8 cover, unchanged except for the band insertion of their s(77) construction: cut at x = 4 and y = 4, and shift the far side by 1. The input's SHA-256 is 6f4d2b64….
Mine: the cross {x or y ∈ [2.5, 6.5]} was re-optimized by LP over D4-orbit weights, with free points capped at 0.004 and row margin 0.005. Candidates were a 1/20 lattice, the base's own positions, 1/16 segments on integer lines, and 2/1000 segments for lattice points on integer lines. Rows came from cutting planes: GPU screening, zmx2 sweeps, and dense float64 scans of the zmx2-failing roots. The scripts are in construction/; they are research code and not needed to check the proof.

Notes that may help others.

zmx2's float-min in uncertified boxes can miss real violations. Two intermediate covers had a handful of zmx2-failing roots, and float minima ≥ 1 were logged there. Both had genuine violations, with exact μ = 0.98998 and 0.99857 from zm_mixed.py pose. Only dense float64 scans of the failing roots found them.
Exact coincidences at θ = 2·arctan(1/3), the 3-4-5 angle, defeat zm_mixed at any depth. One root kept 2 uncertified boxes at depths 34, 48 and 64 around a single pose. There, 15 lattice atoms lay on the edges of one square, in pairs on opposite edges, yet μ ≥ 1.009 at the pose. Excluding the coincident lattice points fixed it; 28 orbits were excluded in the end.
Bottom-wall tile germs next to the corner/cross seam needed margin of about 0.012 before zm_mixed closed them at depth 24.

AI assistance. Yes, extensively. I chose the problem and the standard of proof, and directed the work. Claude (Anthropic), working as an agent in Claude Code, built and ran the LP search, the export, the verification script, the coverage checks, the Lean wrapper and the replay, and drafted this write-up.

Next. I plan to run the same pipeline on s(95) = 10 and s(116) = 11 (k = 10, 11). I'm posting so the work isn't duplicated.

@bengreff

@bengreff, thank you for the report, and for publishing the cover with the run records of both checkers. We have pinned bengreff/s76-certificate at 1cb924fa2fb7e8e30d8ddeb9b5e0dfcfae4f9f1f and retained the whole tree here, with the credit and AI-assistance statements as your README and this issue give them.

In triage we ran your certificate with Evan Daniel's checkers, built from the copies this repository already holds at the digests your verify.sh pins. zmx2 cert --d4 leaves the same 18 boxes in the same four roots, with every root's census equal to records/zmx2/zmx2_v5.log, and zm_mixed.py with your flags certifies all 64 sub-roots, with records equal to yours apart from the input path and the CPU time. The total, the D4 invariance and the tiling check exactly, the corners are wand125's s(59) cover as you say, and the Lean data matches the cover file. Two mutated covers are refused by zmx2, and zm_mixed.py pose finds a pose in each where the capture is below one.

Next, we will register the result as reported, and a separate review of the mathematics, including the composite of the two checkers, will decide how it stands. When the full zm_mixed.py pass is published, please post its commit here: we will retain it as a new revision. One small question: the cover carries sixteen segments of mass 1/(4·10⁸) on the container's walls. They change no zmx2 decision (we checked), so they look like LP residue; were they intended?

Generated by Claude Code

Update: the second route is done. It is in the repository at commit 06993982e83dba37ca12121bd876396a15571fcb, which only adds records and one checker. The cover and the first route at 1cb924f are unchanged.

zm_mixed alone over the whole D4 region used the same flags as the issue: 129,600 roots of 1/20 × 1/20 × 1/32, 2,227,114 boxes, 181 CPU-hours (7.7 h on 24 processes). At depth 24 it certifies 129,599 roots and leaves 6 boxes uncertified in one root, R = [27/20, 7/5] × [13/10, 27/20] × [1/4, 9/32].
R lies in a corner taken unchanged from wand125's s(59) cover. A unit square centred in R stays inside [0, 2.5)². It is the root that wand125's depth-24 run of s(59) left with 6 boxes (Exact value s(59) = 8 (k = 8 of the k² − 5 series): registration request (external certificate) #280). Run alone at depth 34, R certifies with 13,767 boxes, max depth 26 and 0 uncertified, the same box count as for s(59). This took 44 CPU-minutes.
tools/check_full.py uses the standard library only, with Fraction. Every root of the region must have a record, every header must name this cover and the pinned checker files in cert and D4 mode, and each root must be certified in the full run or in the rerun. It rejects four mutated controls: the rerun left out, one record dropped, the rerun marked uncertified, and a different cover hash.
The records are in records/zm_full/:
- roots.jsonl.gz; the SHA-256 of the unpacked file, 564bac26…, matches the manifest
- manifest.json
- the log
- the rerun files rerun_R_depth34.*
verify.sh now runs check_full.py on the shipped records as part of the default run, which takes seconds. --full-zm repeats the computation.

The covering statement now rests on zm_mixed's exact arithmetic alone, as well as on the zmx2 + zm_mixed composite in the issue. Still not done: the covering statement in Lean, and any review outside this project.

Site: Themes, #6 (s(76) = 9) stopped after jlevy/squares#594

requests: record the 14 October replies and entries; read evand to 62…

@bengreff

@bengreff, thank you. With #602 merged, your result is registered on main:

T-184, V0/C0, significance S3, recorded: s(76) = 9, the lower half by your mixed cover and the upper half by the 9 × 9 grid, credited Greff after Daniel, wand125. Our rerun of zmx2 and zm_mixed.py from the bytes you pin matched your records and refused two mutations; that reproduction is kept in the packet but is not yet recorded as evidence, so the value stands as reported. The case page keeps s(76) ≥ 1793/200 (wand125) until a review.
Next, for C3: the reproduction recorded as evidence, and a review that reads the cover, the two checkers' composite over the D4 region and the wall segments.
Your second route at 06993982 came after the import, so it is not registered yet. The next revision of the packet retains it.

The question in our first reply about the sixteen wall segments of mass 1/(4·10⁸) is still open.

Evidence: E-bengreff-594-cover-report (your report, recorded). On main: RESULTS.md, the packet.

Generated by Claude Code

requests: record #602's post-merge follow-ups and the 14 October verd…

Thank you for the reproduction and the registration.

On the sixteen wall segments: they were not intended. They are residue of the LP.

Where they come from. For every 1/20-lattice point on an integer line, the LP's candidates include a segment of length 2/1000 along that line, centred on the point. At a crossing there is one along each line. That gives 81 such candidates on the wall x = 0 inside the cross, and their images on the other walls.
How they got mass. The interior-point solve, run without crossover, returned weight 0 for all but four of those D4 orbits. The four are the segments at the crossings (0, 3), (0, 4), (0, 5), (0, 6) and their images, which came out at about 1.04·10⁻¹². export_cover.py rounds every weight up to the unit 1/(4·10⁸), so each became one unit.
Why it is harmless. Rounding up only adds mass, so they can only raise captures. Their 16/(4·10⁸) = 4·10⁻⁸ is included in the total 3788361049/50000000.
Their partners. The horizontal segments at those crossings, [0, 2/1000] and [0, 1/16] on y = 3, …, 6 and their images, also carry a single unit each, for the same reason.

The pinned cover stays as it is.

intake #610: zm_mixed.py replays all 304 s(95) sub-roots, equal to th…

resources: retain Benjamin Greff's s(76) certificate, its key and the…

merge: the review lane for bengreff's jlevy#594, s(76) = 9

@bengreff

@bengreff, thank you for the explanation of the sixteen wall segments. With #627 merged, it is recorded in this issue's entry in result-requests.yaml on main: they are LP residue, interior-point weights of about 1.04·10⁻¹² that export_cover.py rounded up to the unit 1/(4·10⁸). Rounding up can only raise captures, and their mass is counted in the total. That answers the question in our first reply. The pinned cover stays as it is, and no result changes.

Where the result stands is unchanged since our reply of 14 October:

T-184, V0/C0, recorded: s(76) = 9. Our reproduction of zmx2 and zm_mixed.py is kept in the packet but not yet recorded as evidence. The case page at n = 76 keeps s(76) ≥ 1793/200 (wand125) until a review.
Next, for C3: the reproduction recorded as evidence, with case 76 registered in our replay and audit tools, and a review that reads the cover, the two checkers' composite over the D4 region and the wall segments.
Your second route at 06993982 is not registered yet; the next revision of the packet retains it (think-osvq).

The same pattern shows in your s(95) cover on #610, at every lattice point of the cross, and without those segments zmx2 makes every decision the same there too.

This issue stays open while that work is queued, and a reply follows each change in the record.

Generated by Claude Code

@bengreff

@bengreff, a follow-up to our reply of 16 October, which gave your result as V0/C0, recorded. With #649 merged, it has moved on main:

T-184, V3/C1, reviewed: s(76) = 9, the lower half by your mixed cover and the upper half by the 9 × 9 grid, credited Greff after Daniel, wand125. Our reproduction of your two checkers' runs, zmx2 over all 8,100 roots and zm_mixed.py over the 64 sub-roots, from the bytes you pin, is now recorded as evidence. It is a reproduction with the producer's code, Evan Daniel's checkers, read as one decision over the D4 region. The stage 4 review of 16 October of the cover and of that composite found no mathematical defect and no blocking finding. Your report's evidence entry, E-bengreff-594-cover-report, is now reviewed.
Why C1 and not yet C3: the confirmation is held until zm_mixed.py's mutated-certificate controls are held, two mutated certificates refused by it and kept by a test. The rule is already met for zmx2. Whether a refusal the review found at a depth limit of 12 counts as one of the two is a question for the owner, and a second is owed either way.
On the case page. n = 76 keeps wand125's 1793/200 as its lower bound until the case adopts the value, so the entry is pending adoption there.
Your second route at 06993982 is still not registered; the next revision of the packet retains it.

On main. packing/frontier/RESULTS.md, packing/frontier/n-076.md, the review.

This issue stays open while that work is queued, and a reply follows each change in the record.

Generated by Claude Code

Where this request stands in the record on main.

What is registered.

s(76) = 9: the lower half by a mixed cover, the upper half by the 9 x 9 grid:
- T-184, reviewed: its argument has been read here and no blocking defect found, and no replay here has passed yet (V3/C1). On the frontier it is pending adoption: better than its case records hold, and not yet taken into them.

Not registered.

zm_mixed.py alone certifies the cover over the whole D4 region, with one root rerun at depth 34: Posted after the import; the next revision of the bengreff packet retains it (think-osvq).

What remains, and which beads own it.

T-184: C3 waits on stage 4's control rule for zm_mixed.py, which decides the 64 sub-roots: two mutated certificates refused by it and held by a test. The review's depth-12 pair is one if a refusal at a depth limit of 12 counts, which is owner question 16 (think-l3oo, the review's finding F8); a second is owed either way, and refusals at the source's limit of 24 did not finish. The rule is met for zmx2. V4 and C4 then need a second adversarial AI review by a distinct reviewer and a human oversight record; one adversarial review is retained. An unreduced zmx2 --full sweep (about 6 CPU-hours with its follow-up, think-eucc) would take the D4 reduction off the zmx2 part. Owned by think-osvq.

On main. packing/frontier/RESULTS.md, docs/project/reviews/review-2026-10-16-greff-k2m5-mixed-covers-76-95.md, packing/frontier/n-076.md.

Nothing you asked for is queued, so this issue is closed with this comment. Closing it confirms nothing above that is still open: each entry stands at the rungs given, what remains of its validation is owned by think-osvq, and a follow-up will be posted on this issue whenever an id, a rung, a status or a position above changes.

Generated by Claude Code

@bengreff

@bengreff, a follow-up to our comment of 26 October, which gave your result as V3/C1, reviewed, pending adoption. With #886 merged, it has moved on main:

T-184, V3/C3, confirmed: s(76) = 9, the lower half by your mixed cover and the upper half by the 9 × 9 grid, credited Greff after Daniel, Hosono. It is confirmed, reproduced with the producer's code: Evan Daniel's zmx2 over all 8,100 D4 roots and zm_mixed.py over the 64 sub-roots of the other four, run here from the bytes you pin and read as one decision over the D4 region.
The controls that held it at C1 are done. Stage 4 asks that each checker refuse two mutated certificates. zmx2 already refused your cover with its heaviest point orbit dropped and with its heaviest segment orbit dropped. zm_mixed.py, with your verify.sh flags and its depth limit of 24, now refuses two uniform scalings of your cover, every mass multiplied by 49979/50000 and by 49301/50000, each on a cell where it certifies your cover with the same flags. Each refusal is true: at a pose in that cell the scaled cover captures 0.9999974 and 0.9999833 exactly. Both zm_mixed.py controls come from one mutation family, a uniform scaling just below one; a test keeps both pairs. No ruling on the review's refusal at a depth limit of 12 was needed.
The case page. n = 76 now adopts the value: s(76) = 9 is proved there, and Hiroaki Hosono's 1793/200 (T-091) is superseded.
Your second route at 06993982, zm_mixed.py alone over all 129,600 D4 roots with one root rerun at depth 34, has been retained here as reported since 31 October, in a packet of its own. It is not run or audited here; audited, it would put every cell under zm_mixed.py.
What remains, for V4/C4: a second adversarial AI review by a distinct reviewer and a human oversight record. That and the audit of the second route stay with think-osvq.

On main. packing/frontier/RESULTS.md, packing/frontier/n-076.md, the packet, the second route's packet.

The issue stays closed; this brings what the record says up to date.

Generated by Claude Code

Merge pull request #888 from jlevy/claude/bold-ritchie-xo28us-l31

Navigation Menu

Repository navigation

Exact value s(76) = 9 (k = 9 of the k² − 5 series): registration request (external certificate) #594

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Exact value s(76) = 9 (k = 9 of the k² − 5 series): registration request (external certificate) #594

Description

Activity

jlevy commented on Oct 14, 2026

bengreff commented on Oct 14, 2026

jlevy commented on Oct 14, 2026

bengreff commented on Oct 15, 2026

jlevy commented on Oct 16, 2026

jlevy commented on Oct 20, 2026

jlevy commented on Oct 26, 2026

jlevy commented on Nov 2, 2026

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions