superperm5889 v1.0 — Unconditional Lean proof of S(7) >= 5889

Verification

• Headline theorem: Ssuper7_ge_5889 : 5889 ≤ Hunter.Ssuper 7
• The proof is unconditional.
• lake build succeeds.
• lake build AxiomCheck5889 succeeds.
• The source contains no sorry, admit, or user-defined axioms.
• Finite certificate checks use the explicitly documented native_decide trust path.
• Reproduction instructions are in REPRODUCE.md.
• A proof overview is in PROOF_OVERVIEW.md.