A Drop at Forty-Nine in Erdős Problem 85

For n ≥ 4 let f(n) be the least d such that every simple graph on n vertices with minimum degree at least d contains a four-cycle. Erdős Problem 85 asks whether f is eventually nondecreasing. We report two results. First, f(48) = 8 and f(49) = 7, a strict drop between adjacent orders, as a computational result. The lower sides are explicit graphs checked in Lean 4 through native_decide. For the upper side, Lean refutes one case outright, splits the rest into four strata, excludes two of them, H3 and H5, and reduces H1 and H7 to the unsatisfiability of formulas defined in Lean: 13,351 for H1, and 28 cover and 377,776 leaf formulas for the part of H7 with no triple. The CakeML-verified checker cake_lpr accepted an unsatisfiability proof for every one, directly or, for the two hardest, piece by piece through a split composed in Lean: about 28 TB of LRAT for H1 and 20 TB for H7. Lean thus derives the upper side from two explicit unsatisfiability hypotheses, which the external checks support but which are not admitted into Lean; the derivation prints 598 native_decide axioms beyond the three standard ones, and each checked file is tied to its Lean formula by emitters, not a kernel proof. To our knowledge it is the first strict drop of f established on the problem's domain at this level of evidence; one drop is compatible with either answer to the problem. Second, Lean verifies from the standard axioms alone that one proposition, A-REG (for no k ≥ 3 is there a C4-free 2^k-regular graph on 4^k vertices), implies a negative answer to Erdős Problem 85. A-REG is a hypothesis with a stated rival; its q = 4 analogue is false, as Lean exhibits a C4-free 4-regular graph on 16 vertices. Data and checkers. H1 checker: public AMI ami-05697724475f2e748 (us-east-1, erdos85-h1-checker-20261006); proofs and checker kit in the Requester Pays S3 bucket 2am-erdos85-certs under public/erdos85-h1-checker-kit/ and sat49/campaign-20260825/h1/ (the 12,094 bank proofs); guide CHECKING.md in the receipts bundle. H7 certificates: the thirteen packed files read by the Lean build (about 2.57 GB) are in the same bucket under public/erdos85-h7-positive-triple-lrat/ (Requester Pays); proofs/scripts/fetch-h7-certificates.sh downloads them and checks them against proofs/Proofs/Certificates/strata-lrat.MANIFEST.sha256. Lean sources and all receipts: GitHub release erdos85-paper-v1. Receipts bundle sha256: 54f08629ca9d229f08a25ec34c6e48ddaed6d7f65aab6cc235233cc920567aae.