A computer-assisted proof that the maximum number of stable matchings of order seven is 85

Let f(n) be the maximum number of stable perfect matchings in a strict, complete stable-marriage instance with n participants on each side. This preprint assembles a computer-assisted mathematical proof that f(7)=85 from an explicit construction, structural bounds for rotation posets, and finite obstruction certificates. The construction has a direct ideal-cut stability proof and a short three-chain count. Participation bounds give at most 21 rotations; structural, deletion and neutral-core arguments handle the boundary and high-deficit layers. The remaining cases use local no-reentry arguments, decreasing fresh-partner graph budgets and complete geometric case covers. This deposit contains the English manuscript and the selected proof and reproduction dependencies: supplementary mathematical proofs, fixed numerical certificates and Python checkers, and a pinned source-only Lean companion. Historical validation records, build logs, diagnostic and alternative calculation collections are excluded. The 33 fixed calculation checks generate their prerequisite results afresh during each run; they do not enumerate all preference profiles. Exact Lean scope: the companion proves the unconditional actual-profile lower bound f(7)>=85, the fixed construction's 85-ideal event-poset count, and substantial abstract/local results with their explicit hypotheses. The universal upper bound over all actual preference profiles is not yet fully connected in Lean. This is a companion formalization, not an unconditional end-to-end Lean proof of f(7)=85. All 218 custom proof source modules belong to the build-target import closure and retain their R2 bytes. No new Lean kernel build is claimed by this packaging cleanup. The README files and CLAIM_MAP.json inside the ZIP explain exact formalization boundaries and reproduction commands. The computational checkers require Python 3.10+ without -O. The Lean companion uses Lean 4.27.0 and locked dependencies and supplies a source build and theorem/axiom audit driver for independent checking.