Prove Q26 has no thirteen-queen dominator

[jkolantree]

What changed

• add a pinned Lean 4.32.1/mathlib project proving that no 13-element queen set dominates the 26 by 26 board
• formalize the unrestricted 36-shadow classification, bichromatic closure, and monochromatic threshold-shell closure
• add a self-contained proof note and a tiny exact arithmetic checker with focused tests

Why

The earlier five-profile route remained conditional on a structural bridge. This proof derives the actual unrestricted parity shadow from board semantics and closes both exhaustive branches in Lean.

The main theorem is:

theorem no_thirteen_queen_dominator :
    ¬ ∃ queens : Finset Square, Dominates queens ∧ queens.card = 13

Validation

• pinned lake build: 8,679/8,679
• lake env lean Q26GridAnnihilator/AxiomAudit.lean
• lake env leanchecker Q26GridAnnihilator.Unconditional
• standalone checker tests: 10/10
• checker CLI: PASS ... root_cnf=UNKNOWN_UNCHANGED
• publication scan: no sorry, admit, project-defined axioms, native_decide, generated caches, secrets, or private absolute paths

The final theorem prints only Lean's standard [propext, Classical.choice, Quot.sound] axioms.

Evidence boundary

This PR establishes the mathematical exact-cardinality theorem in Lean. The separate unrestricted root-CNF proof receipt remains UNKNOWN after solver timeout; this PR does not claim an LRAT/DRAT replay or promote that receipt.

[jkolantree]

Important validation correction: this historical PR used Lean 4.32.1, whose trust base was later found to require the kernel soundness fix in Lean 4.32.2. The formal sources are not alleged to have exploited that defect, but the 4.32.1 validation should not be treated as the current trust receipt. Follow-up PR #19 upgrades the project to Lean/mathlib 4.32.2, adds public patched-kernel CI, and publishes a pinned Comparator run accepted by both Lean 4.32.2 and the independently implemented nanoda kernel. The exact root-CNF certificate track remains UNKNOWN.

[jkolantree]

Final supersession status: follow-up PR #19 is now merged into public main at commit 467b623. Post-merge Verify release run 31550096829 passed all jobs on that exact commit, including the Lean 4.32.2 proof build, patched-kernel replay, and axiom audit. The public Comparator/nanoda receipt in PR #19 is the current external-checking evidence. The exact root-CNF certificate track remains UNKNOWN_UNCHANGED.