T-207: Mixed rectangle-measure lower bound $s(85)\ge 379/40$$s(85)\ge 379/40$ verified, on the 201-direction net

S3 V3 C3 Lower bound confirmed

2026-10-16 published · Hosono after Tokoharu and Levy · $n=85$$n=85$

A rectangle measure of wand125/square-packing, published on 16 October 2026 and reported in jlevy/squares#446, proves $s(85)\ge 379/40$$s(85)\ge 379/40$ = 9.475.

The certificate, mixed_n85_L9475, is a density of 838 uniform rectangles in D4 orbits, 6672 distinct rectangles after expansion, and no point or segment, of total mass 8499999/100000 < 85. Its declared net has 201 half-angle tangents of step 83/40000 at core side 9977/10000. The strict core extent 399908091/400000000 < 1 and the last tangent 83/200, past tan(pi/8), supply the reviewed net-and-shrink implication.

The retained maintained sqverify-fast capture verifies all 201 directions at threshold one, under the qualified Mac release build of Rust 1.98.0. Its whole-net controls record 201 coverage refusals and no verified mutant direction, and the near-threshold mutant is refused. The mathematical review accepts the implication and independently recomputed the saved-point captures. The outer capture, check and control commands all have observed exit 0.

This raises the verified and reported lower lanes from 473/50 to 379/40. The bound is confirmed by a re-implementation sharing components with the producer's checker, sqverify-proof-net, which is Hosono's adaptation of this repository's sqverify_fast crate: the two share the crate apart from their declared-net readers. The exact audits check premises and saved poses, not coverage between poses; no independent full implementation, second method, proof-assistant check or optimality theorem is claimed.

wand125 after Tokoharu and Levy, square-packing. The source says parts of the work were produced with AI assistance under human direction.