From 96e2f6b0ee4389bd96755927bbbf0e33a2b3c315 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 23:25:52 +0300 Subject: [PATCH 1/3] =?UTF-8?q?Add=20Erd=C5=91s=20625=20review=20sequence?= =?UTF-8?q?=20roadmap?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- 625/REVIEW_SEQUENCE_ROADMAP.md | 258 +++++++++++++++++++++++++++++++++ 1 file changed, 258 insertions(+) create mode 100644 625/REVIEW_SEQUENCE_ROADMAP.md diff --git a/625/REVIEW_SEQUENCE_ROADMAP.md b/625/REVIEW_SEQUENCE_ROADMAP.md new file mode 100644 index 00000000..9a9bd02f --- /dev/null +++ b/625/REVIEW_SEQUENCE_ROADMAP.md @@ -0,0 +1,258 @@ +# Erdős Problem 625 review sequence and integration roadmap + +**Snapshot:** 24 July 2026, based on `main` commit +`cda78922ea6c87bfc81f9bf693374dd045dac624`. + +**Status:** coordination and review record. This file is not a proof, external +peer review, a priority claim, or a completed formal verification. The +canonical manuscript remains a candidate solution and `Erdos625Statement` +remains unproved in Lean. + +## 1. Purpose + +A broad exploratory review originally accumulated in pull request #27. The +mature parts have now been separated into narrow pull requests so that each +claim can be reviewed, tested, and integrated independently. This file records +that separation, the dependency structure, the exact coefficient ledger, and +the recommended integration order. + +## 2. Pull-request map + +| PR | Role | Current classification | +|---|---|---| +| [#27](https://github.com/SamPetkov/Erdos/pull/27) | Broad revisions, Section 8 bookkeeping, alternative supports, non-midpoint placement, and corollaries | **Research notebook; keep draft** | +| [#30](https://github.com/SamPetkov/Erdos/pull/30) | Section 7 central-rate improvement and Section 9 residual-restriction simplification | **Focused result; ready for review** | +| [#31](https://github.com/SamPetkov/Erdos/pull/31) | Propagation of the phase-resolved root displacement through midpoint rounding and amplification | **Focused conditional result; ready for review** | +| [#32](https://github.com/SamPetkov/Erdos/pull/32) | Stronger exact four-support entropy certificate | **Focused conditional result; ready for review** | + +The narrower PRs were created directly from the then-current `main`; they do +not depend on the branch history of #27. + +## 3. Result isolated in PR #30 + +### 3.1 Central partial-diagonal rate + +On the same domain as the central range of Lemma 7.1, + +\[ + \Phi_T(z)\le -\frac{1-R}{100} + \qquad\left(\frac1{64}\le R\le1\right), +\] + +improving the manuscript's displayed coefficient `1/5000` to `1/100`. The +proof uses the same two convexity intervals, with the endpoint signs certified +by rational logarithm bounds. + +### 3.2 Residual restriction instead of cycle traversal + +For the exposed high matching `M`, restriction + +\[ + F\longmapsto F\setminus M +\] + +is injective on even edge sets. Therefore + +\[ + \sum_{F\ \mathrm{even}}\prod_{e\in F\setminus M}q_e + \le \prod_{e\notin M}(1+q_e) + \le \exp\!\left(\sum_{e\notin M}q_e\right). +\] + +Together with the corrected one-sided off-matching square-sum inequality and +the local increment estimate already used by the manuscript, this gives + +\[ + \mathcal A(M,j) + \le \exp\!\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}. +\] + +In the large-residual regime the cost is `exp(O(N^2))`, rather than the +manuscript's `exp(O(N^8))`. This removes the simple-cycle decomposition, +residual-walk enumeration, mixed matching-cycle encoding, `tau`, and `h tau` +from that branch of the argument. + +The finite injection and the generic product-to-exponential algebra already +have Lean counterparts. The complete probability specialization is not yet +claimed as formally closed. + +## 4. Result isolated in PR #31 + +The canonical phase-resolved root displacement is + +\[ + r_+-r_4^{co} + =\left(\frac{q^2}{4}\{q-D_4(\delta_n)\}+o(1)\right) + \frac{n}{N^3}. +\] + +For the midpoint integer and chromatic lower integer, exact floor/ceiling +arithmetic gives + +\[ + k_\chi^- - k_{co} + > \frac{r_+-r_4^{co}}2-N-3. +\] + +Since `(N+3)/(n/N^3) -> 0` and amplification subtracts only `o(n/N^3)`, no +additional fixed halving occurs after the midpoint. Conditional on the +canonical inputs and their asserted phase-uniformity, the surviving coefficient +is + +\[ + \frac{q^2}{8}\{q-D_4(\delta_n)\}. +\] + +Using only the existing manuscript certificate gives the phase-independent +coefficient + +\[ + \frac{(\ln2)^2}{8}\ln\frac{200}{153}. +\] + +PR #31 verifies the deterministic rounding and coefficient propagation; it +does not independently prove equation (5.11), the uniform `o(1)`, the second +moment, or amplification. + +## 5. Result isolated in PR #32 + +For the same four-size support `{2,3,4,5}`, exact rational interval arithmetic +proves + +\[ + D_4(\delta)<\ln\frac{639}{500}, + \qquad + \ln2-D_4(\delta)>\ln\frac{1000}{639}. +\] + +The certificate uses + +\[ + \frac{49}{20}\ln2<\lambda_4<\frac{83}{20}\ln2 +\] + +and a split at `(29/10) ln 2`. Its four omitted-weight estimates imply the +uniform omitted ratio `<139/500`. + +PR #32 proves the elementary limiting certificate conditional on the same +variational dual comparison used by Lemma 5.1. It does not independently +prove finite-to-limiting optimizer convergence or any later probabilistic +module. + +## 6. Explicit coefficient ledger + +Let + +\[ + c_{\rm old}=\frac{(\ln2)^2}{32}\ln\frac{200}{153}. +\] + +The four relevant coefficients are: + +| Inputs accepted | Coefficient | Decimal value | +|---|---:|---:| +| Current canonical display | `((ln 2)^2/32) ln(200/153)` | `0.004021983962242...` | +| PR #31 only | `((ln 2)^2/8) ln(200/153)` | `0.016087935848968...` | +| PR #32 only, canonical `/32` propagation | `((ln 2)^2/32) ln(1000/639)` | `0.006724102452095...` | +| PR #31 and PR #32 | `((ln 2)^2/8) ln(1000/639)` | `0.026896409808379...` | + +The combined value is about `6.69` times the currently displayed coefficient. +The table is a dependency ledger, not a request to change the canonical theorem +before the relevant reviews are accepted. + +## 7. Dependency structure + +```text +canonical phase/root and variational setup + | + +-----+------------------+ + | | + v v +PR #31: rounding and PR #32: limiting +constant propagation entropy certificate + | | + +-----------+------------+ + | + v + possible constant integration + +PR #30 is logically separate: it simplifies Sections 7 and 9 without relying +on either constant improvement. +``` + +In particular: + +- #30 can be reviewed and merged first; +- #31 does not depend on the stronger certificate in #32; +- #32 does not depend on the `/8` propagation in #31; +- the combined constant should be integrated only after both reviews are + accepted; +- #27 should not be used as the source of canonical replacement text while its + Section 8 globalization remains under review. + +## 8. Support-frontier diagnostic + +The companion script `experiments/support_frontier_scan.py` scans every support +of size three through five that contains `{2,3}` and is contained in +`{2,...,8}`. It minimizes the limiting advantage + +\[ + q-D_S(T) +\] + +over a 1001-point grid spanning the complete target interval. The full +support is evaluated with cutoffs 80 and 100 as a truncation-stability check. +This is numerical diagnostic evidence, not a proof. + +Selected results are: + +| Support | Scanned minimum of `q-D_S` | +|---|---:| +| `{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` to the canonical support improves the scanned limiting +advantage by only about `1.017%`, while changing the dense transportation table +from `4 by 4` to `5 by 5`. Removing deficit `4` produces a much larger loss. +The canonical support `{2,3,4,5}` therefore remains close to the practical +frontier between entropy advantage and proof complexity. + +No support-replacement theorem is claimed. A different support would require +a complete replay of integer rounding, partial diagonals, dense +transportation, high-skeleton summation, and residual attachments. + +## 9. Recommended integration order + +1. Review and merge PR #30. +2. Review PR #32's finite certificate and its variational interpretation. +3. Review PR #31's uniform root displacement, rounding, and final event + intersection. +4. Open one canonical-integration PR only after those reviews are complete. + That PR should update the canonical Markdown, generated TeX, PDFs, audit + records, equation references, and displayed constant together. +5. Keep #27 as a research notebook until the complete Section 8 + labelled/unlabelled high-skeleton summation is independently closed. + +## 10. Remaining highest-priority proof boundary + +Further support or constant optimization is lower priority than the global +Section 8 bookkeeping. The concentrated unresolved review obligation remains +the exact passage from canonical demand/witness/residual fibres to the complete +unlabelled high-skeleton sum, with every multiplicity and conditional +expectation factor explicit. + +## 11. Reproduction commands + +After the relevant branches are checked out, the focused scripts are: + +```text +python 625/experiments/section7_section9_supercheck.py +python 625/experiments/root_gap_constant_supercheck.py +python 625/experiments/four_support_entropy_certificate.py +python 625/experiments/support_frontier_scan.py +``` + +The first three scripts accompany PRs #30--#32. The fourth belongs to this +roadmap PR and is deliberately labelled diagnostic. From 64de4b44a8f1738dd1131234f131d4a407142628 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 23:26:16 +0300 Subject: [PATCH 2/3] Add support-frontier diagnostic scan --- 625/experiments/support_frontier_scan.py | 157 +++++++++++++++++++++++ 1 file changed, 157 insertions(+) create mode 100644 625/experiments/support_frontier_scan.py diff --git a/625/experiments/support_frontier_scan.py b/625/experiments/support_frontier_scan.py new file mode 100644 index 00000000..016d160f --- /dev/null +++ b/625/experiments/support_frontier_scan.py @@ -0,0 +1,157 @@ +#!/usr/bin/env python3 +"""Numerical support-frontier scan for the Erdős 625 signed profile. + +This is a diagnostic experiment, not a proof. It scans finite deficit supports +that contain {2,3}, evaluates the limiting entropy advantage over the complete +phase interval, and compares the canonical four-size profile with nearby +alternatives. + +The full-support value is approximated twice, with cutoffs 80 and 100. The +reported truncation disagreement is a numerical stability check. +""" +from __future__ import annotations + +import argparse +import itertools +import math +from dataclasses import dataclass + + +def require(condition: bool, message: str) -> None: + """Raise even under ``python -O`` when a diagnostic gate fails.""" + if not condition: + raise RuntimeError(message) + + +@dataclass(frozen=True) +class ScanResult: + support: tuple[int, ...] + minimum_advantage: float + target_at_minimum: float + + +def constrained_value(support: tuple[int, ...], target: float) -> float: + """Return ``log Z(lambda)-lambda*target`` at the mean-matching tilt.""" + q = math.log(2.0) + lo, hi = -40.0, 40.0 + + for _ in range(90): + lam = (lo + hi) / 2.0 + scores = [lam * i - q * i * i / 2.0 for i in support] + shift = max(scores) + weights = [math.exp(score - shift) for score in scores] + total = math.fsum(weights) + mean = math.fsum(i * w for i, w in zip(support, weights)) / total + if mean < target: + lo = lam + else: + hi = lam + + lam = (lo + hi) / 2.0 + scores = [lam * i - q * i * i / 2.0 for i in support] + shift = max(scores) + log_partition = shift + math.log( + math.fsum(math.exp(score - shift) for score in scores) + ) + return log_partition - lam * target + + +def scan_support( + support: tuple[int, ...], + targets: tuple[float, ...], + full_values: tuple[float, ...], +) -> ScanResult: + q = math.log(2.0) + best_advantage = float("inf") + best_target = targets[0] + for target, full_value in zip(targets, full_values): + finite_value = constrained_value(support, target) + advantage = q - (full_value - finite_value) + if advantage < best_advantage: + best_advantage = advantage + best_target = target + return ScanResult(support, best_advantage, best_target) + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--grid", type=int, default=1001) + parser.add_argument("--max-deficit", type=int, default=8) + parser.add_argument("--max-size", type=int, default=5) + args = parser.parse_args() + + require(args.grid >= 2, "--grid must be at least 2") + require(args.max_deficit >= 5, "--max-deficit must be at least 5") + require(args.max_size >= 3, "--max-size must be at least 3") + + q = math.log(2.0) + target_lo = 2.0 / q + target_hi = 1.0 + 2.0 / q + targets = tuple( + target_lo + (target_hi - target_lo) * step / (args.grid - 1) + for step in range(args.grid) + ) + + full_80 = tuple(range(-1, 80)) + full_100 = tuple(range(-1, 100)) + values_80 = tuple(constrained_value(full_80, target) for target in targets) + values_100 = tuple(constrained_value(full_100, target) for target in targets) + truncation_disagreement = max(abs(x - y) for x, y in zip(values_80, values_100)) + require(truncation_disagreement < 1e-12, "full-support truncation check failed") + + universe = tuple(range(2, args.max_deficit + 1)) + results: list[ScanResult] = [] + for size in range(3, min(args.max_size, len(universe)) + 1): + for support in itertools.combinations(universe, size): + if 2 not in support or 3 not in support: + continue + if support[0] > target_lo or support[-1] < target_hi: + continue + results.append(scan_support(support, targets, values_100)) + + results.sort(key=lambda item: item.minimum_advantage, reverse=True) + by_support = {item.support: item for item in results} + + expected = { + (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, + } + for support, reference in expected.items(): + result = by_support.get(support) + require(result is not None, f"expected support missing: {support}") + require( + abs(result.minimum_advantage - reference) < 2e-9, + f"support regression changed for {support}: " + f"{result.minimum_advantage} vs {reference}", + ) + + print("ERDOS 625 SUPPORT FRONTIER SCAN: PASS") + print("DIAGNOSTIC ONLY — numerical limiting-profile experiment") + print(f" grid points: {args.grid}") + print(f" supports scanned: {len(results)}") + print(f" full-support truncation disagreement: {truncation_disagreement:.3e}") + print() + print("rank support min(q-D_S) target at minimum") + for rank, item in enumerate(results[:15], start=1): + print( + f"{rank:>4} {str(item.support):<17} " + f"{item.minimum_advantage: .12f} {item.target_at_minimum:.12f}" + ) + + canonical = by_support[(2, 3, 4, 5)].minimum_advantage + five_size = by_support[(2, 3, 4, 5, 6)].minimum_advantage + relative_gain = (five_size / canonical - 1.0) * 100.0 + print() + print(f"canonical S4 minimum: {canonical:.12f}") + print(f"S4 plus deficit 6: {five_size:.12f}") + print(f"relative numerical gain: {relative_gain:.3f}%") + print( + "Interpretation: adding deficit 6 gives only a small limiting advantage " + "while increasing the transportation dimension from 4x4 to 5x5." + ) + + +if __name__ == "__main__": + main() From 74709bb3d223ca3c1b54fbdc59269b6ce3844ceb Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 23:26:29 +0300 Subject: [PATCH 3/3] Add review roadmap support scan workflow --- .github/workflows/erdos625-review-roadmap.yml | 33 +++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 .github/workflows/erdos625-review-roadmap.yml diff --git a/.github/workflows/erdos625-review-roadmap.yml b/.github/workflows/erdos625-review-roadmap.yml new file mode 100644 index 00000000..40c8ae5d --- /dev/null +++ b/.github/workflows/erdos625-review-roadmap.yml @@ -0,0 +1,33 @@ +name: Erdős 625 review roadmap support scan + +on: + pull_request: + paths: + - "625/REVIEW_SEQUENCE_ROADMAP.md" + - "625/experiments/support_frontier_scan.py" + - ".github/workflows/erdos625-review-roadmap.yml" + workflow_dispatch: + +permissions: + contents: read + +jobs: + support-frontier-diagnostic: + runs-on: ubuntu-24.04 + steps: + - name: Check out repository + uses: actions/checkout@v4 + + - name: Set up Python + uses: actions/setup-python@v5 + with: + python-version: "3.14" + + - name: Compile diagnostic + run: python -m py_compile 625/experiments/support_frontier_scan.py + + - name: Run full support-frontier scan + run: python 625/experiments/support_frontier_scan.py + + - name: Verify optimization-independent gates + run: python -O 625/experiments/support_frontier_scan.py --grid 101