formalist(OPE-6): n-queens namesake theorem, zero sorry (supersedes #4)

[agentforce314]

OPE-6 (Formalist). Lean 4 + Mathlib proof of the n-queens namesake theorem, zero sorry. Supersedes PR #4 (branch is built on ope/4-nqueens-statement-pin; this PR contains PR #4's statement pin plus the proof, so #4 can be closed unmerged).

Status: known-classical, formalize-only, no novelty claim. Do not merge — board merges after Adversarial Reviewer (OPE-7) sign-off. catalog/, docs/PROBLEM_LEDGER.md, STATEMENT.md deliberately untouched per Director instruction.

What is proved (proofs/lean-project/ProofLab/NQueensTheorem.lean)

theorem queens_exists_of_four_le (n : ℕ) (hn : 4 ≤ n) : ∃ q : Fin n → Fin n, NonAttacking q
theorem n_queens_exists_iff (n : ℕ) : (∃ q : Fin n → Fin n, NonAttacking q) ↔ (n ≠ 2 ∧ n ≠ 3)

def NonAttacking and both theorem statements are byte-identical to the OPE-4 pin (checked by diff of the extracted blocks).

Route (Attack Lead OPE-5, attacks/n-queens-20260912-180329/LOG.md)

• nonAttacking_of_nat — the only Fin lemma; everything else is ℕ → ℕ.
• GoodEven n f — bound / injective / anti-diag / main-diag / no fixed point.
• f₁ (n % 6 ∈ {0,4}), f₂ (n % 6 = 2, 8 ≤ n), each five lemmas by simp only [f]; split_ifs <;> omega.
• corner m g — odd boards m + 1 from a GoodEven m g; no_fix is used exactly in corner_main.
• n = 2, 3: unfold NonAttacking; decide on the function encoding (4 / 27 functions) — kernel handled it, no bridge to Level A needed. n = 0, 1: id.

Deviations from the LOG text (both arithmetic, both flagged in the file header)

1. f₂ pieces P3/P4 written 2 * r + 2 - n / 2 / 2 * r + 2 - 3 * (n / 2) instead of 2 * r - 3 * (n / 2) + 2: the latter truncates in ℕ when 2r ∈ {3h−2, 3h−1} (e.g. n = 14, r = 10). Python verifier used signed ints so never saw it. Values agree on every evaluated branch.
2. e2_no_fix takes 4 ≤ n: at n = 2 (h = 1) f₂ fixes both rows. Irrelevant to assembly (8 ≤ n there).

Gate output

lake build ProofLab.NQueensTheorem   → Build completed successfully. (0 × "declaration uses 'sorry'")
lake build ProofLab (root)           → Build completed successfully.
#print axioms n_queens_exists_iff        : [propext, Classical.choice, Quot.sound]
#print axioms queens_exists_of_four_le   : [propext, Quot.sound]
#print axioms nonAttacking_of_nat        : (none)
rg -n "sorry|admit" ProofLab/NQueensTheorem.lean → empty (exit 1)

Verify

export PATH="$HOME/.elan/bin:$PATH"; cd proofs/lean-project
lake build ProofLab.NQueensTheorem
rg -n "sorry|admit" ProofLab/NQueensTheorem.lean

Residual risks (for OPE-7)

• Mathematical: none known; the theorem is classical. The reviewer should confirm NonAttacking is the intended predicate (both diagonal families, n = 0 vacuous) — the proof is only as good as the pin.
• Engineering: omega closes every arithmetic case; decide on Fin 3 → Fin 3 compiles in seconds on Lean 4.10.0. Sanity examples check f₁ 4 = [1,3,0,2] and f₂ 8 = [3,5,7,1,6,0,2,4].

🤖 Generated with Claude Code