Complete and externally validate the exact Q26 result

[jkolantree]

Outcome

This follow-up completes the public Q26 result and fixes the broken GitHub equation rendering.

• Replaces all 32 \tag{...} display labels with GitHub-safe horizontal labels and makes \tag a tested forbidden command.
• Adds Q26GridAnnihilator.q26_domination_exact, proving directly that a 14-queen dominator exists and every dominator has cardinality at least 14.
• Kernel-checks the retained 14-queen witness inside Lean and derives the at-most-13 exclusion by finite padding from the unrestricted exact-13 theorem.
• Replaces the validation challenge with self-contained board, attack, and domination definitions.
• Freshly checks both named theorems with Lean 4.32.2 Comparator and the independent nanoda kernel.
• Preserves the separate exact root-CNF certificate track as UNKNOWN_UNCHANGED.

Validation

• Lean 4.32.2 direct source/object/root compilation: PASS
• Axiom audit: [propext, Classical.choice, Quot.sound]
• Comparator challenge build: 608/608
• Comparator solution build: 8676/8676
• Nanoda kernel: ACCEPTED
• Lean default kernel: ACCEPTED
• Comparator: Your solution is okay!
• Frozen 27-file Lean projection: 358f8fcdcea4ae5255f62cb399d57e9addafc8adc54e24f222ad3732a1c5b764
• Repository tests: 278 PASS, 1 environment-limited symlink skip
• Markdown tests: 38/38 PASS
• Q26 receipt tests: 12/12 PASS
• Manifest/inventory contexts: 167 files PASS across checkout, fresh clone, linked worktree, and Git archive

The external run took 922.842 seconds and peaked at 21.8 GB with no swap. The complete v2 receipt, transcripts, source projections, and pinned reproducer are included.