OPE-3: n-queens fresh Scout dossier + Level B statement pin (board-named)

[agentforce314]

Summary

• Fresh feasibility dossier for n-queens as a board-named, full-process run (parent OPE-2). Five readings disambiguated on docs/FEASIBILITY_RUBRIC.md: (a) existence iff n≠2,3 — 88, TARGET; (b) counting Q(n) 54; (c) Simkin asymptotics 28; (d) completion NP-complete 36; (e) toroidal Pólya 80 (different theorem, out of scope).
• Level B statement pin in catalog/problems/n-queens/STATEMENT.md: NonAttacking (q : Fin n → Fin n) = injective + both subtraction-free diagonal families; theorem n_queens_exists_iff (n : ℕ) : (∃ q, NonAttacking q) ↔ (n ≠ 2 ∧ n ≠ 3); n=0 convention stated; what-counts-as-done + out-of-scope list.
• Novelty pre-screen against the local Mathlib pin a719ba5c31 (v4.10.0): ZERO named n-queens theorem (commands + hit list in DOSSIER.json). Literature: Pauls 1874; Hoffman–Loessi–Moore 1969; Bernhardsson 1991; Bell–Stevens 2009. "Gauss 1850" corrected to the 8×8 count only.
• Catalog row → shortlisted (PR OPE-1424: n-queens Level A (n=2 none / n=3 none / n=4 [1,3,0,2]) Paul3435/open-math-lab#174 Level A history kept in tickets/artifacts/prior_art); ledger update block + table row; mathforge score n-queens run (problems/n-queens/feasibility.json).

Paperclip

• Issue: OPE-3 (parent OPE-2)
• Agent role: Scout

Math honesty

• Claim status: none. Known-classical theorem; formalize-only. No Lean opened, nothing solved.
• ProofLab/NQueens.lean (PR OPE-1424: n-queens Level A (n=2 none / n=3 none / n=4 [1,3,0,2]) Paul3435/open-math-lab#174) is cited as prior art / reusable encoding, not as a solution; the namesake was left residual there.
• Scout brute-force checked the transcribed Bernhardsson construction for n = 4..199 (0 failures) — a transcription sanity check, not a proof.
• Residual risks: R1 n=0 convention; R2 both diagonal families load-bearing, subtraction-free encoding equivalence to be reviewed; R3 1-indexed literature vs 0-indexed Fin + the n mod 6 ∈ {2,3} list surgery.

Test plan

• python3 test_mathforge.py -v — 11 tests OK
• python3 bin/mathforge status
• JSON parse of catalog/problems.json + DOSSIER.json
• (no Lean in this PR)

Board

• Please review + merge if OK
• Do not treat this PR as external publication of a proof