T-055: by a point-only route
V3 C3 simplification confirmed
by a second, point-only route: the lower half by wand125's point-only measure, completed on 28 September 2026 with a Lean 4 reduction, the upper half by the grid.
The lower half is Evan Daniel's s21_lower_4.9950.txt support (T-050) scaled by 1001/1000 and re-weighted, 4,604 D4-invariant entries of total 2624862500021/125000000000, with capture threshold q = 249987/250000 over every closed unit square in [0,5]^2, so that 21q exceeds the total by 999979/125000000000.
The capture statement is decided by the source's own exact rational replay of a retained certificate tree over 5,000 root boxes, and Lean proves minSide 21 = 5 from that one hypothesis.
That replay was run here in full on 29 September 2026, the source's runner unchanged: every stage passed, and its records match the source's M1 run, 45,436 of the 45,446 output files byte for byte and the rest in every certified quantity. The Lean overlay was not built here.
wand125 after Evan Daniel, square-packing-bounds. The source names Daniel's mixed-cover proof (T-052) as first, claims no priority, and says its code was developed with Codex.
Significance, composition and next rung
- Significance
- A second, point-only route to a value T-052 already holds, with a positive-margin threshold rather than a zero-margin cover and a Lean reduction of its own. A citable detail that changes no theorem.
- Composition
- Compound, and the minimum is set by the lower half. The lower half is E-n021-wand125-point-endpoint-source-replay (exact-algebraic, the source's runner replayed here), the upper half the grid (E-basic-grid-upper); the equality is C3. The runner is the source's, so the replay, reproduced with the producer's code, confirms the source's run rather than adding a second method, and the Lean reduction, not built here, adds nothing to the rung.
- Next rung
- V4 and C4 need two adversarial AI reviews by distinct reviewers and a human oversight record; one adversarial review is retained. A build of the Lean overlay with its axiom receipt, and the runner's lemmas formalised (review F10), would be the road to rung 5. The controls end at the first root box that holds a pose, so neither exercises the sieve or frontier stages; a control refused deeper in the tree would test more of the runner.
- Novelty
- previously-published Present in an identified source
The case
Results on the case
12 results in the register on , oldest first, each with what it established and how it stands now.
2005 published T-007
for
V0 C1 lower bound incomplete on this case, superseded by T-052
Nagamochi · Nagamochi 2005 · source · register
2026-09-04 established T-020
for
V3 C3 lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-04 published T-085
Nagamochi 2005, Lemma 1 is false for every container with and
V3 C3 correction confirmed
Karakuş; chelokot · Karakuş 2026 · chelokot Nagamochi counterexample 2026 · packet · register
2026-09-05 established T-021
for
V3 C3 lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-23 established T-034
V3 C3 lower bound confirmed superseded by T-052
Levy after Burns, Massaccesi · register
2026-09-23 published T-050
V3 C3 lower bound confirmed superseded by T-052
Daniel after Burns, Massaccesi · evand square-packing 2026 · packet · source · review · register
2026-09-27 published T-052
, by a mixed cover of points and grid-line segments
V3 C3 optimality confirmed
Daniel after Burns, Massaccesi · evand square-packing 2026-09-28 · packet · source · review · register
2026-09-28 published T-055 this result
by a point-only route
V3 C3 simplification confirmed
wand125 after Daniel, Tokoharu, Levy, Stromquist, Nagamochi, Burns, Massaccesi · wand125 point and mixed bounds 2026-09-28 · packet · source · review · register
2026-09-29 published T-058
Rectangle-certificate ceiling
α·UB(n)proved for ..100;B·UB(n)on 64 grid rowsV3 C3 method limit confirmed
wand125 after Tokoharu, Daniel · wand125 tools 2026 · packet · register
2026-09-29 published T-083
for every nonsquare
V3 C3 lower bound confirmed on this case, superseded by T-052
Karakuş · Karakuş 2026 · source · register
2026-10-03 published T-081
for every integer from 5 up; are the cases held here
V0 C1 optimality reviewed on this case, second certificate, reported
Daniel after Burns, Massaccesi · evand square-packing 2026-10-03 · packet · packet · source · review · register
2026-10-07 published T-124
Reported non-strict local minima for 178 source configurations
V0 C0 restricted optimality recorded
Daniel after Couzo · Daniel exact and local reports 2026 · packet · register
Links
- On this site
- Case record, · Frontier row, · T-055 in the results table
On GitHub, at main
- Register
- T-055 in
results.yaml, line 4810 - Evidence
E-n021-wand125-point-endpoint-report·E-n021-wand125-point-endpoint-source-replay·E-basic-grid-upper- Proofs and certificates
- certificate
n21-original.txt.gz· proofREADME.md· auditreview-2026-09-28-wand125-point-only-s21-s45.md - Sources
- wand125 point and mixed bounds 2026-09-28 (its own site, retained copy)
- Source packet
resources/web/wand125-point-and-mixed-2026-09-28/README.md- Artifacts
13 artifacts and controls
resources/web/wand125-point-and-mixed-2026-09-28/README.mdresources/web/wand125-point-and-mixed-2026-09-28/square-packing-bounds/point_n21_L5/certificates/n21-original.txt.gzresources/web/wand125-point-and-mixed-2026-09-28/square-packing-bounds/point_n21_L5/README.mdresources/web/wand125-point-and-mixed-2026-09-28/receipts/n21/stage_comparison.jsonresources/web/wand125-point-and-mixed-2026-09-28/receipts/n21/result.jsonresources/web/wand125-point-and-mixed-2026-09-28/receipts/n21/comparison.jsonresources/web/wand125-point-and-mixed-2026-09-28/receipts/exact-audit.jsondevtools/audit_wand125_point_and_mixed.pydevtools/check_basic_bounds.pydocs/project/reviews/review-2026-09-28-wand125-point-only-s21-s45.mdtests/test_wand125_checker_controls.pyresources/web/wand125-point-and-mixed-2026-09-28/receipts/controls/n21_control_drop-heaviest-point.logresources/web/wand125-point-and-mixed-2026-09-28/receipts/controls/n21_control_move-point.log- Case file
frontier/n-021.md(verified lower, verified upper, reported lower, reported upper)