Six unit squares in a strip of height 1.87 ≤ H < 2: the minimum width is F6(H)

For every H with 1.87 ≤ H < 2, every packing of six unit squares with arbitrary rotations and pairwise disjoint interiors in a rectangle of width L and height H has L ≥ F6(H) = min over θ of 2 + (4 − (3H − 2) cos θ)/sin θ + (4 − 2H sin θ)/cos θ; the bound is attained by Morandi's configuration (Friedman, Math Magic, June 2010), so F6(H) is the exact minimum width. The proof is computer-assisted: an elementary reduction from packings to 64 floor/ceiling chain functions, a certified min-plus dynamic program for the 62 non-alternating patterns, and for the alternating pattern a support-function dual with an analytic reduction to a compact box and a certified branch-and-bound with outward rounding. Premises: IEEE-754 binary64 with directed rounding and an 8-ulp libm padding. Source, certificates, replay commands and three blind referee reports are in the linked repositories. The interval [1.8611, 1.87), where the statement remains meaningful, is not covered.