An honest attempt that didn't land — here's what I learned

Verdict: PARTIAL. Nothing we checked breaks it. Every part of the upper bound except the largest stratum we have now re-proved from scratch, with our own encoding and two solvers, without reading any of your formulas. The largest stratum (one degree-8 vertex) we re-derived by hand down to exactly your 13,351 cells, and sampled: your orbit CNFs re-solved with a different solver family, and our own encoding of a sample of cells, including the 25 that were hardest for you. If the external certificate checks are right, this is a new exact value, R(C₄, K₁,₄₂) = 49, equivalently f(49) = 7, and the first strict drop of f known: f is 8, 7, 8 at n = 48, 49, 50 (f(50) = 8 from the Hoffman–Singleton graph). "Partial" describes what we could re-run, not a flaw: the H1 stratum rests on about 28 TB of LRAT checked by cake_lpr outside Lean, and we re-checked a random sample of it, not the whole.

The statement. We read the Lean definitions: containsC4 is an injective copy of the 4-cycle, minDegreeForC4 is the problem's f, and ¬ C4FreeMinDegreeWitness 49 7 is exactly f(49) ≤ 7. Both hypotheses of the capstone (hOne, hSeven) are semantic unsatisfiability statements about fixed, non-empty formula lists (hOne's structure also carries a well-formedness field, gap 2 below); neither can be met trivially (soundness of the symmetry breaking is proved for every depth). Your Lean theorems are conditional on these two hypotheses, as your FiniteDropCapstone says, and you discharge them outside Lean with cake_lpr: hOne is the H1 stratum, hSeven the H7 t = 0 covers and leaves. What we report below about H1 and H7 t = 0 is evidence for those two hypotheses (for H7 t = 0, an independent proof of the same stratum in our own encoding, not a check of your covers and leaves), not a Lean proof of them.

What we re-ran or re-derived (our code unless noted):

