diff --git a/625/PR27_VERIFICATION_REPORT.md b/625/PR27_VERIFICATION_REPORT.md new file mode 100644 index 00000000..afffb91e --- /dev/null +++ b/625/PR27_VERIFICATION_REPORT.md @@ -0,0 +1,127 @@ +# Verification report for Erdős 625 draft PR #27 + +**Repository base audited:** `main` at +`cda78922ea6c87bfc81f9bf693374dd045dac624`. + +**Scope.** This report audits the new review appendix, extensions note, and +standard-library verification scripts in draft PR #27. It does not audit the +entire canonical manuscript from first principles, and it does not claim that +`Erdos625Statement` is formally proved. + +## 1. Corrections made during this audit + +Four defects or ambiguities were found in earlier PR #27 text and corrected. + +1. **Missing degree-cap hypotheses in Proposition 8.0.** The high-cell matching + assertion is false for arbitrary margins. The corrected statement assumes + `s_a <= U` and `t_b <= U` for every row and column. The checker retains the + counterexample `U=4`, row margin `(6)`, column margins `(3,3)`, table `(3,3)` + as a regression test. + +2. **Non-finite middle-strip notation.** The expression + `j <= 3a/4 + O(1)` has been replaced by the exact type-dependent bound + + \[ + R_0= n/N^6`. +- The displayed central-rate constant `1/100` is valid on the stated domain. +- The exact rational checks support + + \[ + D_4(\delta)<\ln(33/25),\qquad q-D_4(\delta)>\ln(50/33), + \] + + and the separate three-support first-moment certificate recorded in the + extensions note. + +## 4. Remaining review boundary + +The tests above do not prove an asymptotic theorem. Before canonical +integration, an independent reviewer should still check: + +1. that the exact finite disintegration in Proposition 8.0 is instantiated with + precisely the same labelled/unlabelled conventions as the normalized second + moment; +2. that every factor in the global inequality (8.29d) agrees with the canonical + endpoint and conditional residual laws; +3. that the rational entropy comparisons are translated into the manuscript's + finite-`n` optimizer uniformly in the phase; +4. that carrying equation (5.11) directly through rounding and amplification + introduces only the stated `o(n/N^3)` loss; +5. the literature-dependent fixed-`p` and second-order upper-bound corollaries. + +The three-size profile and non-midpoint root placement remain proposed +alternative routes. They are not replacements for the four-size theorem until +the full partial-diagonal, transportation, high-skeleton, residual, and +amplification chains are replayed. + +## 5. Recommendation + +Keep PR #27 as a draft mathematical-review PR. The residual-restriction +simplification and the corrected Section 8 finite maps are suitable for +line-by-line review. Do not replace the canonical manuscript or publication +PDFs until that review is complete. diff --git a/625/REVIEW_GUIDE.md b/625/REVIEW_GUIDE.md new file mode 100644 index 00000000..625d80f1 --- /dev/null +++ b/625/REVIEW_GUIDE.md @@ -0,0 +1,283 @@ +# Reviewer guide for Erdős Problem 625 + +## 1. Scope and status + +This guide is an entry point for an independent mathematical review of the +candidate proof in +[`proofs/COMPLETE_PROOF_SELF_CONTAINED.md`](proofs/COMPLETE_PROOF_SELF_CONTAINED.md). +The current review appendix has been re-audited against repository `main` at +`cda78922ea6c87bfc81f9bf693374dd045dac624`. The PR branch was originally +cut earlier, so all added files state their base explicitly and remain +additive. + +The current status is deliberately narrower than “verified solution”: + +- the manuscript is a self-contained candidate proof; +- internal audits report no presently known blocking defect after the repairs + recorded on 13 July 2026; +- the diagnostics test finite identities and selected numerical inequalities + but do not prove the asymptotic theorem; +- the Lean project is substantial but partial, and `Erdos625Statement` remains + unproved. + +A reviewer should therefore treat every manuscript claim as unproved and use +this guide only as a navigation and traceability aid. + +The current PR appendix incorporates the blocking corrections raised in the +first PR review: bounded row/column degrees are now hypotheses of the high-cell +matching statement; the middle strip has exact floor bounds; the Section 8 +summation exposes its dependent witness fibres and admits infeasible formal data +only as a nonnegative overcount; and the Section 9 square-sum identity is stated +only off the exposed matching. The separate verification report records the +finite regression coverage and the remaining asymptotic review boundary. + +## 2. Exact theorem under review + +For `G_n ~ G(n,1/2)`, the manuscript claims + +\[ + \Pr\!\left\{\chi(G_n)-\zeta(G_n)\ge + \frac{(\ln2)^2}{32}\ln\!\left(\frac{200}{153}\right) + \frac{n}{(\ln n)^3}\right\}\longrightarrow1. +\] + +The quantifier is along the full sequence of integers `n`, not merely an +infinite subsequence or a density-one set. + +## 3. Canonical files + +| Purpose | Canonical location | +|---|---| +| Mathematical manuscript | `proofs/COMPLETE_PROOF_SELF_CONTAINED.md` | +| Generated TeX | `output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex` | +| Internal-layout PDF | `COMPLETE_PROOF_SELF_CONTAINED.pdf` | +| Publication source | `arxiv/main.tex` | +| Formal target | `formalization/Erdos625/Target.lean` | +| Formalization status | `formalization/FORMALIZATION_LEDGER.md` | +| Adversarial repair audit | `audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md` | +| Verification and artifact record | `FINAL_VERIFICATION.md` | +| Independent finite checker | `verification/erdos625_independent_checks.py` | +| PR #27 verification report | `PR27_VERIFICATION_REPORT.md` | +| Corrected Section 7 appendix | `proofs/PR27_SECTION7_CENTRAL_RATE.md` | +| Corrected Section 8 exposure | `proofs/PR27_SECTION8_EXPOSURE.md` | +| Corrected Section 8 sum | `proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md` | +| Corrected Section 9 route | `proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.md` | +| PR #27 finite regression checker | `experiments/review27_verification.py` | +| Entropy certificate checker | `experiments/entropy_certificate_upgrade.py` | + +Historical drafts and earlier `PASS` audits are not substitutes for the +canonical manuscript. Their scope is limited to the hashes and dates stated +inside them. + +## 4. Logical dependency chain + +The proof route is: + +1. endpoint-uniform independence-number phase expansion; +2. unrestricted chromatic lower location; +3. four-size signed first-moment root and integer profile; +4. exact sign-summed overlap identity; +5. all partial diagonals; +6. canonical high-cell decomposition and high-skeleton summation; +7. uniform capped residual attachment estimate; +8. normalized second moment; +9. Paley--Zygmund seed and induced-capacity amplification; +10. final gap comparison. + +The profile is constructed before the second-moment estimate is invoked. +Lemma 7.1 uses first-moment/profile information; Sections 8--9 then estimate +the exact overlap sum from Section 6. + +## 5. Recommended review order + +### Pass A: model, first moment, and root geometry + +Read Sections 1--5. Check: + +- the definition of the phase `alpha_0`, floor phase `alpha`, and `delta`; +- uniformity as `delta` approaches either endpoint; +- exact adjacent-size ratios for `mu_s`; +- existence and localization of both ordinary and signed roots before applying + the mean-value theorem; +- the entropy-loss constant and the direction of every comparison; +- tangent integer rounding and the effect on the exact signed first moment. + +### Pass B: exact overlap representation + +Read Section 6. Check: + +- ordered versus unordered normalization; +- compatibility of row and column signs on cells of multiplicity at least two; +- the component count `2^{c(H)}`; +- the factorization into local rewards and the binary cycle-space factor; +- the prescribed-cell bound before any product relaxation. + +### Pass C: partial diagonals + +Read Section 7 and +[`proofs/PR27_SECTION7_CENTRAL_RATE.md`](proofs/PR27_SECTION7_CENTRAL_RATE.md). +Check all three ranges separately: + +- empty corner: iteration of the exact recurrence and the Poisson majorant; +- central range: the Stirling expression, the rate function, and its uniform + negative gap; +- full corner: the reverse recurrence and use of the complete signed + first-moment margin. + +### Pass D: canonical high skeleton + +Read Section 8 together with +[`proofs/PR27_SECTION8_EXPOSURE.md`](proofs/PR27_SECTION8_EXPOSURE.md) and +[`proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md`](proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md). +The critical finite statement is the exact exposure identity: +for every overlap table, the canonical high support, its multiplicities, the +selected labelled stub pairs, and the capped residual table reconstruct the +original table uniquely, and the incidence times the residual contingency law +cancels exactly to the original law. + +Then check separately: + +- endpoint transportation; +- near-containment decoration products; +- the large-residual middle strip; +- the small-residual completion bound; +- the final sum over all feasible canonical skeletons. + +### Pass E: residual attachments + +Read Section 9 and +[`proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.md`](proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.md). +Check: + +- local reward telescoping and the fact that threshold alternatives do not + double-charge triple cells; +- injectivity of the restriction `F -> F \ M` on even edge sets; +- the weighted subset-product expansion and nonnegativity of every `q_e`; +- the distinction between the off-matching square sum and its unrestricted + factorized upper bound; +- both residual-mass regimes and the uniformity in the skeleton. + +The direct restriction argument removes the simple-cycle decomposition, +residual-walk enumeration, and mixed matching-cycle encoding from the proposed +large-residual proof. + +### Pass F: amplification and final quantifiers + +Read Sections 10--11. Check: + +- the one-block oscillation of the induced cocolourable capacity; +- inversion of the rare seed into an expectation deficit; +- the simultaneous leftover-colouring event; +- deterministic selection of the growing tail parameter; +- the final union bound and full-sequence quantifier. + +## 6. Four concentrated proof obligations + +### 6.1 Uniform root and optimizer corridor + +The derivative estimate must hold on a corridor already known to contain every +root of `L_S(n,k)+ck` for `0 <= c <= ln 2`. The signed-root localization may +not depend on the derivative estimate it is later used with. + +### 6.2 Complete partial-diagonal rate + +The central rate is + +\[ + \Phi_T(z)=R\ln R+\frac{\ln2}{2}(I_r-TR). +\] + +The review rewrite isolates a finite analytic lemma proving a uniform negative +multiple of `1-R` over the exact stated domain. Check the domain restrictions, +numerical endpoint inequalities, and the domination of entropy/Stirling +errors. + +### 6.3 Conditioned global high-skeleton expansion + +A per-cell ratio is not enough. The proof needs a finite global identity or +nonnegative expansion that records: + +- distinguishable selected cells; +- typed multiplicities when labels are forgotten; +- the one global falling-factorial denominator; +- cap and no-return constraints; +- the split between large and small residual mass. + +### 6.4 Weighted residual restriction + +The revised large-residual route uses the simpler finite fact that an even edge +set supported on a matching plus residual edges is uniquely determined by its +residual restriction. Check the injection, then verify + +\[ + \sum_{F\text{ even}}\prod_{e\in F\setminus M}q_e + \le\prod_{e\notin M}(1+q_e). +\] + +The off-matching square sum is only bounded by the unrestricted factorized sum; +it is not equal to it. The exact finite cycle and traversal modules remain +valid but are not needed by this replacement route. + +## 7. Uniformity checklist + +For every load-bearing `O`, `o`, or `Omega`, record: + +| Item | Required uniform variables | +|---|---| +| Section 3 root corridor | phase `delta`, support, `0 <= c <= ln 2` | +| finite optimizer convergence | target mean in the fixed compact interval | +| Section 7 rate gap | phase, exact rounded profile, all central subprofiles | +| Section 8 middle strip | cell type, floor errors, residual skeleton | +| Section 9 local increments | every feasible canonical skeleton | +| Section 9 residual restriction | residual edge relation, degree lists, and matching support | +| amplification | deterministic `k_n`, seed exponent, and tail parameter | + +A useful audit question is: “Could the implicit constant change with the +skeleton, phase, profile coordinate, or residual mass?” If yes, the estimate +is not yet sufficient for the downstream supremum or full-sequence limit. + +## 8. Notation cleanup + +The current manuscript uses `B_n` for two unrelated quantities: + +- the affine coefficient in the profile decomposition near equation (3.12); +- the scale `n/N^4` near equation (10.10). + +The review rewrite recommends `b_n^{aff}` for the first and `mathcal B_n` for +the second. It also recommends reserving: + +- `M` for the high matching only; +- `m_0` for residual stub mass; +- `R` for the partial-diagonal residual proportion; +- `r` for an overlap table or tail parameter only when the context is explicit. + +## 9. Mechanical checks + +The following are useful regression checks, not proof certificates: + +```text +python 625/verification/erdos625_independent_checks.py +python 625/experiments/exact_chi_zeta.py --self-test --exhaustive-n 5 +python 625/experiments/review27_verification.py +python 625/experiments/entropy_certificate_upgrade.py +``` + +For Lean reproduction, follow +[`formalization/SELF_CONTAINED_BUILD.md`](formalization/SELF_CONTAINED_BUILD.md) +and the pinned toolchain. The formalization ledger, not successful compilation +alone, determines which manuscript claims are actually closed. + +## 10. Reporting a finding + +A useful review report should identify: + +1. the exact equation, lemma, or paragraph; +2. the quantified domain in which the issue occurs; +3. whether the problem is logical, asymptotic, combinatorial, probabilistic, + notational, or expository; +4. a minimal counterexample or failed inequality when available; +5. whether downstream statements use only a weaker claim; +6. the smallest repair that restores the dependency chain. + +Avoid reporting finite numerical agreement as proof, or a successful Lean +component build as proof of an unformalized manuscript endpoint. diff --git a/625/experiments/entropy_certificate_upgrade.py b/625/experiments/entropy_certificate_upgrade.py new file mode 100644 index 00000000..f64fc28e --- /dev/null +++ b/625/experiments/entropy_certificate_upgrade.py @@ -0,0 +1,218 @@ +#!/usr/bin/env python3 +"""Exact rational checks and numerical support scans for Erdős 625. + +The exact checks certify the proposed strengthening + D_4(delta) < log(33/25), + log(2) - D_4(delta) > log(50/33), +conditional only on the displayed elementary weight comparison argument. + +The support scans are diagnostics, not proofs. +""" + +from __future__ import annotations + +from fractions import Fraction +import math +from typing import Sequence + + +# Rational intervals used in the exact certificate. +Q_LO = Fraction(693147, 10**6) +Q_HI = Fraction(693148, 10**6) +X_LO = Fraction(1071773, 10**6) +X_HI = Fraction(1071774, 10**6) + + +def certify_log_two_interval(terms: int = 8) -> None: + """Certify Q_LO < log(2) < Q_HI using log(2)=2*atanh(1/3).""" + a = Fraction(1, 3) + partial = sum( + (2 * a ** (2 * k + 1)) / (2 * k + 1) + for k in range(terms) + ) + # For k >= terms, 1/(2k+1) <= 1/(2*terms+1). + tail = ( + Fraction(2, 2 * terms + 1) + * a ** (2 * terms + 1) + / (1 - a * a) + ) + assert Q_LO < partial + assert partial + tail < Q_HI + + +def certify_tenth_root_interval() -> None: + """Certify X_LO < 2^(1/10) < X_HI by exact integer arithmetic.""" + assert X_LO**10 < 2 < X_HI**10 + + +def certify_tilt_bracket() -> None: + """Certify the four-support mean brackets at 12q/5 and 21q/5.""" + # At lambda=(12/5)q, after dividing the four weights by x^(-5), + # their exponents are 33, 32, 21, 0 for deficits 2,3,4,5. + numerator_hi = 2 * X_HI**33 + 3 * X_HI**32 + 4 * X_HI**21 + 5 + denominator_lo = X_LO**33 + X_LO**32 + X_LO**21 + 1 + assert Q_HI * numerator_hi < 2 * denominator_lo + + # At lambda=(21/5)q, the unnormalised exponents are 64,81,88,85. + # The desired inequality mean > 1+2/q is equivalent to the positive + # sum of (q(i-1)-2)w_i. Bound negative terms downward with X_HI and + # positive terms downward with X_LO. + lower_sum = Fraction(0) + for i, exponent in ((2, 64), (3, 81), (4, 88), (5, 85)): + coefficient = Q_LO * (i - 1) - 2 + x_power = X_HI**exponent if coefficient < 0 else X_LO**exponent + lower_sum += coefficient * x_power + assert lower_sum > 0 + + +def certify_omitted_weight_bounds() -> None: + """Certify L(12q/5)<3/10 and H(21q/5)<1/5.""" + # At 12q/5, after dividing by the deficit -1 weight, the low numerator + # has exponents 0,29,48 and the retained denominator 57,56,45,24. + low_num_hi = 1 + X_HI**29 + X_HI**48 + kept_den_lo = X_LO**57 + X_LO**56 + X_LO**45 + X_LO**24 + assert 10 * low_num_hi < 3 * kept_den_lo + + # At 21q/5, the first omitted high weight (deficit 6) has exponent 72. + # Subsequent ratios are at most x^(-23), so the whole tail is bounded by + # x^72/(1-x^(-23)). + high_tail_hi = X_HI**72 / (1 - X_LO**(-23)) + kept_den_lo = X_LO**64 + X_LO**81 + X_LO**88 + X_LO**85 + assert 5 * high_tail_hi < kept_den_lo + + # Recheck the two existing lambda=3q estimates with 0.7 < 2^(-1/2) < 0.71. + b_lo = Fraction(7, 10) + b_hi = Fraction(71, 100) + denominator_lo = Fraction(5, 4) + 2 * b_lo + low_num_hi = Fraction(1, 256) + b_hi / 16 + Fraction(1, 4) + high_num_hi = b_hi / 16 + Fraction(1, 256) + Fraction(1, 3968) + assert 25 * low_num_hi < 3 * denominator_lo # L(3q) < 3/25 + assert 50 * high_num_hi < denominator_lo # H(3q) < 1/50 + + +def certify_three_support_certificate() -> None: + """Certify a positive entropy advantage for support {2,3,5}.""" + # At lambda=(29/10)q the S3 exponents are 38,42,20. + # Its mean is below 2/q, so the target tilt lies to the right. + numerator_hi = 2 * X_HI**38 + 3 * X_HI**42 + 5 * X_HI**20 + denominator_lo = X_LO**38 + X_LO**42 + X_LO**20 + assert Q_HI * numerator_hi < 2 * denominator_lo + + # At lambda=(21/5)q the S3 exponents are 64,81,85. + # Its mean is above 1+2/q, so the target tilt lies to the left. + lower_sum = Fraction(0) + for i, exponent in ((2, 64), (3, 81), (5, 85)): + coefficient = Q_LO * (i - 1) - 2 + x_power = X_HI**exponent if coefficient < 0 else X_LO**exponent + lower_sum += coefficient * x_power + assert lower_sum > 0 + + # Low omitted ratio at 2.9q: after division by the deficit -1 weight, + # low exponents are 0,34,58 and retained exponents are 72,76,54. + low_29_hi = 1 + X_HI**34 + X_HI**58 + kept_29_lo = X_LO**72 + X_LO**76 + X_LO**54 + assert 5 * low_29_hi < kept_29_lo + + # At 3.5q the retained exponents are 50,60,50. The first high + # exponent is 30 and subsequent ratios are at most x^(-30). + kept_35_lo = 2 * X_LO**50 + X_LO**60 + high_35_hi = X_HI**30 / (1 - X_LO**(-30)) + assert 25 * high_35_hi < 2 * kept_35_lo + + # The low omitted ratio at 3.5q is also below 2/25. + low_35_hi = X_LO**(-40) + 1 + X_HI**30 + assert 25 * low_35_hi < 2 * kept_35_lo + + # At 4.2q the high tail begins with exponents 72,49,16; after that + # every ratio is at most x^(-43). This sharper split proves H<1/4. + kept_42_lo = X_LO**64 + X_LO**81 + X_LO**85 + high_42_hi = ( + X_HI**72 + X_HI**49 + X_HI**16 / (1 - X_LO**(-43)) + ) + assert 4 * high_42_hi < kept_42_lo + + # The omitted deficit-4 ratio is below 5/8 at the upper bracket. + assert 8 * X_HI**88 < 5 * kept_42_lo + + # The S3 mean at the upper bracket is below 4, so the deficit-4 + # ratio is increasing throughout the relevant tilt interval. + assert 2 * X_LO**64 + X_LO**81 > X_HI**85 + + +def value_function(support: Sequence[int], target: float) -> tuple[float, float]: + """Return (tilt, entropy-quadratic value) for a finite support.""" + def moments(lam: float) -> tuple[float, float]: + scores = [lam * i - math.log(2) * i * i / 2 for i in support] + maximum = max(scores) + weights = [math.exp(score - maximum) for score in scores] + total = sum(weights) + mean = sum(i * weight for i, weight in zip(support, weights)) / total + return mean, maximum + math.log(total) + + low, high = -16.0, 16.0 + for _ in range(100): + mid = (low + high) / 2 + mean, _ = moments(mid) + if mean < target: + low = mid + else: + high = mid + lam = (low + high) / 2 + _, log_partition = moments(lam) + return lam, log_partition - lam * target + + +def scan_supports() -> None: + """Numerically compare selected finite supports over the full phase interval.""" + q = math.log(2) + target_lo = 2 / q + target_hi = 1 + 2 / q + infinite_proxy = tuple(range(-1, 80)) + supports: dict[str, tuple[int, ...]] = { + "{2,3,4,5}": (2, 3, 4, 5), + "{2,3,4,5,6}": (2, 3, 4, 5, 6), + "{2,3,5}": (2, 3, 5), + "{2,4,5}": (2, 4, 5), + "{1,2,3,4,5}": (1, 2, 3, 4, 5), + } + + print("\nNumerical diagnostics (not proof):") + for name, support in supports.items(): + minimum = float("inf") + argmin = None + for step in range(2001): + target = target_lo + (target_hi - target_lo) * step / 2000 + _, full_value = value_function(infinite_proxy, target) + _, finite_value = value_function(support, target) + advantage = q - (full_value - finite_value) + if advantage < minimum: + minimum = advantage + argmin = target + print(f" {name:15s} min(q-D)={minimum:.12f} at T={argmin:.12f}") + + old_gamma = math.log(200 / 153) + new_gamma = math.log(50 / 33) + actual_s4 = 0.5207013354912283 + print("\nConstants:") + print(f" old certificate gamma = {old_gamma:.12f}") + print(f" proposed certificate gamma = {new_gamma:.12f}") + print(f" numerical S4 minimum = {actual_s4:.12f}") + print(f" current displayed constant = {q*q*old_gamma/32:.12f}") + three_gamma = math.log(400 / 391) + print(f" carry-(5.11)+new certificate = {q*q*new_gamma/8:.12f}") + print(f" proved S3 certificate gamma = {three_gamma:.12f}") + print(f" carry-(5.11)+S3 certificate = {q*q*three_gamma/8:.12f}") + + +def main() -> None: + certify_log_two_interval() + certify_tenth_root_interval() + certify_tilt_bracket() + certify_omitted_weight_bounds() + certify_three_support_certificate() + print("EXACT CERTIFICATE CHECKS: PASS") + scan_supports() + + +if __name__ == "__main__": + main() diff --git a/625/experiments/review27_verification.py b/625/experiments/review27_verification.py new file mode 100644 index 00000000..8c12bc28 --- /dev/null +++ b/625/experiments/review27_verification.py @@ -0,0 +1,388 @@ +#!/usr/bin/env python3 +"""Independent finite diagnostics for the Erdős 625 PR #27 review appendix. + +This script uses only the Python standard library. Exact combinatorial checks +use integers/Fraction. Decimal checks are explicitly labelled diagnostics, +not substitutes for the displayed analytic proofs. +""" +from __future__ import annotations + +from collections import Counter, defaultdict +from decimal import Decimal, getcontext +from fractions import Fraction +from itertools import permutations, product +from math import factorial, floor +from typing import Iterator, Sequence + + +def falling(n: int, k: int) -> int: + out = 1 + for x in range(k): + out *= n - x + return out + + +def enumerate_tables(rows: Sequence[int], cols: Sequence[int]) -> Iterator[tuple[tuple[int, ...], ...]]: + """Enumerate nonnegative integer contingency tables with given margins.""" + r, c = len(rows), len(cols) + table = [[0] * c for _ in range(r)] + + def fill(i: int, j: int, row_left: list[int], col_left: list[int]): + if i == r: + if all(x == 0 for x in col_left): + yield tuple(tuple(row) for row in table) + return + if j == c: + if row_left[i] == 0: + yield from fill(i + 1, 0, row_left, col_left) + return + if i == r - 1 and j == c - 1: + x = row_left[i] + if x == col_left[j]: + table[i][j] = x + row_left[i] -= x + col_left[j] -= x + yield from fill(i, j + 1, row_left, col_left) + row_left[i] += x + col_left[j] += x + return + maximum = min(row_left[i], col_left[j]) + for x in range(maximum + 1): + table[i][j] = x + row_left[i] -= x + col_left[j] -= x + yield from fill(i, j + 1, row_left, col_left) + row_left[i] += x + col_left[j] += x + + yield from fill(0, 0, list(rows), list(cols)) + + +def table_margins(table: Sequence[Sequence[int]]) -> tuple[list[int], list[int]]: + rows = [sum(row) for row in table] + cols = [sum(table[i][j] for i in range(len(table))) for j in range(len(table[0]))] + return rows, cols + + +def canonical_high_checks() -> int: + checked = 0 + # Regression: without degree caps the matching statement is false. + U = 4 + bad = ((3, 3),) + bad_high = [(0, j) for j, x in enumerate(bad[0]) if x > U // 2] + assert len(bad_high) == 2 + + # Exhaust bounded 2x2 tables and smaller 2x3/3x2 tables. + for nr, nc, max_u in ((2, 2, 6), (2, 3, 4), (3, 2, 4)): + for U in range(2, max_u + 1): + cutoff = U // 2 + for rows in product(range(U + 1), repeat=nr): + if sum(rows) == 0: + continue + for cols in product(range(U + 1), repeat=nc): + if sum(rows) != sum(cols): + continue + for table in enumerate_tables(rows, cols): + checked += 1 + high = [ + (i, j) + for i in range(nr) + for j in range(nc) + if table[i][j] > cutoff + ] + assert len({i for i, _ in high}) == len(high) + assert len({j for _, j in high}) == len(high) + jvals = {(i, j): table[i][j] for i, j in high} + drow = [sum(jvals.get((i, j), 0) for j in range(nc)) for i in range(nr)] + dcol = [sum(jvals.get((i, j), 0) for i in range(nr)) for j in range(nc)] + residual = [ + [0 if (i, j) in jvals else table[i][j] for j in range(nc)] + for i in range(nr) + ] + rr, cc = table_margins(residual) + assert rr == [rows[i] - drow[i] for i in range(nr)] + assert cc == [cols[j] - dcol[j] for j in range(nc)] + assert all(residual[i][j] <= cutoff for i in range(nr) for j in range(nc)) + + # Exact probability/incidence cancellation. + n = sum(rows) + J = sum(jvals.values()) + pi_num = 1 + for i in range(nr): + pi_num *= falling(rows[i], drow[i]) + for j in range(nc): + pi_num *= falling(cols[j], dcol[j]) + pi_den = falling(n, J) + for x in jvals.values(): + pi_den *= factorial(x) + incidence = Fraction(pi_num, pi_den) + + pres_num = 1 + for i in range(nr): + pres_num *= factorial(rows[i] - drow[i]) + for j in range(nc): + pres_num *= factorial(cols[j] - dcol[j]) + pres_den = factorial(n - J) + for i in range(nr): + for j in range(nc): + pres_den *= factorial(residual[i][j]) + residual_mass = Fraction(pres_num, pres_den) + + p_num = 1 + for x in rows: + p_num *= factorial(x) + for x in cols: + p_num *= factorial(x) + p_den = factorial(n) + for row in table: + for x in row: + p_den *= factorial(x) + assert incidence * residual_mass == Fraction(p_num, p_den) + return checked + + +def labelled_matching_disintegration_checks() -> int: + """Exhaust small labelled matchings and their canonical dependent encoding.""" + checked = 0 + cases = [ + (3, (3, 2), (2, 3)), + (3, (3, 3), (3, 3)), + (4, (4, 3), (3, 4)), + ] + for U, rows, cols in cases: + row_stubs = tuple((i, k) for i, degree in enumerate(rows) for k in range(degree)) + col_stubs = tuple((j, k) for j, degree in enumerate(cols) for k in range(degree)) + n = len(row_stubs) + assert n == len(col_stubs) + cutoff = U // 2 + encodings: set[tuple[object, ...]] = set() + table_counts: Counter[tuple[tuple[int, ...], ...]] = Counter() + + for perm in permutations(col_stubs): + pairs = tuple(zip(row_stubs, perm)) + table = [[0] * len(cols) for _ in rows] + for (i, _), (j, _) in pairs: + table[i][j] += 1 + table_t = tuple(tuple(row) for row in table) + table_counts[table_t] += 1 + + high = {(i, j) for i in range(len(rows)) for j in range(len(cols)) if table[i][j] > cutoff} + assert len({i for i, _ in high}) == len(high) + assert len({j for _, j in high}) == len(high) + demand = tuple(sorted(((i, j), table[i][j]) for i, j in high)) + witness = tuple(sorted(pair for pair in pairs if (pair[0][0], pair[1][0]) in high)) + residual = tuple(sorted(pair for pair in pairs if (pair[0][0], pair[1][0]) not in high)) + key = (demand, witness, residual) + assert key not in encodings + encodings.add(key) + checked += 1 + + assert checked >= len(encodings) + assert sum(table_counts.values()) == factorial(n) + for table_t, count in table_counts.items(): + table = [list(row) for row in table_t] + high = {(i, j) for i in range(len(rows)) for j in range(len(cols)) if table[i][j] > cutoff} + jvals = {(i, j): table[i][j] for i, j in high} + drow = [sum(jvals.get((i, j), 0) for j in range(len(cols))) for i in range(len(rows))] + dcol = [sum(jvals.get((i, j), 0) for i in range(len(rows))) for j in range(len(cols))] + residual = [[0 if (i, j) in high else table[i][j] for j in range(len(cols))] for i in range(len(rows))] + + table_count = 1 + for x in rows: + table_count *= factorial(x) + for x in cols: + table_count *= factorial(x) + for row in table: + for x in row: + table_count //= factorial(x) + assert count == table_count + + witness_count = 1 + for i, degree in enumerate(rows): + witness_count *= falling(degree, drow[i]) + for j, degree in enumerate(cols): + witness_count *= falling(degree, dcol[j]) + for x in jvals.values(): + witness_count //= factorial(x) + + residual_table_count = 1 + for i, degree in enumerate(rows): + residual_table_count *= factorial(degree - drow[i]) + for j, degree in enumerate(cols): + residual_table_count *= factorial(degree - dcol[j]) + for row in residual: + for x in row: + residual_table_count //= factorial(x) + assert witness_count * residual_table_count == table_count + return checked + + +def multinomial_fibre_checks() -> int: + checked = 0 + for ell in range(0, 8): + options = (0, 1, 2, 3) + fibres: dict[tuple[int, ...], int] = defaultdict(int) + weights = (Fraction(1), Fraction(2, 3), Fraction(5, 7), Fraction(11, 13)) + labelled_sum = Fraction(0) + for assignment in product(options, repeat=ell): + counts = tuple(assignment.count(e) for e in options) + fibres[counts] += 1 + term = Fraction(1) + for e in assignment: + term *= weights[e] + labelled_sum += term + for counts, cardinality in fibres.items(): + expected = factorial(ell) + for count in counts: + expected //= factorial(count) + assert cardinality == expected + checked += 1 + assert labelled_sum == sum(weights) ** ell + + # After multiplication by 1/ell!, grouping gives 1/prod count!. + grouped = Fraction(0) + for counts in fibres: + term = Fraction(1) + for e, count in enumerate(counts): + term *= weights[e] ** count / factorial(count) + grouped += term + assert grouped == labelled_sum / factorial(ell) + return checked + + +def middle_strip_checks() -> int: + checked = 0 + for a in range(4, 80): + cutoff = a // 2 + for m in range(max(1, a - 3), a + 1): + for r in range(cutoff + 1, m + 1): + e = m - r + kind = "endpoint" if e == 0 else ("near" if 4 * e < m else "middle") + if kind == "middle": + assert r <= m - ((m + 3) // 4) + assert r <= floor(3 * m / 4) + assert r <= floor(3 * a / 4) + elif kind == "near": + assert 1 <= e and 4 * e < m + checked += 1 + return checked + + +def is_even_edge_set(edge_set: set[tuple[int, int]], nr: int, nc: int) -> bool: + row_deg = [0] * nr + col_deg = [0] * nc + for i, j in edge_set: + row_deg[i] ^= 1 + col_deg[j] ^= 1 + return not any(row_deg) and not any(col_deg) + + +def all_matchings(nr: int, nc: int) -> Iterator[set[tuple[int, int]]]: + edges = [(i, j) for i in range(nr) for j in range(nc)] + for mask in range(1 << len(edges)): + chosen = {edges[k] for k in range(len(edges)) if mask >> k & 1} + if len({i for i, _ in chosen}) == len(chosen) and len({j for _, j in chosen}) == len(chosen): + yield chosen + + +def residual_restriction_checks() -> int: + checked = 0 + weights_pool = [Fraction(1, 7), Fraction(2, 5), Fraction(3, 4), Fraction(5, 3)] + for nr, nc in ((2, 2), (2, 3), (3, 3)): + all_edges = [(i, j) for i in range(nr) for j in range(nc)] + for M in all_matchings(nr, nc): + remaining = [e for e in all_edges if e not in M] + # Deterministic family of residual relations, including the full one. + residual_sets = [set(remaining)] + residual_sets += [set(remaining[::2]), set(remaining[1::2])] + for R in residual_sets: + universe = sorted(M | R) + even_sets: list[set[tuple[int, int]]] = [] + images: set[frozenset[tuple[int, int]]] = set() + for mask in range(1 << len(universe)): + F = {universe[k] for k in range(len(universe)) if mask >> k & 1} + if is_even_edge_set(F, nr, nc): + image = frozenset(F - M) + assert image not in images + images.add(image) + even_sets.append(F) + assert len(even_sets) <= 2 ** len(R - M) + + weights = {e: weights_pool[idx % len(weights_pool)] for idx, e in enumerate(sorted(R - M))} + lhs = Fraction(0) + for F in even_sets: + term = Fraction(1) + for e in F - M: + term *= weights[e] + lhs += term + rhs = Fraction(1) + for e in R - M: + rhs *= 1 + weights[e] + assert lhs <= rhs + checked += 1 + return checked + + +def residual_square_sum_checks() -> int: + """Check the corrected off-matching square-sum inequality exactly.""" + checked = 0 + for nr, nc in ((2, 2), (2, 3), (3, 2), (3, 3)): + for U in range(1, 6): + for row_deg in product(range(U + 1), repeat=nr): + m0 = sum(row_deg) + if m0 == 0: + continue + for col_deg in product(range(U + 1), repeat=nc): + if sum(col_deg) != m0: + continue + full_numerator = sum(d * d for d in row_deg) * sum(d * d for d in col_deg) + assert full_numerator <= U * U * m0 * m0 + for M in all_matchings(nr, nc): + off_numerator = sum( + row_deg[i] ** 2 * col_deg[j] ** 2 + for i in range(nr) + for j in range(nc) + if (i, j) not in M + ) + assert off_numerator <= full_numerator + checked += 1 + return checked + + +def central_rate_decimal_checks() -> None: + getcontext().prec = 80 + q = Decimal(2).ln() + c = Decimal(1) / 100 + r_lo = Decimal(1) / 64 + r_split = Decimal(47) / 100 + + def f(r: Decimal) -> Decimal: + return r * r.ln() + (Decimal(5) * q / 2 - 1) * r + c * (1 - r) + + def h(r: Decimal) -> Decimal: + return r * r.ln() + (1 - q / 2 + c) * (1 - r) + + assert f(r_lo) < Decimal("-0.0436") + assert f(r_split) < Decimal("-0.0051") + assert h(r_split) < Decimal("-0.0032") + assert h(Decimal(1)) == 0 + + +def main() -> None: + counts = { + "bounded canonical tables": canonical_high_checks(), + "labelled matching decompositions": labelled_matching_disintegration_checks(), + "typed decoration fibres": multinomial_fibre_checks(), + "middle-strip classifications": middle_strip_checks(), + "even-subgraph restriction instances": residual_restriction_checks(), + "off-matching square-sum instances": residual_square_sum_checks(), + } + central_rate_decimal_checks() + print("PR27 FINITE VERIFICATION: PASS") + for name, count in counts.items(): + print(f" {name}: {count}") + print(" central-rate endpoint diagnostics: PASS (80-digit Decimal)") + + +if __name__ == "__main__": + main() diff --git a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md new file mode 100644 index 00000000..a0b271df --- /dev/null +++ b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md @@ -0,0 +1,783 @@ +# Erdős Problem 625: result extensions and proof simplifications + +**Status.** This note records deductions and replacement arguments obtained by +re-examining the candidate manuscript at repository `main` commit +`cda78922ea6c87bfc81f9bf693374dd045dac624`. It separates: + +- exact deductions that can be inserted after ordinary mathematical review; +- exact finite inequalities whose attached script checks by rational arithmetic; +- numerical diagnostics and architectural alternatives that still require a + full replay of the proof chain. + +Nothing here is external peer review, priority verification, or a completed +Lean proof of `Erdos625Statement`. + +Throughout, + +\[ + q=\ln2,\qquad N=\ln n, +\] + +and `D_4(delta)` is the four-support entropy loss in equation (5.2) of the +canonical manuscript. + +--- + +## 1. Exact simplification of the large-residual attachment bound + +The cycle decomposition and cycle-to-walk estimates in equations +(9.15)--(9.18) are not needed at the precision required by Proposition 9.2. +The matching structure gives a direct weighted restriction injection. + +### Lemma 1.1 (an even completion of residual edges is unique) + +Let `M` be a matching in a finite graph and let `R` be any other finite edge +set. Let + +\[ + \mathcal E(M,R) + =\{F\subseteq M\cup R:\deg_F(v)\equiv0\pmod2\ \text{for every }v\}. +\] + +Then + +\[ + \rho:\mathcal E(M,R)\longrightarrow\mathcal P(R\setminus M), + \qquad + \rho(F)=F\setminus M, + \tag{1.1} +\] + +is injective. + +#### Proof + +If `rho(F)=rho(F')`, then the symmetric difference `F triangle F'` is contained +in `M`. It is also even, because the symmetric difference of two even edge +sets is even. A nonempty subset of a matching has degree one at every incident +vertex, so it cannot be even. Hence `F triangle F'` is empty and `F=F'`. +\(\square\) + +Equivalently, after the residual edges are specified, parity forces every +matching edge that can occur; some residual subsets have no completion, but +none has two. + +### Corollary 1.2 (weighted product bound) + +For nonnegative residual weights `(q_e)`, extended by zero on `M`, + +\[ + \sum_{F\in\mathcal E(M,R)}\prod_{e\in F\setminus M}q_e + \le + \sum_{S\subseteq R\setminus M}\prod_{e\in S}q_e + =\prod_{e\in R\setminus M}(1+q_e) + \le\exp\left(\sum_e q_e\right). + \tag{1.2} +\] + +This is the weighted form of the restriction injection already present in the +Lean development as `residualRestriction_injective`; the generic +product-to-exponential endpoint is already present as +`finiteInjectiveFamily_product_exp_bound`. + +### Application to Lemma 9.1 + +Equation (9.12) gives + +\[ + \mathcal A(M,j) + \le e^{\Lambda_0} + \sum_{F\in\mathcal C_{\rm even}(M,R)} + \prod_{e\in F\setminus M}q_e. + \tag{1.3} +\] + +Therefore Corollary 1.2 gives immediately + +\[ + \mathcal A(M,j) + \le\exp\left(\Lambda_0+\sum_e q_e\right). + \tag{1.4} +\] + +For every off-matching cell put +\(\widetilde\theta_{ab}=e d_ad'_b/m_0\). The weights \(q_e\) are zero on +\(M\), so (9.5)--(9.6) give + +\[ + \sum_e q_e + =\frac12\sum_{(a,b)\notin M}\widetilde\theta_{ab}^{\,2}+\Lambda_0 + \le\frac12\sum_{a,b}\widetilde\theta_{ab}^{\,2}+\Lambda_0. + \tag{1.5} +\] + +The unrestricted square sum factorizes exactly: + +\[ + \sum_{a,b}\widetilde\theta_{ab}^{\,2} + =\frac{e^2}{m_0^2} + \left(\sum_a d_a^2\right) + \left(\sum_b(d'_b)^2\right). + \tag{1.6} +\] + +Since every residual degree is at most `U` and both degree sums are `m_0`, + +\[ + \sum_a d_a^2\le Um_0, + \qquad + \sum_b(d'_b)^2\le Um_0, + \tag{1.7} +\] + +so + +\[ + \sum_{a,b}\widetilde\theta_{ab}^{\,2}\le e^2U^2. + \tag{1.8} +\] + +Together with (9.13), this yields the stronger uniform estimate + +\[ + \boxed{ + \mathcal A(M,j) + \le\exp\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} + \tag{1.9} +\] + +In the large-residual regime `m_0 >= n/N^6` and `U=O(N)`, + +\[ + \mathcal A(M,j)\le\exp(CN^2), + \tag{1.10} +\] + +which is stronger than the current `exp(CN^8)` bound and still +`exp(o(n/N^4))`. + +This replacement removes from the manuscript proof: + +- deterministic simple-cycle decompositions; +- residual-only walk enumeration; +- mixed matching-cycle encodings; +- the row-norm parameter `tau` and the `h tau` term; +- equations (9.15)--(9.18). + +Those formalized cycle and traversal modules remain independently useful, but +they are no longer logically required for the displayed second-moment bound. + +--- + +## 2. A stronger and simpler central partial-diagonal rate + +The rate estimate in Lemma 7.1 can be strengthened from `Y/5000` to `Y/100` +without changing the split point. + +### Lemma 2.1 + +Under the hypotheses and notation of Lemma 7.1A in the review rewrite, + +\[ + \boxed{\Phi_T(z)\le-\frac{1-R}{100}} + \qquad(1/64\le R\le1). + \tag{2.1} +\] + +#### Proof + +For `1/64 <= R <= 47/100`, use + +\[ + \Phi_T(z)\le R\ln R+(5q/2-1)R. + \tag{2.2} +\] + +The convex function + +\[ + f(R)=R\ln R+(5q/2-1)R+\frac{1-R}{100} + \tag{2.3} +\] + +satisfies + +\[ + f(1/64)<-0.0436, + \qquad + f(47/100)<-0.0051. + \tag{2.4} +\] + +It is therefore nonpositive throughout that interval. For +`47/100 <= R <= 1`, use + +\[ + \Phi_T(z)\le R\ln R+(1-q/2)(1-R). + \tag{2.5} +\] + +The convex function + +\[ + h(R)=R\ln R+(1-q/2+1/100)(1-R) + \tag{2.6} +\] + +has `h(47/100)<-0.0032` and `h(1)=0`, so it is nonpositive on the second +interval. This proves (2.1). \(\square\) + +This does not alter the final order, but it makes the domination of the entropy +and Stirling errors substantially less delicate. + +--- + +## 3. Carry the phase-resolved root displacement to the theorem + +The current proof obtains the sharp phase-dependent root displacement in +(5.11), then discards most of it through two safety halvings. That loss is not +structural. + +Define + +\[ + A(\delta)=q-D_4(\delta), + \qquad + A_*:=\min_{0\le\delta\le1}A(\delta). + \tag{3.1} +\] + +The value functions in Section 3 are continuous, so \(A\) is continuous. Lemma +5.1 gives \(A(\delta)>\gamma_4\) on the compact closed phase interval, where + +\[ + \gamma_4=\ln(200/153). + \tag{3.2} +\] + +Consequently \(A_*>\gamma_4\). + +Using (5.11) directly and the midpoint definition (5.13), rather than replacing +(5.11) by (5.12), gives + +\[ + k_\chi^- - k_{co} + =\left(\frac{q^2}{8}A(\delta)+o(1)\right)\frac{n}{N^3}. + \tag{3.3} +\] + +The amplification loss is `o(n/N^3)`, hence the proof yields the stronger +phase-resolved conclusion + +\[ + \boxed{ + \chi(G_n)-\zeta(G_n) + \ge\left(\frac{q^2}{8}A(\delta_n)-o(1)\right) + \frac{n}{N^3}} + \quad\text{with high probability}. + \tag{3.4} +\] + +In particular, the explicit phase-independent constant can be increased from + +\[ + \frac{q^2\gamma_4}{32} + \quad\text{to}\quad + \frac{q^2\gamma_4}{8}. + \tag{3.5} +\] + +This is a factor-four improvement that changes no profile, overlap estimate, or +amplification argument. + +--- + +## 4. An elementary stronger four-support entropy certificate + +The current certificate uses the broad tilt interval +`2q < lambda_4 < 9q/2`. A tighter interval gives a cleaner omitted-mass bound. + +### Proposition 4.1 + +For every phase, + +\[ + \frac{12}{5}q<\lambda_4<\frac{21}{5}q. + \tag{4.1} +\] + +Moreover, with `L(lambda)` and `H(lambda)` defined as in Lemma 5.1, + +\[ + L(12q/5)<3/10, + \qquad + H(3q)<1/50, + \tag{4.2} +\] + +and + +\[ + L(3q)<3/25, + \qquad + H(21q/5)<1/5. + \tag{4.3} +\] + +Hence, splitting at `lambda=3q`, + +\[ + L(\lambda_4)+H(\lambda_4)<8/25. + \tag{4.4} +\] + +Therefore + +\[ + D_4(\delta)<\ln(33/25), + \qquad + q-D_4(\delta)>\ln(50/33). + \tag{4.5} +\] + +#### Certificate + +Put `x=2^(1/10)`. The exact rational intervals + +\[ + 0.6931471/2`, the larger chromatic number is `chi(G)`, so (6.3) is directly a +lower bound for `chi(G)-zeta(G)`. For `p<1/2`, it is the complementary +chromatic gap. This identifies `p=1/2` as the unique fixed-density point where +the first-order comparison cancels and the finer `n/(ln n)^3` analysis is +needed. + +--- + +## 7. A standard upper bound narrows the remaining scale + +Let + +\[ + h(G)=\max\{\alpha(G),\omega(G)\}. +\] + +Every coclour class has size at most `h(G)`, so + +\[ + \zeta(G)\ge n/h(G). + \tag{7.1} +\] + +The standard clique/independence and chromatic estimates for `G(n,1/2)` +give + +\[ + h(G)=2\log_2n-2\log_2\log_2n+O(1) + \tag{7.2} +\] + +and, writing \(d_\chi(G)=n/\chi(G)\), + +\[ + d_\chi(G)=2\log_2n-2\log_2\log_2n+O(1) + \tag{7.3} +\] + +with high probability. Deterministically \(\chi(G)\ge n/h(G)\), so +\(d_\chi(G)\le h(G)\). The two quantities in (7.2)--(7.3) differ by `O(1)`, +and therefore + +\[ + 0\le \chi(G)-\zeta(G) + \le \frac{n}{d_\chi(G)}-\frac{n}{h(G)} + =O\left(\frac{n}{(\ln n)^2}\right). + \tag{7.4} +\] + +For the chromatic estimate, see McDiarmid (1990), cited above. The +clique-number input is the classical two-point result of Bollobás--Erdős and +Matula; see B. Bollobás and P. Erdős, *Cliques in random graphs*, Math. Proc. +Cambridge Philos. Soc. 80 (1976), 419--427, DOI +[`10.1017/S0305004100053056`](https://doi.org/10.1017/S0305004100053056). + +Combined with the candidate lower bound, this gives the current scale window + +\[ + \frac{n}{(\ln n)^3} + \ \lesssim\ + \chi(G)-\zeta(G) + \ \lesssim\ + \frac{n}{(\ln n)^2}. + \tag{7.5} +\] + +Closing the remaining logarithmic factor would require a substantially sharper +lower bound on `zeta`, not merely another improvement to the signed first +moment. + +--- + +## 8. An exactly certified three-size first-moment alternative + +Let + +\[ + S_3=\{2,3,5\}, + \qquad + D_3(\delta)=\mathcal F_{S_+}(T_0)-\mathcal F_{S_3}(T_0). + \tag{8.1} +\] + +The three-size support has a positive uniform signed advantage that can be +proved by the same elementary omitted-mass method as Lemma 5.1. + +### Proposition 8.1 (three-size entropy certificate) + +For every target + +\[ + \frac2q\le T\le1+\frac2q, +\] + +let \(\lambda_3\) be the unique tilt for the support \(S_3\). Then + +\[ + \frac{29}{10}q<\lambda_3<\frac{21}{5}q. + \tag{8.2} +\] + +At a tilt \(\lambda\), let \(L_3(\lambda)\) be the weight of deficits +\(-1,0,1\) divided by the retained \(S_3\) weight, let +\(M_4(\lambda)\) be the deficit-4 weight divided by the retained weight, and +let \(H_3(\lambda)\) be the analogous ratio for deficits at least six. The +following exact bounds hold: + +\[ + L_3(29q/10)<\frac15, + \qquad + H_3(7q/2)<\frac2{25}, + \qquad + M_4(7q/2)=\frac12, + \tag{8.3} +\] + +and + +\[ + L_3(7q/2)<\frac2{25}, + \qquad + H_3(21q/5)<\frac14, + \qquad + M_4(21q/5)<\frac58. + \tag{8.4} +\] + +Consequently + +\[ + L_3(\lambda_3)+M_4(\lambda_3)+H_3(\lambda_3) + <\frac{191}{200}, + \tag{8.5} +\] + +and hence + +\[ + \boxed{ + D_3(\delta)<\ln\frac{391}{200}, + \qquad + q-D_3(\delta)>\ln\frac{400}{391}>0.} + \tag{8.6} +\] + +#### Proof + +The mean on a finite support is strictly increasing in the tilt. At +\(29q/10\), exact rational comparison gives a mean below \(2/q\); at +\(21q/5\), it gives a mean above \(1+2/q\). This proves (8.2). + +The low ratio \(L_3\) decreases with the tilt because every low omitted index +is below every retained index. The high ratio \(H_3\) increases for the +opposite reason. The ratio \(M_4\) has logarithmic derivative +\(4-\mathbb E_{S_3,\lambda}i\). The retained mean is below four throughout +(8.2), so \(M_4\) is increasing on the relevant interval. + +Put \(x=2^{1/10}\). At \(29q/10\), after division by the deficit \(-1\) +weight, the low exponents are \(0,34,58\), while the retained exponents are +\(72,76,54\). Thus + +\[ + 5(1+x^{34}+x^{58})0`, while the retained chromatic gap becomes + +\[ + \left((1-\theta)\frac{q^2}{4}A(\delta)+o(1)\right) + \frac{n}{N^3}. + \tag{9.2} +\] + +The focused component proofs state their first-moment input only as the +existence of some fixed positive `c_Z`. This strongly suggests that every +fixed `theta>0` is admissible and that the coefficient can approach the full +root displacement as `theta` is chosen small. + +This is not yet classified as a completed improvement: every use of `c_Z` must +be replayed with constants allowed to depend on `theta`. A conservative first +test is `theta=1/4`, which increases the midpoint gap by a factor `3/2` while +leaving a substantial fixed first-moment margin. + +--- + +## 10. Verification status of the new claims + +The companion script `experiments/review27_verification.py` independently +checks the finite combinatorial seams used by the review rewrite: + +- bounded-margin canonical extraction and the exact cancellation + \(\pi(M,j)p_{\rm res}(r')=p(r)\) on 3,809 small contingency tables; +- the dependent labelled demand/witness/residual encoding and table-count + factorization on 5,880 perfect matchings; +- the typed-decoration fibre cardinality + \(\ell!/\prod_e n_e!\) and its cancellation against the endpoint-table + factorial on 330 count fibres; +- the exact endpoint/near/middle partition and the floor bound + \(r\le\lfloor3m/4\rfloor\) on 5,929 finite cases; +- injectivity of \(F\mapsto F\setminus M\), the cardinality bound, and the + weighted subset-product inequality on 162 finite bipartite instances; +- the corrected off-matching square-sum inequality on 263,967 finite + degree/matching instances; +- the endpoint signs in the \(1/100\) central-rate argument at 80 decimal + digits. + +These computations are regression and transcription tests. They do not +replace the asymptotic proof, the dependent conditional-law construction, or +an independent review of the new entropy certificates. In particular, the +three-size profile and the non-midpoint placement remain separate proposed +routes until their complete second-moment chains are replayed. + +--- + +## 11. Recommended integration order + +1. Replace the large-residual cycle expansion by Lemma 1.1 and Corollary 1.2. +2. Strengthen the central rate to (2.1). +3. Carry equation (5.11) directly to the final theorem, producing (3.4). +4. Insert the exact entropy certificate (4.1)--(4.8) after independent review of + the rational-check script. +5. Add the complement-symmetric corollary and fixed-density criticality remark. +6. Treat the three-size support and non-midpoint root placement as separate + experimental branches rather than mixing them into the canonical proof. diff --git a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex new file mode 100644 index 00000000..2ae1ecf8 --- /dev/null +++ b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex @@ -0,0 +1,156 @@ +\documentclass[11pt]{article} +\usepackage[margin=1in]{geometry} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{amsmath,amssymb,amsthm,mathtools} +\usepackage[hidelinks]{hyperref} +\usepackage{microtype} +\setlength{\emergencystretch}{3em} +\newtheorem{lemma}{Lemma} +\newtheorem{proposition}{Proposition} +\title{Erd\H{o}s Problem 625: Verified Extensions and Simplifications} +\author{Companion synopsis for draft PR \#27} +\date{24 July 2026} +\begin{document} +\maketitle + +\paragraph{Status.} +This is a concise TeX synopsis of +\texttt{ERDOS625\_EXTENSIONS\_AND\_SIMPLIFICATIONS.md}. The Markdown file +contains the detailed certificates and literature notes. Nothing here is +external peer review or a completed Lean proof of +\texttt{Erdos625Statement}. + +Throughout, let \(q=\ln2\) and \(N=\ln n\). + +\section{Direct residual-restriction bound} + +Let \(M\) be a matching and \(R\) a finite residual edge set. For +\[ + \mathcal E(M,R)=\{F\subseteq M\cup R:\deg_F(v)\equiv0\pmod2 + \text{ for every }v\}, +\] +the map \(F\mapsto F\setminus M\) is injective: the symmetric difference of +two completions with the same residual restriction would be a nonempty even +subset of a matching, which is impossible. Hence, for nonnegative weights, +\[ + \sum_{F\in\mathcal E(M,R)}\prod_{e\in F\setminus M}q_e + \le \prod_{e\in R\setminus M}(1+q_e) + \le \exp\!\left(\sum_{e\in R\setminus M}q_e\right). + \tag{1.1} +\] + +In the notation of Lemma 9.1, put +\(\widetilde\theta_{ab}=e d_ad_b'/m_0\) off the exposed matching. Because the +weights vanish on \(M\), +\[ + \sum_e q_e + =\frac12\sum_{(a,b)\notin M}\widetilde\theta_{ab}^{\,2}+\Lambda_0 + \le\frac12\sum_{a,b}\widetilde\theta_{ab}^{\,2}+\Lambda_0. + \tag{1.2} +\] +Only the unrestricted sum factorizes: +\[ + \sum_{a,b}\widetilde\theta_{ab}^{\,2} + =\frac{e^2}{m_0^2} + \left(\sum_a d_a^2\right)\left(\sum_b(d_b')^2\right) + \le e^2U^2. + \tag{1.3} +\] +Together with \(\Lambda_0\le CU^4/m_0\), this gives +\[ + \boxed{\mathcal A(M,j)\le + \exp\!\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} + \tag{1.4} +\] +Thus the large-residual regime costs only \(\exp(O(N^2))\), and the +simple-cycle decomposition, residual-walk enumeration, parameter \( au\), and +term \(h\tau\) are unnecessary for this bound. + +\section{Stronger central rate} + +On the domain of the central partial-diagonal argument, +\[ + \boxed{\Phi_T(z)\le-\frac{1-R}{100}}, + \qquad \frac1{64}\le R\le1. + \tag{2.1} +\] +The proof uses the same two convex endpoint comparisons as the manuscript but +retains the larger numerical margin. The companion finite checker evaluates +the three endpoint signs at 80 decimal digits. + +\section{Constant propagation} + +Writing \(A(\delta)=q-D_4(\delta)\), equation (5.11) and the midpoint choice give +\[ + k_\chi^- -k_{co} + =\left(\frac{q^2}{8}A(\delta)+o(1)\right)\frac{n}{N^3}. + \tag{3.1} +\] +The amplification loss is \(o(n/N^3)\). Thus carrying the existing root +displacement directly would improve the explicit coefficient from +\(q^2\gamma_4/32\) to \(q^2\gamma_4/8\), subject to line-by-line review of the +rounding and amplification propagation. + +\section{Exact entropy certificates} + +The exact rational checker verifies the four-support bounds +\[ + \frac{12}{5}q<\lambda_4<\frac{21}{5}q, + \qquad + D_4(\delta)<\ln\frac{33}{25}, + \qquad + q-D_4(\delta)>\ln\frac{50}{33}. + \tag{4.1} +\] +Combined with (3.1), the candidate coefficient is +\[ + \frac{(\ln2)^2}{8}\ln\frac{50}{33} + =0.0249544559\ldots. + \tag{4.2} +\] +The checker also verifies an exact first-moment certificate for the three-size +support \(S_3=\{2,3,5\}\): +\[ + \frac{29}{10}q<\lambda_3<\frac{21}{5}q, + \qquad + D_3(\delta)<\ln\frac{391}{200}, + \qquad + q-D_3(\delta)>\ln\frac{400}{391}. + \tag{4.3} +\] +The three-size support reduces the transportation table from \(4\times4\) to +\(3\times3\), but its complete second-moment chain has not been replayed. + +\section{Additional consequences} + +Complement invariance gives, conditionally on the candidate theorem, +\[ + \min\{\chi(G_n),\chi(\overline G_n)\}-\zeta(G_n) + \ge c\frac{n}{(\ln n)^3} + \quad\text{with high probability}. + \tag{5.1} +\] +For fixed \(p\ne1/2\), the standard dense-random-graph chromatic asymptotic +shows that the larger of \(\chi(G(n,p))\) and its complementary chromatic +number exceeds \(\zeta\) by order \(n/\ln n\); \(p=1/2\) is the unique +first-order cancellation point. Standard second-order clique/independence and +chromatic estimates also imply +\[ + 0\le\chi(G(n,1/2))-\zeta(G(n,1/2)) + =O\!\left(\frac{n}{(\ln n)^2}\right) + \quad\text{with high probability}. + \tag{5.2} +\] + +\section{Verification boundary} + +The companion scripts check 3,809 bounded contingency tables, 5,880 labelled +perfect matchings, 330 typed decoration fibres, 5,929 middle-strip cases, 162 +even-subgraph restriction instances, and 263,967 off-matching square-sum +instances. These are regression tests, not a proof of the asymptotic theorem. +The corrected Section 8 maps, the finite-\(n\) entropy translation, and the +constant propagation still require independent mathematical review before any +canonical manuscript integration. + +\end{document} diff --git a/625/proofs/PR27_SECTION7_CENTRAL_RATE.md b/625/proofs/PR27_SECTION7_CENTRAL_RATE.md new file mode 100644 index 00000000..3ebd44d4 --- /dev/null +++ b/625/proofs/PR27_SECTION7_CENTRAL_RATE.md @@ -0,0 +1,160 @@ +# PR #27: Section 7 central-rate replacement + +**Status.** This file is a review appendix and candidate replacement for the +most concentrated parts of the canonical manuscript. It does not change the +theorem, constant, four class sizes, or proof architecture. The finite maps, +fibre cardinalities, and inequality chains below are stated explicitly so that +they can be reviewed before any canonical integration. + +## Replacement block A: the central rate in Lemma 7.1 + +Insert the following lemma after equation (7.21), replacing the compressed +numerical paragraph leading to (7.25). + +### Lemma 7.1A (uniform central-rate gap) + +Let \(p=(p_i)_{i=2}^5\) be a probability vector with + +\[ + \sum_{i=2}^5 i p_i=T, + \qquad + \frac2q\le T\le1+\frac2q. +\] + +Let \(0\le z_i\le p_i\), and put + +\[ + R=\sum_{i=2}^5 z_i,\qquad + Y=1-R,\qquad + I_r=\sum_{i=2}^5 i z_i. +\] + +For + +\[ + \Phi_T(z)=R\ln R+\frac q2(I_r-TR), +\] + +with the convention \(0\ln0=0\), one has + +\[ + \Phi_T(z)\le-\frac{Y}{100} + \qquad\text{whenever}\qquad + \frac1{64}\le R\le1. + \tag{7.21a} +\] + +#### Proof + +Because every residual deficit lies in \(\{2,3,4,5\}\), + +\[ + I_r-TR=\sum_i(i-T)z_i\le(5-T)R. + \tag{7.21b} +\] + +Since \(y_i=p_i-z_i\), the mean identity for \(p\) also gives + +\[ + I_r-TR=\sum_i(T-i)y_i\le(T-2)Y. + \tag{7.21c} +\] + +First suppose \(1/64\le R\le47/100\). Since \(T\ge2/q\), + +\[ + \Phi_T(z) + \le R\left\{\ln R+\frac q2\left(5-\frac2q\right)\right\} + =R\{\ln R+5q/2-1\}. + \tag{7.21d} +\] + +The function + +\[ + f(R)=R\{\ln R+5q/2-1\}+\frac{1-R}{100} +\] + +is convex on \((0,\infty)\). Hence its maximum on +\([1/64,47/100]\) occurs at an endpoint. Using \(q<0.6932\), + +\[ + f(1/64)<-0.0436, + \qquad + f(47/100)<-0.0051, +\] + +so \(f(R)<0\) throughout the interval. + +Now suppose \(47/100\le R\le1\). Since +\(T\le1+2/q\), equation (7.21c) gives + +\[ + \Phi_T(z) + \le R\ln R+(1-q/2)(1-R). + \tag{7.21e} +\] + +Set + +\[ + h(R)=R\ln R+(1-q/2+1/100)(1-R). +\] + +This function is convex, \(h(1)=0\), and a direct evaluation gives +\(h(47/100)<-0.0032\). Convexity therefore places \(h\) below the chord joining +these endpoint values, so \(h(R)\le0\) on \([47/100,1]\). Thus + +\[ + \Phi_T(z)\le-\frac{1-R}{100}. +\] + +Combining the two ranges proves (7.21a). \(\square\) + +### Completion of the central range + +Return to the notation of Lemma 7.1. If + +\[ + m>\eta n, + \qquad + n-m>n/32, +\] + +then equation (7.13) gives \(R\ge1/64\) for all sufficiently large \(n\), and +the selected mass satisfies \(Y\ge\eta/2\). Lemma 7.1A and equation (7.20) +therefore give + +\[ + \ln D(\ell) + \le-\frac{k_{co}\alpha Y}{100} + +Ck_{co}Y\ln(e/Y)+CN. + \tag{7.24a} +\] + +Here \(Y\ge w/(64N)\), \(\alpha=(2/q+o(1))N\), and +\(k_{co}=\Theta(n/N)\). Consequently + +\[ + \frac{\ln(e/Y)}{\alpha}=o(1), + \qquad + \frac{N}{k_{co}\alpha Y}=o(1), +\] + +uniformly in the phase and in the central subprofile. After increasing the +eventual threshold for \(n\), the two error terms in (7.24a) are at most half +of the leading negative term. Thus there is an absolute \(c>0\) such that + +\[ + D(\ell)\le \exp(-c k_{co}w) + \tag{7.25} +\] + +throughout the central range. Since there are at most +\((k_{co}+1)^4\) subprofile vectors, their total contribution is \(o(1)\). + +This formulation isolates the only numerical analytic estimate used in the +central range and makes its domain independent of the later asymptotic error +comparison. + +--- diff --git a/625/proofs/PR27_SECTION7_CENTRAL_RATE.tex b/625/proofs/PR27_SECTION7_CENTRAL_RATE.tex new file mode 100644 index 00000000..c951c01b --- /dev/null +++ b/625/proofs/PR27_SECTION7_CENTRAL_RATE.tex @@ -0,0 +1,159 @@ +\documentclass[11pt]{article} +\usepackage[margin=1in]{geometry} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{amsmath,amssymb,amsthm,mathtools} +\usepackage{longtable,booktabs,array} +\usepackage[hidelinks]{hyperref} +\usepackage{microtype} +\setlength{\emergencystretch}{3em} +\providecommand{\tightlist}{\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}} +\title{PR \#27: Section 7 central-rate replacement} +\author{Companion revision for the Erd\H{o}s Problem 625 candidate manuscript} +\date{24 July 2026} +\begin{document} +\maketitle +\section{PR \#27: Section 7 central-rate replacement}\label{pr-27-section-7-central-rate-replacement} + +\textbf{Status.} This file is a review appendix and candidate replacement for the most concentrated parts of the canonical manuscript. It does not change the theorem, constant, four class sizes, or proof architecture. The finite maps, fibre cardinalities, and inequality chains below are stated explicitly so that they can be reviewed before any canonical integration. + +\subsection{Replacement block A: the central rate in Lemma 7.1}\label{replacement-block-a-the-central-rate-in-lemma-7.1} + +Insert the following lemma after equation (7.21), replacing the compressed numerical paragraph leading to (7.25). + +\subsubsection{Lemma 7.1A (uniform central-rate gap)}\label{lemma-7.1a-uniform-central-rate-gap} + +Let \(p=(p_i)_{i=2}^5\) be a probability vector with + +\[ + \sum_{i=2}^5 i p_i=T, + \qquad + \frac2q\le T\le1+\frac2q. +\] + +Let \(0\le z_i\le p_i\), and put + +\[ + R=\sum_{i=2}^5 z_i,\qquad + Y=1-R,\qquad + I_r=\sum_{i=2}^5 i z_i. +\] + +For + +\[ + \Phi_T(z)=R\ln R+\frac q2(I_r-TR), +\] + +with the convention \(0\ln0=0\), one has + +\[ + \Phi_T(z)\le-\frac{Y}{100} + \qquad\text{whenever}\qquad + \frac1{64}\le R\le1. + \tag{7.21a} +\] + +\paragraph{Proof}\label{proof} + +Because every residual deficit lies in \(\{2,3,4,5\}\), + +\[ + I_r-TR=\sum_i(i-T)z_i\le(5-T)R. + \tag{7.21b} +\] + +Since \(y_i=p_i-z_i\), the mean identity for \(p\) also gives + +\[ + I_r-TR=\sum_i(T-i)y_i\le(T-2)Y. + \tag{7.21c} +\] + +First suppose \(1/64\le R\le47/100\). Since \(T\ge2/q\), + +\[ + \Phi_T(z) + \le R\left\{\ln R+\frac q2\left(5-\frac2q\right)\right\} + =R\{\ln R+5q/2-1\}. + \tag{7.21d} +\] + +The function + +\[ + f(R)=R\{\ln R+5q/2-1\}+\frac{1-R}{100} +\] + +is convex on \((0,\infty)\). Hence its maximum on \([1/64,47/100]\) occurs at an endpoint. Using \(q<0.6932\), + +\[ + f(1/64)<-0.0436, + \qquad + f(47/100)<-0.0051, +\] + +so \(f(R)<0\) throughout the interval. + +Now suppose \(47/100\le R\le1\). Since \(T\le1+2/q\), equation (7.21c) gives + +\[ + \Phi_T(z) + \le R\ln R+(1-q/2)(1-R). + \tag{7.21e} +\] + +Set + +\[ + h(R)=R\ln R+(1-q/2+1/100)(1-R). +\] + +This function is convex, \(h(1)=0\), and a direct evaluation gives \(h(47/100)<-0.0032\). Convexity therefore places \(h\) below the chord joining these endpoint values, so \(h(R)\le0\) on \([47/100,1]\). Thus + +\[ + \Phi_T(z)\le-\frac{1-R}{100}. +\] + +Combining the two ranges proves (7.21a). \(\square\) + +\subsubsection{Completion of the central range}\label{completion-of-the-central-range} + +Return to the notation of Lemma 7.1. If + +\[ + m>\eta n, + \qquad + n-m>n/32, +\] + +then equation (7.13) gives \(R\ge1/64\) for all sufficiently large \(n\), and the selected mass satisfies \(Y\ge\eta/2\). Lemma 7.1A and equation (7.20) therefore give + +\[ + \ln D(\ell) + \le-\frac{k_{co}\alpha Y}{100} + +Ck_{co}Y\ln(e/Y)+CN. + \tag{7.24a} +\] + +Here \(Y\ge w/(64N)\), \(\alpha=(2/q+o(1))N\), and \(k_{co}=\Theta(n/N)\). Consequently + +\[ + \frac{\ln(e/Y)}{\alpha}=o(1), + \qquad + \frac{N}{k_{co}\alpha Y}=o(1), +\] + +uniformly in the phase and in the central subprofile. After increasing the eventual threshold for \(n\), the two error terms in (7.24a) are at most half of the leading negative term. Thus there is an absolute \(c>0\) such that + +\[ + D(\ell)\le \exp(-c k_{co}w) + \tag{7.25} +\] + +throughout the central range. Since there are at most \((k_{co}+1)^4\) subprofile vectors, their total contribution is \(o(1)\). + +This formulation isolates the only numerical analytic estimate used in the central range and makes its domain independent of the later asymptotic error comparison. + +\begin{center}\rule{0.5\linewidth}{0.5pt}\end{center} +\end{document} diff --git a/625/proofs/PR27_SECTION8_EXPOSURE.md b/625/proofs/PR27_SECTION8_EXPOSURE.md new file mode 100644 index 00000000..99026e0a --- /dev/null +++ b/625/proofs/PR27_SECTION8_EXPOSURE.md @@ -0,0 +1,130 @@ +# PR #27: exact canonical high-cell exposure + +**Status.** Candidate replacement text, audited against current `main` on 24 July 2026. It is not a completed proof of the asymptotic theorem. + +## Replacement block B: exact canonical exposure at the start of Section 8 + +Replace the prose following equation (8.3) with the following proposition. + +### Proposition 8.0 (canonical high-cell exposure identity) + +Let \(A,B\) be finite row and column index sets. Fix degree lists +\((s_a)_{a\in A}\), \((t_b)_{b\in B}\) satisfying + +\[ + 0\le s_a\le U,\qquad 0\le t_b\le U, + \qquad + \sum_a s_a=\sum_b t_b=n. + \tag{8.3a} +\] + +Let \(r=(r_{ab})\) be a feasible overlap table with these margins, put +\(R_0=\lfloor U/2\rfloor\), and define + +\[ + M(r)=\{(a,b):r_{ab}>R_0\}. +\] + +Then the following hold. + +1. **Matching property.** The support \(M(r)\) is a partial matching. If two + selected cells shared a row, their total would be at least + \(2(R_0+1)>U\), contradicting \(s_a\le U\); the column argument is the same. + +2. **Canonical demand and residual table.** For \(e=(a,b)\in M(r)\), set + \(j_e=r_{ab}\), \(J=\sum_{e\in M(r)}j_e\), and + + \[ + d_a=\sum_{b:(a,b)\in M(r)}j_{ab}, + \qquad + d_b'=\sum_{a:(a,b)\in M(r)}j_{ab}. + \] + + Remove the selected paired stubs and define + + \[ + s_a'=s_a-d_a, + \qquad + t_b'=t_b-d_b', + \qquad + r'_{ab}=\begin{cases} + 0,&(a,b)\in M(r),\\ + r_{ab},&(a,b)\notin M(r). + \end{cases} + \] + + The table \(r'\) has margins \((s_a')\), \((t_b')\), both summing to + \(n-J\); it vanishes on \(M(r)\) and satisfies \(r'_{ab}\le R_0\) off it. + +3. **Exact finite reconstruction.** Let \(\mathcal D(s,t,U)\) be the + finite image of the canonical high-demand map. For + \(D=(M,j)\in\mathcal D(s,t,U)\), let \(\mathcal W(D)\) be the finite set of + labelled prescribed-demand witnesses. For a witness \(w\in\mathcal W(D)\), + let \(\Omega_{\rm res}(w)\) be the residual matching space with the displayed + residual margins, zero-on-\(M\), and cap-off-\(M\) conditions. A full + matching is recovered uniquely from \((D,w,\omega)\), and canonical + extraction gives the inverse map. Thus the exact finite decomposition is + the dependent disjoint union + + \[ + \Omega(s,t)\ \cong\ + \bigsqcup_{D\in\mathcal D(s,t,U)} + \bigsqcup_{w\in\mathcal W(D)}\Omega_{\rm res}(w). + \tag{8.3b} + \] + + The dependence on \(w\) is material: residual stub types are canonically + relabelled for each witness before comparison with a standard residual + configuration space. + +4. **Exact mass cancellation.** The aggregate normalized incidence obtained by + summing all labelled witnesses for the demand \(D=(M,j)\) is + + \[ + \pi(M,j)= + \frac{\prod_a(s_a)_{d_a}\prod_b(t_b)_{d_b'}} + {(n)_J\prod_{e\in M}j_e!}. + \tag{8.3c} + \] + + After any fixed witness is standardized, the residual contingency-table mass + is + + \[ + p_{\rm res}(r')= + \frac{\prod_a(s_a-d_a)!\prod_b(t_b-d_b')!} + {(n-J)!\prod_{a,b}r'_{ab}!}. + \tag{8.3d} + \] + + The residual table law is the same for all witnesses after unused-stub + relabelling. Since \((s)_d=s!/(s-d)!\) and + \((n)_J=n!/(n-J)!\), + + \[ + \pi(M,j)p_{\rm res}(r') + =\frac{\prod_a s_a!\prod_b t_b!} + {n!\prod_{a,b}r_{ab}!} + =p(r). + \tag{8.3e} + \] + +Thus the canonical exposure is a genuine partition of the finite matching +space, not a union bound or a proportionality statement. The cap assumptions +in (8.3a) are essential; without them the matching assertion is false. + +### Definition 8.0A (bare canonical-skeleton weight) + +For a feasible canonical skeleton \((M,j)\), set + +\[ + \operatorname{Bare}(M,j)=\pi(M,j)\prod_{e\in M}g(j_e). + \tag{8.3f} +\] + +The residual cap/no-return event and its local/cycle factor remain in the +conditional residual law. A later use of the full residual integrand as a +nonnegative majorant does not redefine \(\operatorname{Bare}\) and does not +cause that factor to be applied twice. + +--- diff --git a/625/proofs/PR27_SECTION8_EXPOSURE.tex b/625/proofs/PR27_SECTION8_EXPOSURE.tex new file mode 100644 index 00000000..44d687b0 --- /dev/null +++ b/625/proofs/PR27_SECTION8_EXPOSURE.tex @@ -0,0 +1,125 @@ +\documentclass[11pt]{article} +\usepackage[margin=1in]{geometry} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} +\usepackage{amsmath,amssymb,amsthm,mathtools} +\usepackage{longtable,booktabs,array} +\usepackage[hidelinks]{hyperref} +\usepackage{microtype} +\setlength{\emergencystretch}{3em} +\providecommand{\tightlist}{\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}} +\title{PR \#27: exact canonical high-cell exposure} +\author{Companion revision for the Erd\H{o}s Problem 625 candidate manuscript} +\date{24 July 2026} +\begin{document} +\maketitle +\section{PR \#27: exact canonical high-cell exposure}\label{pr-27-exact-canonical-high-cell-exposure} + +\textbf{Status.} Candidate replacement text, audited against current \texttt{main} on 24 July 2026. It is not a completed proof of the asymptotic theorem. + +\subsection{Replacement block B: exact canonical exposure at the start of Section 8}\label{replacement-block-b-exact-canonical-exposure-at-the-start-of-section-8} + +Replace the prose following equation (8.3) with the following proposition. + +\subsubsection{Proposition 8.0 (canonical high-cell exposure identity)}\label{proposition-8.0-canonical-high-cell-exposure-identity} + +Let \(A,B\) be finite row and column index sets. Fix degree lists \((s_a)_{a\in A}\), \((t_b)_{b\in B}\) satisfying + +\[ + 0\le s_a\le U,\qquad 0\le t_b\le U, + \qquad + \sum_a s_a=\sum_b t_b=n. + \tag{8.3a} +\] + +Let \(r=(r_{ab})\) be a feasible overlap table with these margins, put \(R_0=\lfloor U/2\rfloor\), and define + +\[ + M(r)=\{(a,b):r_{ab}>R_0\}. +\] + +Then the following hold. + +\begin{enumerate} +\def\labelenumi{\arabic{enumi}.} +\item + \textbf{Matching property.} The support \(M(r)\) is a partial matching. If two selected cells shared a row, their total would be at least \(2(R_0+1)>U\), contradicting \(s_a\le U\); the column argument is the same. +\item + \textbf{Canonical demand and residual table.} For \(e=(a,b)\in M(r)\), set \(j_e=r_{ab}\), \(J=\sum_{e\in M(r)}j_e\), and + + \[ + d_a=\sum_{b:(a,b)\in M(r)}j_{ab}, + \qquad + d_b'=\sum_{a:(a,b)\in M(r)}j_{ab}. + \] + + Remove the selected paired stubs and define + + \[ + s_a'=s_a-d_a, + \qquad + t_b'=t_b-d_b', + \qquad + r'_{ab}=\begin{cases} + 0,&(a,b)\in M(r),\\ + r_{ab},&(a,b)\notin M(r). + \end{cases} + \] + + The table \(r'\) has margins \((s_a')\), \((t_b')\), both summing to \(n-J\); it vanishes on \(M(r)\) and satisfies \(r'_{ab}\le R_0\) off it. +\item + \textbf{Exact finite reconstruction.} Let \(\mathcal D(s,t,U)\) be the finite image of the canonical high-demand map. For \(D=(M,j)\in\mathcal D(s,t,U)\), let \(\mathcal W(D)\) be the finite set of labelled prescribed-demand witnesses. For a witness \(w\in\mathcal W(D)\), let \(\Omega_{\rm res}(w)\) be the residual matching space with the displayed residual margins, zero-on-\(M\), and cap-off-\(M\) conditions. A full matching is recovered uniquely from \((D,w,\omega)\), and canonical extraction gives the inverse map. Thus the exact finite decomposition is the dependent disjoint union + + \[ + \Omega(s,t)\ \cong\ + \bigsqcup_{D\in\mathcal D(s,t,U)} + \bigsqcup_{w\in\mathcal W(D)}\Omega_{\rm res}(w). + \tag{8.3b} + \] + + The dependence on \(w\) is material: residual stub types are canonically relabelled for each witness before comparison with a standard residual configuration space. +\item + \textbf{Exact mass cancellation.} The aggregate normalized incidence obtained by summing all labelled witnesses for the demand \(D=(M,j)\) is + + \[ + \pi(M,j)= + \frac{\prod_a(s_a)_{d_a}\prod_b(t_b)_{d_b'}} + {(n)_J\prod_{e\in M}j_e!}. + \tag{8.3c} + \] + + After any fixed witness is standardized, the residual contingency-table mass is + + \[ + p_{\rm res}(r')= + \frac{\prod_a(s_a-d_a)!\prod_b(t_b-d_b')!} + {(n-J)!\prod_{a,b}r'_{ab}!}. + \tag{8.3d} + \] + + The residual table law is the same for all witnesses after unused-stub relabelling. Since \((s)_d=s!/(s-d)!\) and \((n)_J=n!/(n-J)!\), + + \[ + \pi(M,j)p_{\rm res}(r') + =\frac{\prod_a s_a!\prod_b t_b!} + {n!\prod_{a,b}r_{ab}!} + =p(r). + \tag{8.3e} + \] +\end{enumerate} + +Thus the canonical exposure is a genuine partition of the finite matching space, not a union bound or a proportionality statement. The cap assumptions in (8.3a) are essential; without them the matching assertion is false. + +\subsubsection{Definition 8.0A (bare canonical-skeleton weight)}\label{definition-8.0a-bare-canonical-skeleton-weight} + +For a feasible canonical skeleton \((M,j)\), set + +\[ + \operatorname{Bare}(M,j)=\pi(M,j)\prod_{e\in M}g(j_e). + \tag{8.3f} +\] + +The residual cap/no-return event and its local/cycle factor remain in the conditional residual law. A later use of the full residual integrand as a nonnegative majorant does not redefine \(\operatorname{Bare}\) and does not cause that factor to be applied twice. + +\begin{center}\rule{0.5\linewidth}{0.5pt}\end{center} +\end{document} diff --git a/625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md b/625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md new file mode 100644 index 00000000..5cf0221b --- /dev/null +++ b/625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md @@ -0,0 +1,266 @@ +# PR #27: split high-skeleton summation + +**Status.** Candidate replacement text, audited against current `main` on 24 July 2026. Exact finite tests are recorded in the PR verification report; the asymptotic chain still requires independent review. + +## Replacement block C: split form of Lemma 8.3 + +### Lemma 8.3A (one-cell near-containment series) + +Let the smaller slot size be \(m\), the larger \(m+d\), with \(0\le d\le3\). +Replacing endpoint multiplicity \(m\) by \(m-e\) has exact local ratio + +\[ + R_{m,d}(e)= + \frac{\binom me}{(d+1)\cdots(d+e)} + 2^{-em+e(e+1)/2}. + \tag{8.21} +\] + +Let + +\[ + \mathcal E_m=\{e\in\mathbb N:1\le e\text{ and }4e0). +\] + +For a typed count array \(n_{\tau,e}\) with +\(\sum_e n_{\tau,e}=\ell_{ij}\), the fibre of the forgetting map + +\[ + \phi\longmapsto n_{\tau,e}=|\phi_\tau^{-1}(e)| +\] + +has the exact cardinality + +\[ + \prod_\tau\frac{\ell_\tau!}{\prod_{e\in E_\tau}n_{\tau,e}!}. + \tag{8.25a} +\] + +Consequently + +\[ + \sum_\phi\prod_{\tau}\prod_{c\in C_\tau}a_\tau(\phi_\tau(c)) + =\prod_\tau\left(\sum_{e\in E_\tau}a_\tau(e)\right)^{\ell_\tau} + \tag{8.25b} +\] + +and, after grouping by the arrays \((n_{\tau,e})\), the factor +\(\ell_\tau!\) in (8.25a) cancels exactly with the factor +\(1/\ell_\tau!\) already present in \(W(L)\). The resulting coefficient is +\(1/\prod_e n_{\tau,e}!\), which is exactly the typed multinomial coefficient +of the decorated table. There is no hidden multiplicity. + +Using Lemma 8.3A and the fact that a high skeleton has at most \(k_{co}\) cells, + +\[ + \sum_{\text{near decorations of }L}w(S) + \le W(L)(1+O(N^3/n))^{k_{co}} + =W(L)e^{O(N^2)}. + \tag{8.26} +\] + +### Lemma 8.3C (exact middle strip with large residual mass) + +Fix a near-containment skeleton \(S\), let \(m_0\) be its remaining stub mass, +and let \(\nu_S\) be the uniform residual matching law. On the event +\(\mathcal N(S)\) that no additional endpoint or near-containment cell occurs, +a further high cell of type \((i,j)\), with smaller size +\(m_{ij}=\min(u_i,u_j)\), has the exact range + +\[ + R_00). +\] + +For a typed count array \(n_{\tau,e}\) with \(\sum_e n_{\tau,e}=\ell_{ij}\), the fibre of the forgetting map + +\[ + \phi\longmapsto n_{\tau,e}=|\phi_\tau^{-1}(e)| +\] + +has the exact cardinality + +\[ + \prod_\tau\frac{\ell_\tau!}{\prod_{e\in E_\tau}n_{\tau,e}!}. + \tag{8.25a} +\] + +Consequently + +\[ + \sum_\phi\prod_{\tau}\prod_{c\in C_\tau}a_\tau(\phi_\tau(c)) + =\prod_\tau\left(\sum_{e\in E_\tau}a_\tau(e)\right)^{\ell_\tau} + \tag{8.25b} +\] + +and, after grouping by the arrays \((n_{\tau,e})\), the factor \(\ell_\tau!\) in (8.25a) cancels exactly with the factor \(1/\ell_\tau!\) already present in \(W(L)\). The resulting coefficient is \(1/\prod_e n_{\tau,e}!\), which is exactly the typed multinomial coefficient of the decorated table. There is no hidden multiplicity. + +Using Lemma 8.3A and the fact that a high skeleton has at most \(k_{co}\) cells, + +\[ + \sum_{\text{near decorations of }L}w(S) + \le W(L)(1+O(N^3/n))^{k_{co}} + =W(L)e^{O(N^2)}. + \tag{8.26} +\] + +\subsubsection{Lemma 8.3C (exact middle strip with large residual mass)}\label{lemma-8.3c-exact-middle-strip-with-large-residual-mass} + +Fix a near-containment skeleton \(S\), let \(m_0\) be its remaining stub mass, and let \(\nu_S\) be the uniform residual matching law. On the event \(\mathcal N(S)\) that no additional endpoint or near-containment cell occurs, a further high cell of type \((i,j)\), with smaller size \(m_{ij}=\min(u_i,u_j)\), has the exact range + +\[ + R_0