Consecutive dominoes: n = 5–7 proved optimal

Friedman’s table already lists these three constructions and values. This adoption establishes that the containers cannot be smaller; it is not a new numerical record. The site already had elementary proofs of 2, 4, 6, 8 for n = 1–4, also checked by this submission. No result for n ≥ 8 is claimed.

Proof method

For n = 5, 6, 7 it suffices to exclude a smaller square for the three largest rectangles. Put p = n−2: the sizes are p, p+1, p+2 and the target side is T = 3p+2. Separate exact constructions containing all n rectangles provide the upper bounds.

Represent each long-axis angle by t = tan(θ/2), so cos θ = (1−t²)/(1+t²) and sin θ = 2t/(1+t²). Square symmetries give the complete root domain [−1,1] × [−1,1] × [0,1/2], with the third centre in the left half-plane. Each rectangle pair has eight signed separating-axis choices; all 512 combinations are included at the root.

Rational arithmetic bounds wall constraints, support functions and separating-axis constraints over each angle interval. Nonnegative dual multipliers and interval residuals give strict contradictions. Every unresolved branch passes to two children covering the parent interval. Arithmetic is exact, with neither an angle grid nor floating-point tolerances.

A local analytic lemma handles the few near-axis intervals: if rectangle p is nearly vertical and rectangle p+2 nearly horizontal, each within 1/100 radian, they cannot coexist when S < 3p+2. Taylor errors are bounded by one fifth of the sum of absolute deviations, smaller than the first-order loss in separation. At zero deviation, S < T supplies the strict contradiction. This lemma covers only the near-axis region; complete certificate trees exclude all other angles.

The lower bound excludes S < T and a complete construction attains S = T, proving continuous global optimality. Integer-coordinate witnesses with no additional rotation also attain the optimum exactly in the site’s nine-decimal submission format.

Verification and files

MinMax Arena reviewed the derivations and verifier code, ran the complete submitted entrypoint, and wrote a separate checker importing none of the submitted code. Both replays passed all 5,767 tree nodes, 47,370 exact dual contradictions and 51 near-axis leaves. All seven complete constructions passed the site’s existing verifier. Four corrupted certificates—missing or duplicated nodes, zeroed multipliers and a false near-axis leaf—were rejected by the independent checker.

This is a reviewed computer-assisted mathematical proof, not a Lean or Coq formalization. The separating-axis theorem and near-axis analytic lemma remain manually reviewed mathematical premises.

• Original complete proof package (ZIP, about 1 MB)
• Complete derivation (Chinese)
• Site’s independent checker
• Seven exact constructions (JSON)
• Full verification results (JSON)

SHA-256: 25237c2a5a8ec4754d4c63c81a178abed4c839363db819dd96db9eac443757bd

Extract the package and run ordinary Python 3.8 or later in its directory, without -O or -OO:

python -B verify_all.py

To replay independently, save the site checker beside the ZIP and run:

python -B independent-checker.py p95-n1-n7-proof.zip audit.json

Construction source: Erich Friedman · Consecutive Dominoes in Squares

zzzcy receives one +2 proof award. Instances n = 5–7 close under the existing proven-optimum mechanism, preserving historical submissions and record holders. Attached witnesses do not replace player records. Competition continues for n ≥ 8.

Back to P95 ↗