Research notebook: broader Erdős 625 revisions and experiments

[SamPetkov]

Summary

This remains a draft mathematical-review PR. It does not replace the canonical manuscript or publication PDFs.

The PR now has three purposes:

1. correct and split the concentrated Sections 7--9 replacement text after adversarial review;
2. replace the large-residual cycle-to-walk argument by a direct residual-restriction product bound;
3. record separately reviewed constant/profile extensions, with exact standard-library regression scripts.

Corrections made after PR review

The earlier monolithic appendix has been superseded. The corrected files now address four concrete defects or ambiguities:

• degree caps are explicit: the high-cell matching statement assumes every row and column degree is at most U; without this hypothesis it is false;
• the middle strip is finite: 3a/4 + O(1) is replaced by the exact typewise bound floor(3 min(u_i,u_j)/4);
• Section 8 uses dependent finite fibres: demand, labelled witness, and residual matching are a dependent disjoint union, and infeasible formal tuples enter only later as a nonnegative overcount;
• the square-sum step is one-sided off the matching: only the unrestricted square sum factorizes exactly.

Corrected proof appendices

• 625/proofs/PR27_SECTION7_CENTRAL_RATE.md and .tex
• 625/proofs/PR27_SECTION8_EXPOSURE.md and .tex
• 625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md and .tex
• 625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.md and .tex
• 625/PR27_VERIFICATION_REPORT.md
• 625/experiments/review27_verification.py

SECTIONS_7_9_REVIEW_REWRITE.{md,tex} now serves only as an index to these corrected files.

Main simplification

For an exposed matching M, restriction is injective on even edge sets:

F ↦ F \ M.

Therefore

Σ_F ∏_{e∈F\M} q_e ≤ ∏_{e∉M}(1+q_e) ≤ exp(Σ_{e∉M} q_e).

With the corrected off-matching square-sum inequality and the existing degree-moment estimate,

A(M,j) ≤ exp(C(U² + U⁴/m₀)).

Thus the large-residual branch costs only exp(O(N²)), rather than exp(O(N⁸)). The proposed proof no longer needs the simple-cycle decomposition, residual-walk enumeration, mixed matching-cycle encoding, parameter τ, or term hτ.

The two finite ingredients already have Lean counterparts: residualRestriction_injective and finiteInjectiveFamily_product_exp_bound. Their full probabilistic specialization is not claimed as formally complete.

Other review results

• central rate strengthened from Φ_T ≤ -(1-R)/5000 to Φ_T ≤ -(1-R)/100;
• direct propagation of equation (5.11) would improve the displayed coefficient by a factor four, pending line-by-line rounding/amplification review;
• exact rational four-support certificate:
  D₄(δ) < log(33/25) and log 2 - D₄(δ) > log(50/33);
• exact three-support first-moment certificate for {2,3,5}:
  D₃(δ) < log(391/200) and log 2 - D₃(δ) > log(400/391);
• complement-symmetric, fixed-density, and standard upper-bound consequences are recorded in the extensions note;
• the three-size profile and non-midpoint placement remain separate experimental routes until their full second-moment chains are replayed.

Exact regression coverage

Run:

python 625/experiments/review27_verification.py
python 625/experiments/entropy_certificate_upgrade.py

The first script passes:

• 3,809 bounded contingency tables;
• 5,880 labelled perfect matchings;
• 330 typed decoration fibres;
• 5,929 endpoint/near/middle classifications;
• 162 even-subgraph restriction instances;
• 263,967 off-matching square-sum instances;
• central-rate endpoint checks at 80-digit decimal precision.

The entropy script passes every exact Fraction assertion for the four- and three-support certificates. Its continuum scans are explicitly diagnostic only.

The standalone TeX appendices and verification report were compiled twice with pdflatex -halt-on-error; final logs had no unresolved references, overfull boxes, or underfull boxes. The Markdown files parse with Pandoc.

Review boundary

The finite tests do not prove the asymptotic theorem. Before canonical integration, independent review should still check:

1. labelled/unlabelled normalization in the exact Section 8 disintegration;
2. every factor in the global high-skeleton inequality;
3. finite-n translation of the entropy certificates uniformly through the phase;
4. direct propagation of (5.11) through rounding and amplification;
5. the literature-dependent corollaries.

The repository must continue to describe this as a candidate solution with a partial formalization, not an externally or fully formally verified resolution.

[SamPetkov]

Critical mathematical review (blocking canonical integration, but not the reviewer-guide concept):

1. Proposition 8.0 is false under its displayed hypotheses. It assumes only that the row and column degrees sum to (n), then uses that every degree is at most (U). The missing hypotheses are
   [
   orall a, s_ale U,qquad orall b, t_ble U.
   ]
   For example, with (U=4), (R_0=2), row margin (6), column margins (3,3), and table entries (3,3), both cells exceed (R_0) in the same row, so (M(r)) is not a matching. The intended four-size application does have the cap, but the proposition must state it.

2. Lemma 8.3C is not a finite theorem as written. Its domain contains (jle 3a/4+O(1)). Replace this with an exact integer/floor bound (for example, one derived explicitly for each (min{a,a-1,a-2,a-3})); then quantify the uniform constant in the subsequent estimate.

3. The load-bearing global Section VIII step remains asserted rather than proved. Lemma 8.3B gives no construction showing that forgetting temporary labels produces exactly the typed multinomial multiplicity. Lemma 8.3D does not show the conditional-law/expectation step from the pointwise majorant to the bare completion sum. Proposition 8.4 then invokes these assertions and says every multiplicity occurs exactly once, but supplies no partition/bijection or summation proof. Those are precisely the global bookkeeping obligations that independent review needs exposed. Please add the explicit finite maps, fibre cardinalities, and inequality chain, or relabel these as proof obligations rather than replacement proof text.

