What was already known
Carrion and coauthors asked the factorial-pair question, and Schafhauser, Tikuisis and White posed the completion form as Problem XXII. Related homogeneous-block and commutator obstructions were known.
AI involvement
Sauers directed the project; the repository credits Astra with the counterexample argument, Claude with exposition and Lean work, and Codex with Lean and submission work.
Astra is explicitly credited with developing the original retained counterexample argument; Sauers directed the project.
Importance
The unconditional constructions answer two stated questions about traces on tracial completions.
Limitations
Neither construction is claimed to be nuclear or simple. The source’s historical priority search is limited, and no human expert proof review is documented.
Technical verification
The repository reports a full Lean build, definition-model and axiom checks, exact Comparator statement comparison and Lean/NanoDa replay. The successful run is tied to an earlier source revision with a documented byte-equivalent Lean package at the cited revision; this review did not independently replay it.
Formal checking
Full build, definition checks, statement comparison, axiom audit and independent proof replay; final-package workflow checks Lean-byte equivalence to verified revision
- Checker
- Lean, Comparator and NanoDa in the reported GitHub Actions run
- Scope
- Both unconditional discontinuous-trace existence theorems selected for Palomar
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
No named human explanation of the central antipodal-block/corona-trace proof is documented. The detailed proof account is credited to Codex, and the source reports no human expert review; Few is the evidence-gap default.
Correction and publication history
The unconditional constructions answer two stated questions about traces on tracial completions.
Read this published revision