Document the Erdős 625 review sequence and support frontier

[SamPetkov]

Summary

This PR adds a single coordination record for the current Erdős 625 review sequence and a reproducible numerical support-frontier experiment.

It does not modify the canonical manuscript, generated TeX, PDFs, Lean sources, theorem statement, or any proof PR.

Files

• 625/REVIEW_SEQUENCE_ROADMAP.md
• 625/experiments/support_frontier_scan.py
• .github/workflows/erdos625-review-roadmap.yml

Review roadmap

The roadmap records the intended roles and dependencies of the open review PRs:

• Research notebook: broader Erdős 625 revisions and experiments #27: broad research notebook; keep draft;
• Isolate verified Section 7 and Section 9 simplifications #30: focused Section 7/9 simplifications;
• Verify factor-four root-gap constant propagation #31: factor-four root-gap constant propagation, conditional on canonical inputs;
• Certify a stronger four-support entropy advantage #32: stronger exact four-support entropy certificate.

It also records the recommended integration order and the remaining highest-priority boundary: the exact global Section 8 labelled/unlabelled high-skeleton summation.

Coefficient ledger

The note keeps the constant implications separate:

canonical:                 (ln 2)^2 ln(200/153) / 32
PR #31 only:               (ln 2)^2 ln(200/153) / 8
PR #32 only:               (ln 2)^2 ln(1000/639) / 32
PR #31 + PR #32:           (ln 2)^2 ln(1000/639) / 8

The combined candidate coefficient is 0.026896409808379..., but the roadmap explicitly does not request a canonical theorem change before the corresponding reviews are accepted.

Support-frontier experiment

The diagnostic script scans all supports of size three through five that:

• contain deficits {2,3};
• are contained in {2,...,8};
• span the complete target interval.

It evaluates the limiting advantage on a 1001-point phase grid and compares full-support cutoffs 80 and 100.

Selected output:

{2,3,4,5,6}:  0.525994631053
{2,3,4,5}:    0.520701335491
{2,3,4,6,7}:  0.399733765460
{2,3,5}:      0.092144964328

Adding deficit 6 improves the scanned advantage by only about 1.017% while increasing the dense transportation dimension from 4x4 to 5x5. The experiment therefore supports retaining the canonical four-size profile as the practical complexity/advantage frontier.

This scan is explicitly diagnostic, not a proof or a support-replacement theorem.

Validation

The focused workflow runs:

• python -m py_compile;
• the full 1001-point scan;
• an optimization-independent run under python -O.

The script uses explicit exceptions rather than assert for its regression gates.

[SamPetkov]

Roadmap update: PR #34 (Kernel-check the Section 9 matching-restriction product bound) is the formalization follow-up to PR #30. It should be reviewed after #30 and before any attempt to retire the older cycle/traversal route from the canonical proof. It is intentionally limited to the finite algebraic endpoint and does not yet prove the analytic O(U^2+U^4/m_0) envelope or the tagged attachment expectation.

[SamPetkov]

Review-sequence update:

• Kernel-check the Section 9 matching-restriction product bound #34 now kernel-checks the direct Section 9 matching-restriction product and is ready for review after focused, full, generated-source, self-contained, and publication checks passed.
• Integrate the direct Section 9 attachment and log-square envelope #35 is the stacked integration PR. It carries the direct product through the literal attachment numerator, canonical attained profile skeleton, and the target exp(O((log n)^2)) large-residual endpoint. It remains draft while its final focused/full Lean gates run.
• Kernel-check the Section 8 endpoint transport core #36 kernel-checks the square-root-free endpoint transportation core beneath manuscript (8.8). Its focused, full, generated-source, self-contained, and publication checks pass, and it is ready for review.

The remaining principal mathematical boundary is now narrower: the later Section VIII margin/Cauchy summation and near/middle high-cell globalization, followed by one two-regime profile assembly using #35.