4. In Lemma 9.1C, the marked-edge strategy is mathematically consistent with the existing Lean finite-kernel theorem, but (P=Q+Q^2+cdots) should be defined with its convergent entrywise series (or replaced by the already formalized finite positive-walk kernel), and the canonical choice of orientation should be stated explicitly.

Positive findings: Lemma 7.1A and its numerical split check out; it agrees with the stronger kernel-checked scalar rate bound already in the repository. The simple-cycle product and the single (2|M|) mixed-cycle factor are also aligned with the current Lean modules.

Recommendation: keep the PR draft. The reviewer guide is useful. Until items 1–3 are repaired, retain the Sections 7–9 rewrite as an audit appendix/proposed decomposition and do not integrate it into the canonical manuscript or publication PDFs.

[SamPetkov]

Follow-up to the blocking review above:

1. Degree cap repaired. PR27_SECTION8_EXPOSURE.{md,tex} now assumes 0 <= s_a,t_b <= U explicitly. The finite checker retains the reviewer’s U=4, table (3,3) counterexample as a regression showing why the cap is necessary.

2. Middle strip made finite. PR27_SECTION8_HIGH_SKELETON_SUM.{md,tex} replaces 3a/4+O(1) by
   R₀ < r <= floor(3 min(u_i,u_j)/4) <= floor(3a/4)
   and displays the full logarithmic summand bound with the eventual universal choice c₀=1/8.

3. Global Section VIII maps exposed. The corrected files now state:

   • the dependent disjoint union over canonical demand, labelled witness, and witness-dependent residual fibre;
   • the exact aggregate incidence and residual mass cancellation;
   • the labelled-decoration map and fibre cardinality ell! / prod n_e!;
   • the cancellation with the endpoint-table factorial;
   • an injective endpoint/near/middle encoding;
   • the conditional expectation chain in the small-residual branch;
   • the precise point at which infeasible formal tuples are admitted as a nonnegative overcount.

4. Cycle route removed rather than patched. PR27_SECTION9_RESIDUAL_RESTRICTION.{md,tex} replaces Lemma 9.1C entirely. Restriction F -> F \ M is injective on even edge sets, so the even-family sum is bounded directly by a subset product. The corrected argument also fixes the off-matching square-sum statement: it is an inequality against the unrestricted factorized sum, not an equality.

The stale monolithic rewrite is now only an index to the corrected split appendices. PR27_VERIFICATION_REPORT.md records the exact regression scope. review27_verification.py passes 3,809 bounded tables, 5,880 labelled matchings, 330 decoration fibres, 5,929 middle-strip cases, 162 restriction instances, and 263,967 square-sum instances.

I am keeping the PR in draft. These repairs address the stated finite/formal defects, but the global asymptotic specialization and labelled/unlabelled normalization still warrant independent line-by-line review before canonical integration.

[SamPetkov]

A second super-check is now isolated in clean draft PR #30: #30

PR #30 starts from current main and contains only the two claims that survived the stricter review without depending on the unresolved Section 8 globalization or the proposed constant/profile extensions:

• the exact Section 7 rate Phi_T <= -(1-R)/100;
• the Section 9 residual-restriction product bound, yielding A(M,j) <= exp(C(U^2+U^4/m_0)) = exp(O(N^2)) in the large-residual regime.

Its exact checker exhausts 5,912 residual relations, 12,561 even edge sets, and 613,711 square-sum instances, and certifies the logarithm endpoint signs with rational atanh-series bounds. PR #27 remains the broader draft research notebook; PR #30 is the narrower reviewable result.

[SamPetkov]

Review organization update:

• PR Research notebook: broader Erdős 625 revisions and experiments #27 remains the broad research notebook. It contains corrected Section 8 appendices, entropy/profile experiments, and literature-dependent consequences, but it should not be treated as the next canonical-integration PR.
• PR Isolate verified Section 7 and Section 9 simplifications #30 isolates the independently super-checked Section 7 central-rate improvement and Section 9 residual-restriction simplification. Its focused CI is green and it is now ready for review.
• PR Verify factor-four root-gap constant propagation #31 isolates the factor-four propagation from equation (5.11) through midpoint rounding and amplification. It adds a separate proof note, audit, exact rounding checker, phase diagnostic, and focused workflow.

This split is intentional: reviewers can assess #30 and #31 without accepting the more speculative Section 8, new-support, non-midpoint, or literature-dependent material collected here.

[SamPetkov]

A second narrow extraction is now available as PR #32. It replaces the notebook's preliminary D_4 < log(33/25) certificate by a stronger exact Fraction certificate:

D_4(delta) < log(639/500) and log 2 - D_4(delta) > log(1000/639).

PR #32 contains only the four-support certificate, its audit, checker, and focused workflow. The three-size and non-midpoint experiments remain here in the research notebook.

[SamPetkov]

Additional support-search diagnostic: I exhaustively scanned supports containing deficits 2,3 inside {2,...,8} on a 401-point phase grid. Among supports of size at most five, {2,3,4,5,6} had the largest scanned minimum advantage (~0.525995), but this is only about 1% above {2,3,4,5} (~0.520701) while increasing the transportation dimension. The three-size support {2,3,5} remained positive (~0.092145) but much weaker. This suggests the canonical four-size support is close to the practical Pareto frontier: adding deficit 6 buys little, while removing deficit 4 loses substantial entropy advantage. Diagnostic only; no new PR is proposed for support replacement.

[SamPetkov]

Coordination update: the current review sequence, dependency graph, coefficient ledger, integration order, and support-frontier diagnostic are now collected in PR #33. This PR remains the broad research notebook; the focused claims intended for independent review are isolated in #30, #31, and #32.