• Lower sides, two instruments (edge-list codegrees; adjacency matrix with A² ≤ 1 off the diagonal): Boza's 48-vertex graph is 7-regular and C₄-free; the 49-vertex graph has minimum degree 6 and is C₄-free. Adding an edge between two vertices at distance 2 is rejected (by the matrix instrument on both graphs, by the edge-list instrument on the 48-vertex graph).
• The case split, by hand: every degree is 7 or 8; high vertices are pairwise non-adjacent with exactly one common neighbour; counting high–low incidences (n₁ + 2n₂ + 3n₃ = 8h, n₂ + 3n₃ = C(h,2)) leaves h ∈ {1,3,5,7,9}; for h = 7 it gives the (7−t, 14+3t, 21−3t) split you state.
• Every stratum except H1, from scratch (our normaliser and encoder; nothing of yours read). Beyond the obvious constraints we add one observation: for a degree-8 vertex x the 48 non-returning two-walks out of x end at 48 distinct vertices, i.e. at every other vertex, so every vertex other than x has exactly one neighbour in N(x). C4-freeness gives "at most one"; the "at least one" clauses are a pigeonhole fact a CDCL solver cannot rediscover cheaply. Add lex-leader symmetry breaking on interchangeable low vertices, and every cell falls fast: H3 (2 cells, 176–377 s), H5 (3 cells, 69–622 s), H7 with t ≥ 1 (all 13 representatives, 26–2,625 s), H9 (all 20 classes, 23–52 s) under Kissat; H7 with t = 0 in 336 s when we also break the symmetries of the seven high vertices (transpositions that preserve the high–low incidence). Without that last step the t = 0 cell was still open at our 2-hour cap, so that one result depends on it; its soundness is covered below. Your route for H7 t = 0 used 377,776 leaves and about 4,300 solver CPU-hours. Certificates: CaDiCaL wrote DRAT proofs and drat-trim verified every one: 19/19 for H3/H5/H7 and 20/20 for H9. Two of the nineteen, H7 t = 0 and H7 t = 1 representative 0, are proofs for the encoding with the high-vertex symmetry break (for t = 1 rep 0 the plain encoding also came back UNSAT, in 2,625 s under Kissat, without a proof). A negative control (the same proof checked against the formula with exactly the 220 "at least one" clauses removed) is rejected. Controls on the encoding: brute-force soundness of each kind of symmetry breaking on small instances, with mutations caught; the PG(2,q) polarity graphs ER(5) and ER(7), where the same saturation holds, lex-descended and accepted by the full formula at production scale (up to 6 highs and 719 high permutations) while the raw graph is rejected; ER(3) exhaustively; and a separately briefed hostile referee seat that read the encoder and found it sound. This also covers your trust-base gap for these strata: H3, H5, H9 and the H7 t ≥ 1 certificate replays no longer rest only on compiled native_decide code.
• H1, by hand, and your inventory. Our own derivation of H1's structure lands exactly on your decomposition. With x the degree-8 vertex, the 40 vertices outside N[x] split into 8 blocks of 5 in 4 pairs; each of them misses exactly one of its 7 available blocks, so between two non-paired blocks X, Y the edges form a matching of size 5 − M[X][Y], where M[X][Y] counts the vertices of X missing Y. That makes M symmetric, with row sums twice the internal edge counts, and counting pairs with no common neighbour gives M[X'][Y] + M[X][Y'] ≤ 5. Without that last inequality, enumerating M up to the symmetries of each internal-edge pattern gives exactly your five tables (449,358 / 169,668 / 70,070 / 31,512 / 16,692 labelled, 1,536 / 3,662 / 4,801 / 2,700 / 842 orbits); with it, exactly your 13,351. Row by row as well: your highBranchMissCount is our M, your capacity inequality is ours by symmetry, and after relabelling your profiles our 13,351 classes equal your kept inventory as sets, with your 190 removed rows exactly the ones the inequality rejects. So the H1 inventory and its completeness, which your Lean proves (CapacityCover), also follow from a short counting argument outside Lean. Encoding one cell with the block structure, the exact cross-block counts and a pigeonhole consequence ("every vertex has a neighbour that misses the block paired with the one it misses"), a sample of 26 cells, 5 or 6 from each of the five cases (seeded, but for four of the cases drawn from a prefix of the enumeration rather than uniformly), was UNSAT under Kissat in 19 to 167 seconds each (one solver, no proof), against 142 to 13,660 seconds for your orbit CNFs under CaDiCaL on the same box. We also took the 25 orbits that were hardest for you (your census set ranked by CaDiCaL time, 34,000 to 71,000 seconds each, plus the orbit you call the hardest and had to split), mapped each to its cell in our encoding, and ran those: all 25 UNSAT under Kissat, in 60 to 723 seconds (median 159). The orbit with your longest census solve (71,098 seconds) took us 88. With the C₄ clauses removed, the three hardest are satisfiable and the models pass our structural recheck, so the encoding is not vacuous on them. We have not run all 13,351: about 200 to 255 Kissat CPU-hours by these two samples, and on the order of 300 more to produce and check DRAT proofs. That is a few days of our whole machine, and we have not scheduled it.
• H7 with t = 0, your artefacts: the 28 base cubes from your EmitCube.lean, built by us, equal the hashes in inputs.json; the 28 cover CNFs (our assembly) equal your receipt hashes and are UNSAT under Kissat; and regenerating the leaves from our own compiled build gives your 377,776 leaves, with each cube's leaf stream hash-equal to yours (28/28). All 893 leaves of one whole cube (F6_t14) and 199 more drawn uniformly from the other cubes (seed 20261019; the 200th draw fell inside F6_t14) hash-match your receipts and are UNSAT under Kissat: 1,092 of 1,092.
• H1, your artefacts: a uniform random sample of 12 of the 13,351 orbits (seed 20261019), emitted with your emitter on our build. Every CNF hash equals your receipt. Eleven of the twelve are UNSAT under the other solver family (CaDiCaL where yours used Kissat), in 142 to 13,660 seconds each on our box; the twelfth, census orbit aa3d5ed34629207c, was still undecided when our 4-hour Kissat cap ran out (not a disagreement, just not re-solved). On the two CNFs we inspected byte for byte, the clause count equals the header and no line is malformed. The emitter comment about "duplicated trailing bytes" describes a failure that would show up as exactly that kind of mismatch. Each file does repeat 223,490 clauses verbatim (the same number in both), which is harmless for satisfiability but worth a sentence.
• The Lean reduction: we rebuilt your project cold, module by module, with your pinned Lean 4.31.0 and Mathlib, using our own build driver rather than lake. 883 of your 893 modules compiled without error, and every .olean they produced is byte-identical to the object recorded in your accepted cold build (RUN.json), so our replay checked exactly your objects: the kernel on our machine, plus the same compiled native_decide evaluations your build trusts. (Two modules, T0CanonicalCnfSatisfaction and T0CanonicalCnfDegreeWitness, needed more than the 16 GB memory flag we first gave them; they passed uncapped at 22.8 and 19.1 GB, as yours did.) The largest module, T1Rep0Certificate, which checks the 1.6 GB certificate for H7 t = 1 representative 0 by native_decide, cannot be built on our machine: the machine is shared, and the build was stopped by the out-of-memory killer at about 28 GB after 2.9 hours, roughly 40% of the way (yours took 7,831 s in a 110 GiB container). The nine modules downstream of it, up to the capstones, wait on it, so for that module we did two things instead.
• That one certificate, checked outside Lean: we wrote our own decoder (from your Lean decoder and the binary LRAT format). The text proof it produces hashes to the compact_lrat_sha256 in your module header, so it is your certificate byte for byte (likewise on the small t = 7 certificate). We checked it against the CNF rendered from your Lean definition orderFortyNineGeneratedH7SatCnf (representativeMasks 1 0); our renderer checks at run time that the clauses it writes map clause for clause onto that definition. Two checkers accept it: cake_lpr, the CakeML-verified checker your own kit uses (759 seconds), and a strict RUP checker written independently by our referee seat with its own unpacker and zstd's LZ4 decoder (72 s; it requires every step, including the final empty clause, to reach a real conflict). Controls, on your full certificate: dropping the last hint of the final empty clause, dropping one hint deep in the proof, and flipping a literal in a clause the first step cites are each rejected by the strict checker, at exactly the mutated step; cake_lpr rejects the cited-clause flip at the first step and the final-clause drop at the final step. On the small t = 7 certificate the same three mutations are rejected by both checkers. Under cake_lpr, all 13 of your H7 t ≥ 1 certificates verify (the other twelve were also checked by our Lean replay). We first ran drat-trim's lrat-check; our referee showed that it accepts a final empty clause whose hints never reach a conflict (it prints VERIFIED on a satisfiable two-literal formula, a known open issue upstream, drat-trim #42 and #43), so none of this rests on it.
• The capstones, built over that one substitution: we replaced that module with a stub that derives its single exported theorem from one named axiom stating exactly what those two checkers establish (that CNF is unsatisfiable), built the nine downstream modules on top, and printed the axioms of your three headline theorems: 601, 607 and 604, your audit's counts, and the same sets as your recorded lists except for one swap each (your native_decide axiom for this certificate, our named axiom). No sorry, nothing else assumed. So the reduction composes as stated, and every module's content has now been checked on our side, by our Lean replay or, for that one certificate, by external checkers.
• A separate account. Your fetch script worked from an unrelated AWS account (ours), so the limitation in ACCEPTED.md ("access from a separate AWS account is still untested") is now tested.
• Hostile referee on the submission (a separately briefed seat with tools, told to refute): holds with gaps, nothing fatal. It recomputed the H1 orbit structure from the definitions without Lean (orbits per profile 1,536 / 3,662 / 4,801 / 2,700 / 842, each inventory row hitting its orbit exactly once) and found that the 13,351 receipts equal the capacity-filtered inventory as a set, profiles included. Further referee seats attacked our own instruments (the from-scratch encoding: sound as read; the two H1 reductions: holds with fixes, all applied), and one, today, attacked the T1Rep0 external check. It found the lrat-check hole described above and confirmed the rest: the one-axiom swap, the byte-identity of the decoded certificate, and that every module has now been checked one way or the other.

Gaps worth closing (none changes the verdict; on 20 October the authors wrote that items 1–6 will go into a new version of the Zenodo record, and item 6 is closed below):

1. The emitter comment in Erdos85OneHighV2CnfEmit.lean records an undiagnosed wrong-output bug in compiled code ("duplicated trailing bytes in the native executable"), worked around by chunked printing and not mentioned in the paper. Our from-scratch proofs now cover every stratum that runs through native_decide except H1, and H1 goes through that emitter, so it deserves a sentence and ideally a diagnosis.
2. OneHighFamilyV2CheckedUnsat also carries a nonzero field (no literal 0) that no Lean proof discharges; one native_decide over the inventory would.
3. The 96 historical H1 orbits were checked from archived sweep CNFs with no v2cnf regeneration on record, and the manifest their expected hashes come from (9d04a66c…) is not in the bundle. Our sample's historical orbit (b953a73b0e372480), re-emitted, matches.
4. For the hardest orbit, five of the 36 leaf receipts in pilot_h1_81494a_leaf_solves.jsonl (nodes 54, 61, 64, 65, 70) have no cube_sha_ok field, and the per-leaf expected hashes aren't published.
5. cake_lpr exits 0 on failure, so the scripts that read its output are load-bearing; they're on GitHub at 2029149d7e42 but not in the Zenodo deposit.
6. Closed on 21 October. The CNF our renderer writes from your Lean definitions did not have the source_cnf_sha256 in your module headers, for any of the 13 H7 t ≥ 1 representatives. Your explanation (20 October): those hashes are of the DIMACS your Python encoder wrote through pysat, whose variable pool numbers the edge variables by first use, while the Lean definition numbers them lexicographically; same clauses, same order. We tested that directly. Renaming the edge variables of our own Lean rendering by first use moves 307 of the 1,176 (all of them in the 315 leading unit clauses) and reproduces your header hash for all 13 representatives; the same check fails on a mutated CNF and against another representative's header. The renumbered hashes you sent for t = 1 rep 0 and t = 7 rep 0 equal our renderings byte for byte. The generator script is on GitHub (tag erdos85-paper-v1) but not in the Zenodo deposit.

One suggestion. For the strata you certified through LRAT, two structural additions did most of our work: the "exactly one neighbour in N(x)" clauses at a degree-8 vertex (they took your most expensive H7 cell to minutes), and for H1 the exact cross-block counts per cell plus the pigeonhole clause above. If you ever re-certify H1, the per-cell cost may drop by one to two orders of magnitude. Our encoders are in the bundle (fs/, h1k/, h1m/).

Novelty. Boza's current arXiv version (2409.12770v2, updated 12 June 2026, checked on 20 October) leaves r(42) ∈ {49, 50} (v1's source has "≤ 50"); OEIS A006672 stops at n = 38; erdosproblems.com/85 has no proof claims (checked again on 20 October), and Stijn Cambie's 17 September comment there calls f(49) "tough". We found no earlier determination.

Not checked: the H1 LRAT as a whole, the bank proofs themselves, cake_lpr itself, and the T1Rep0 module inside Lean on our machine (checked outside Lean instead, as above). Files: verification/85/reader-drop-at-49 (the repository is private at the time of writing; files are available on request).