This packet certifies a previously reported observation by Pico: the nonempty finite ten-label TenSystem remains inconsistent after deleting only downward closure. The other five source fields are retained, including no-boundary for every three-face whether or not it lies in T. The written reduction handles arbitrary subset-family T. Nonempty Q is unrestricted; no symmetry reduction or distinguished tetrahedron is used. The direct input has 330 variables and 30361 clauses. A new 18302-addition reverse-unit-propagation certificate ends in the empty clause and passes both a watched-literal replay and a separate bitmask full-scan replay. The packet includes the source-to-CNF argument, exact source pins, independent clause reconstruction, 424 local truth-table cases, 29 tests, explicit satisfiable further weakenings, corrupt/truncated rejection controls, and reproducible generation metadata. This is a finite logical certificate with a written translation, not a formally verified implementation or a new Borsuk theorem. Topology, geometry, the complete source Lean development, and the census classification remain outside scope. It certifies Pico's prior observation without claiming discovery priority. One scoped separate AI review is documented; human peer review and global novelty are not claimed. The follow-up PR11 is open at archival preparation. Alexander Richard Towell contributed with substantial OpenAI Codex assistance. OpenAI's source definition, Pico/Håkon Åmdal's observation and census, prior Towell/Codex replay engines, and Glucose/PySAT are credited. The original accepted finite packet is included as an explicitly identified dependency. Canonical source is commit c714c0a27e1cb668d63c6aa7a8c373aab0f2f9d9; first public disclosure of the new certificate was 20 October 2026.
No takes yet. Share an insight, caveat, or question.
Alexander Towell (2026) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: