Audit the full Erdős 625 proof stack and isolate reusable results

[SamPetkov]

Purpose

This is the cumulative theorem-by-theorem and lemma-by-lemma audit of the Erdős 625 candidate proof and its public PR stack. It is stacked on PR #38 and now also contains the verified Section IX line from PRs #34, #35, and #37, merged mechanically through PR #40.

The branch is intentionally a draft review frontier. It does not claim that Erdos625Statement is proved.

What is included

Full logical audit

• 625/audits/FULL_THEOREM_LEMMA_AUDIT_2026-07-25.md
  • dependency graph for the full manuscript;
  • theorem/lemma classifications: green, finite-green, amber, blocked, improvable;
  • exact audit of PRs Research notebook: broader Erdős 625 revisions and experiments #27 and Isolate verified Section 7 and Section 9 simplifications #30–Audit the full Erdős 625 proof stack and isolate reusable results #39;
  • submission-grade acceptance checklist.
• 625/audits/POST_INTEGRATION_STATUS_2026-07-25.md
  • authoritative status after repairing and integrating Section IX;
  • corrected Section VIII parameterization and CI interpretation.

Section VIII global bridge

• 625/proofs/SECTION8_GLOBAL_DECORATION_BRIDGE.md
  • exact decomposition by endpoint block pairing, deficit choice, and per-cell partial stub matching;
  • explicit warning that a partial physical matching does not have a unique full completion;
  • exact aggregate one-cell ratio

    R_{m,d}(h)
      = C(m,h)/((d+1)...(d+h)) * 2^(-hm+h(h+1)/2);
    

  • global falling-factorial ratio

    (n)_{J+H}/(n)_J = (n-J)_H <= n^H;
    

  • geometric fibre sum and the bare-skeleton exponent

    O(n^(2/3) log(n)^(4/3)) + O(sqrt(n log n))
      = o(n/log(n)^4).
    

Repaired and integrated Section IX

The q-only branch now controls the literal attained attachment sum, not a surrogate law. The focused target is green at commit 2ea82c988218dee89d3639f598090ce813501c40.

The exact chain is:

1. normalized signed-profile second moment = attained canonical attachment sum;
2. pointwise literal attachment factors from the exact mixture;
3. the q-only two-regime theorem gives

   AttachmentSum
     <= BareSkeletonSum * exp(epsilon_n * n/log(n)^4),
   epsilon_n -> 0.
   

4. Section9QOnlySecondMomentFrontier.lean composes this with a single explicit Section VIII bare-skeleton hypothesis.

Section IX is therefore no longer an independent bottleneck. The decisive remaining formal input is the Section VIII bare-skeleton estimate.

Stronger results and follow-up directions

• 625/proofs/TRANSFERABLE_RESULTS_AND_COROLLARIES_2026-07-25.md
  • phase-resolved main coefficient;
  • stronger certified uniform constant;
  • simultaneous graph/complement corollary;
  • balanced-sign seed;
  • matching-restriction theorem for weighted even subgraphs;
  • exact signed-partition cycle-space factor;
  • abstract rare-seed amplifier;
  • aggregate matching-decoration transfer principle;
  • general-p and finite-support follow-up directions.

Exact regression layer

• 625/experiments/full_proof_audit_regression.py
  • midpoint rounding;
  • balanced central-binomial loss;
  • matching-restriction injection and weighted product bound;
  • all-high two-thirds exponent budget;
  • exact local high-deficit aggregate ratio;
  • global falling-factorial ratio;
  • global aggregate decoration product comparison;
  • geometric deficit-fibre sum;
  • coefficient propagation and asymptotic scale checks.

Main mathematical verdict

Sections 2–7 and 10, together with the final event intersection, are structurally coherent. The repaired Section IX route supplies the required literal attained attachment estimate.

The proof frontier is now concentrated in one global Section VIII theorem, with four explicit interfaces:

1. identify every attained canonical high physical skeleton as an endpoint block pairing, allowed cell deficits, and per-cell partial stub matchings;
2. sum the partial physical fibres and prove the aggregate bare-weight comparison, including the single global denominator ratio;
3. identify the aggregate full-reference block-pairing weights with the exact endpoint table sum sum_L fourEndpointW(L);
4. combine endpoint AM–GM/multinomial transport and the all-deficit fibre sum at the actual midpoint profile.

The corrected paper-level aggregate bridge is written in this PR. The corresponding global Lean assembly is not yet present. Proposition 9.2 and the final Erdős 625 theorem must remain conditional until that assembly is checked.

Stronger main theorem available after closure

The audit supports the phase-resolved coefficient

(ln 2)^2/8 * (ln 2 - D_4(delta_n))

and, combining PRs #31 and #32 with an explicit compact uniform-slack lemma, the certified uniform coefficient

(ln 2)^2/8 * ln(1000/639)
  = 0.026896409808379...

This is about 6.687 times the coefficient printed in the canonical manuscript. These improvements do not alter the second-moment architecture, but remain conditional on completing it.

Validation and scope

The focused q-only source branch has a recorded green run. The cumulative head reruns:

• root Lean;
• focused Section VIII simplification;
• the exact q-only normalized-second-moment frontier;
• matching-restriction product and envelope;
• focused q-only attachment;
• exact Python audit under normal and optimized execution.

A green root build alone is not sufficient when a new module is outside the root aggregate; the focused jobs are load-bearing. Keep this PR draft until all checks are green on the exact cumulative head and the global Section VIII theorem is formalized.

Review order

1. Read POST_INTEGRATION_STATUS_2026-07-25.md for the current verdict.
2. Review SECTION8_GLOBAL_DECORATION_BRIDGE.md adversarially, especially the aggregate physical-fibre parameterization.
3. Check the exact regression output.
4. Review the theorem-by-theorem audit and reusable-results dossier.
5. Formalize the four-interface Section VIII assembly before rewriting the canonical manuscript.