Watch the nonacube proof
An exact recording of the SAT search that rules out a second lattice corona. Follow every decision, conflict, backjump and restart, or jump to its largest connected patch.
Decision depth in the current recording segment. Pink marks conflicts. The white line is the current event.
Does it visit every branch?
Glucose uses conflict-driven clause learning (CDCL). It makes Boolean decisions, propagates consequences, learns a clause when it reaches a contradiction, and backjumps. Learned clauses rule out whole families of branches. The checked proof establishes exhaustive exclusion, without literally visiting every leaf of an unpruned tree.
This recording retains every decision, including auxiliary Boolean decisions that do not change the picture. Tile assignments forced between events are applied exactly. At high speed all events are processed, while the screen shows the latest state each animation frame. Use single-step or slow playback to see each event.
Conflicting states can temporarily contain overlapping selected tiles before propagation reports the contradiction; those cubes turn pink. Such states do not count toward the largest legal patch.
What does “largest” mean?
Measuring the recorded run…
Both maxima count tiles, including the root, at propagation-complete states just before a decision. They are maxima of this run, not optima over all finite packings. A large patch can leave holes and fail to complete even the first surround. Coverage and tile count measure different things.
The instrumented run reproduced the original proof byte for byte. Its proof was independently checked by DRAT-trim. Under integer translations, cubic rotations and complete face/edge/vertex surrounds, a verified first corona and the absence of any second corona establish \(H=1\). No topological-ball condition is imposed.