From 009474686ee333a78b2ab6565a957852d47d0090 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 23 Jul 2026 11:35:31 +0300 Subject: [PATCH 01/29] Add reviewer-oriented Problem 625 index --- 625/README.md | 635 ++++++++++---------------------------------------- 1 file changed, 124 insertions(+), 511 deletions(-) diff --git a/625/README.md b/625/README.md index 4196d1a3..f278c5db 100644 --- a/625/README.md +++ b/625/README.md @@ -1,515 +1,128 @@ -# Erdős Problem 625 research dossier - -## Complete proof - -**[Open the complete proof PDF](COMPLETE_PROOF_SELF_CONTAINED.pdf)** - -**[Open the publication-layout preprint PDF](arxiv_625.pdf)** - -The publication-layout PDF is dated 20 July 2026 and lists Samuil Petkov as -the sole author, with explicit AI-assistance, Aristotle-use, funding, and -competing-interests disclosures. It remains a candidate preprint while the -full Lean target is open. - -Its editable source, author--year bibliography, arXiv-ready `.bbl`, build -notes, and byte-identical PDF are collected in the [`arxiv/`](arxiv/) folder. - -The editable canonical manuscript is -[`proofs/COMPLETE_PROOF_SELF_CONTAINED.md`](proofs/COMPLETE_PROOF_SELF_CONTAINED.md), -and the generated TeX is -[`output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex`](output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex). - -## Supplementary exact example - -An [MP4 animation](assets/animations/erdos625-coloring-example.mp4) shows an -exact coloring and cochromatic partition of a fixed 12-vertex graph. It is an -illustrative example, not statistical or asymptotic proof evidence. - -## Lean formalization - -[`formalization/`](formalization/) contains the pinned Lean 4 formalization, -authored by **Samuil Petkov** and developed with disclosed AI assistance. The accepted project is checked -locally with Lean/mathlib `v4.31.0`. Raw Aristotle outputs remain quarantined; -only manually reviewed Lean 4.31 ports or reconstructions that pass the local -repository gates enter the accepted project. The verified closure includes -the labelled finite-graph and `G(n,1/2)` model, chromatic/cochromatic semantics, -exact phase and independent-set asymptotics, Boolean-cube and variable-block -bounded differences, induced-capacity amplification bricks, and finite -four-support entropy/optimizer continuity. - -For audit convenience, the generated -[`Erdos625SelfContained.lean`](formalization/Erdos625SelfContained.lean) -packages the current transitive local import closure into one Lean source -file; its regeneration and independent compile record are in -[`SELF_CONTAINED_BUILD.md`](formalization/SELF_CONTAINED_BUILD.md). This is a -single-file **partial checkpoint**, not a full formal proof of Sections 8--9 -or of `Erdos625Statement`. - -The Section 4 layer now proves the exact unordered profile enumeration and -first-moment formula (4.2), zero-safe factorial/log-weight bounds, the finite -`(n+1)^b` aggregate exponential estimate, and exact equivalence with the -expanded discrete profile objective. Natural profiles now embed exactly in -the constrained real profile space, and an abstract variational-envelope -theorem supplies the finite expectation interface. A zero-safe Gibbs -inequality gives an explicit one-parameter dual domination for positive -support and part count and is composed with the sharp shifted finite - probability bound. The Gibbs mean now has its two endpoint limits and a - unique interior target tilt; its positive optimizer exactly attains the fixed - finite real-profile maximum. The support is reindexed exactly by deficits - with normalized tilt `λ=B_α-t`, and the inverse, entropy, and part-count - envelope derivatives are kernel-checked. The exceptional top residual is - evaluated exactly and the full finite support has a pointwise Gaussian score - bound. Exact support reversal plus finite Gaussian-tail lemmas now give - explicit growing-support partition, first-moment, and second-moment envelopes - on every supplied bounded tilt interval, with a uniform denominator lower - bound from the zero-deficit atom. The limiting deficit Gaussian is defined - with summable moments through order two and a strictly positive partition; - its normalized mean has derivative equal to a strictly positive variance and - has endpoint limits `-1` and `+∞`. Hence every limiting target above `-1` - has a unique finite tilt and compact target intervals admit fixed brackets. -The final phase-cap squeeze interface is also kernel-checked. The layer -also constructs a nonempty kernel -partition from a coloring, refines it to exactly `k` parts, extracts the -bounded profile, and proves the deterministic event containment used in -(4.5), including all zero endpoints. Finite-space Markov and union bounds -then give the exact probability reduction and its conditional -`(n+1)^b exp(L)+μ(n,b+1)` form. - -The current Sections 6--8 checkpoint now includes the exact fixed-row ordered -overlap law (6.1)--(6.2), the uniform configuration-model prescribed-cell bound -(6.8), the effective -falling-factorial estimate (6.10), and the all-cases cellwise product bound -(6.9), including a proof that the excessive-total event is empty. The exact -partial-diagonal algebra, endpoint factorization, and recurrences (7.1)--(7.6) -are kernel-checked. Exact row and column margins of the configuration cell -table also instantiate the concrete high-cell matching assertion before -(8.2). Extending a fixed exposed witness is moreover equivalent to a bijection -of its unused stubs, with exact remaining cardinalities. The unused fibres -are now identified class-preservingly with standard residual stub types having -the exact residual degrees, so the fixed-witness extension subtype is -equivalent to the corresponding residual `ConfigurationMatching` space and -its uniform law pushes forward to the residual uniform law. Generic finite -uniform conditioning is also proved. The target-fibre and class-preservation -lemmas culminate in the exact per-cell fixed-witness identity -`full configurationCellCount = demand + residual configurationCellCount`. -The accepted cell-constraint module separately identifies `full = demand` -with residual count zero through a cap-free arithmetic lemma. Its packaged -configuration theorem assumes `hcap : demand a b <= cap` and returns that -equivalence together with `full <= cap` iff -`residual <= cap - demand`. High-skeleton cells use the zero branch; an -off-skeleton application of the unshifted residual cap first needs -`demand a b = 0`. These fixed-witness results do not by themselves select the -canonical high skeleton or package the constraints as the full Section 8 -conditional event. - -[`Section8FixedWitnessAssembly.lean`](formalization/Erdos625/Section8FixedWitnessAssembly.lean) -now composes those leaves for one fixed labelled witness: conditioning the -ambient uniform law on its extension event, transporting that law to the -residual configuration, splitting every full cell count as demand plus -residual count, and imposing the cap/no-additional-pair constraints -simultaneously. This is a fixed-witness seam theorem under its explicit -nonemptiness and `demand <= cap` hypotheses. It still does not select the -canonical high skeleton or estimate the probability of the canonical skeleton -event. - -[`Section8CanonicalSkeleton.lean`](formalization/Erdos625/Section8CanonicalSkeleton.lean) -now defines the deterministic canonical high demand and proves that its support -is a partial matching with exact on- and off-support values. It also proves -compatibility uniqueness after the selected fibres are fixed, that zero -residual mass makes a selected fibre the whole fibre, and an exact generic -translation of support-indexed cap/no-return constraints. The added theorem -`canonicalHighDemand_eq_iff_exact_support_and_capped_off` characterizes the -same cutoff by exact support values and the off-support `U/2` cap. -[`Section8CanonicalLabelledWitness.lean`](formalization/Erdos625/Section8CanonicalLabelledWitness.lean) -then proves `existsUnique_canonicalHighDemandWitness`: for one fixed -configuration matching, its literal canonical high-cell demand has a unique -labelled prescribed-demand witness extended by that matching. This is a -deterministic fixed-matching identification, not a count or probability for -the global canonical event. -[`Section8LabelledIncidence.lean`](formalization/Erdos625/Section8LabelledIncidence.lean) -proves `labelledWitnessIncidence_eq`, the normalized labelled-witness -descending-factorial identity, while -[`Section8NearSkeletonExpansion.lean`](formalization/Erdos625/Section8NearSkeletonExpansion.lean) -proves `sum_nearSkeletonChoiceWeight_eq_product` for distinguishable optional -deficit choices. These are deterministic/counting leaves. For a fixed demand, -the formalization also proves the exact finite canonical conditional-law -transport: under its strict high-demand and nonemptiness hypotheses, the -ambient conditional law is the uniform joint law of a labelled witness and a -residual-event fibre. With a reference witness this becomes a product law, -and the standardized residual coordinate has the uniform finite marginal. -The corresponding exact event-probability factorization is also proved as -labelled-witness incidence times the fixed residual-event probability. None -of these facts proves event nonemptiness or a quantitative skeleton estimate; -the unlabelled typed-skeleton multiplicity bridge, ratio bounds, and the -endpoint/near/middle estimates of Lemma 8.3 remain open. - -At the ambient level, -[`Section8CanonicalDemandGlobalResidual.lean`](formalization/Erdos625/Section8CanonicalDemandGlobalResidual.lean) -now decomposes every configuration matching by its attained canonical-demand -table, its labelled witness, and its demand-dependent residual event. It -transports the ambient uniform law to this dependent sigma space and proves -that a demand table has mass proportional to its exact fibre cardinality. It -also factors that fibre into its labelled-witness cardinality times one -demand-specific residual-fibre cardinality. It does not claim that demands -are uniformly distributed, that one residual law works across all demands, or -that any canonical event is likely. - -The companion marginal theorem states this directly as the labelled-witness -cardinality times that demand-specific residual-fibre cardinality, divided by -the ambient matching-space cardinality. - -[`Section9GlobalCanonicalResidualBridge.lean`](formalization/Erdos625/Section9GlobalCanonicalResidualBridge.lean) -then retypes every residual fibre by its literal Section 9 cap/no-return -event and transports the ambient uniform matching PMF exactly to the uniform -PMF on that tagged Section 9 sigma family. The attained demand and labelled -witness remain explicit tags, so this is not an untagged residual -distribution, conditioning statement, expectation bound, or asymptotic -estimate. - -For Section 9, restriction to the residual relation is proved injective for -even matrices supported on the union of that relation with a row matching, -giving a generic `2 ^ |R|` cardinal bound. Finite bipartite edge sets now have -an injective zero-one incidence-matrix encoding over `ZMod 2`, with matrix -parity equivalent to even row and column fibres. The number of cells of an -actual configuration matching with multiplicity at least two is at most the -total row-stub count divided by two. The explicitly defined actual residual -even-edge family is now connected to the generic restriction theorem, giving -the precise `2 ^ |R|` support bound, and the division-free finite choose-two -mass estimate (9.21) is proved. It also has an exact one-sided `ENNReal` -weighted embedding into the finite sum over all even bipartite edge sets, for -arbitrary cell weights. This is a subfamily comparison, not an `ENNReal` -polymer estimate. The finite forest-plus-residual-edge -cycle-rank inequality in (9.20) is also kernel-checked, including its literal -configuration-support and `m₀ / 2` forms. The exact finite binary cycle-space -cardinality, a recoverable real-valued minimal-even polymer decomposition, and -the abstract row-norm/geometric traversal kernel are also proved. The accepted -[`Section9MatchingTraversalBridge.lean`](formalization/Erdos625/Section9MatchingTraversalBridge.lean) -adds the relaxed finite matching-operator/walk-mass bridge: matching traversal -preserves the residual row bound, oriented starts cost exactly `2 * |M|`, and -the finite block-walk sum has the stated geometric bound. It does not build -the positive residual kernel from `q` or an injective, weight-preserving -cycle-to-walk encoding. The exact finite subfamily embedding is checked, but -an `ENNReal` polymer bound, the cycle-to-walk weight transfer, instantiation -of the accepted eventual-`tau` bridge, -the finite attachment estimates, and the global Lemma -9.1/Proposition 9.2 -assembly remain open. Aristotle is used only for redundant -isolated candidate generation; reviewed local Lean 4.31 source is -authoritative. -The capped degree moments and exact theta factorizations/bounds behind -(9.13)--(9.14) are also kernel-checked. The literal residual `q` now has a -finite degree-cap row/column norm bound, and hence its symmetric bipartite -cell kernel has the corresponding row norm; this still supplies neither a -conditioned residual law nor a cycle-to-walk encoding. - -[`Section9EncodingAssembly.lean`](formalization/Erdos625/Section9EncodingAssembly.lean) -packages the generic counting seam. An explicit injective even-matrix -encoding supported on a row matching together with a residual relation gives -the bound `2 ^ |R|`; when that residual relation is the actual configuration -support already bounded above, the exponent is at most half the row-stub -count. These are conditional cardinality theorems under the displayed -encoding, evenness, and support hypotheses. -[`Section9ActualResidualFamily.lean`](formalization/Erdos625/Section9ActualResidualFamily.lean) -discharges those encoding/evenness/support hypotheses for the literal finite -family of even edge sets supported on the high matching or multiplicity-at- -least-two cells. [`Section9ActualResidualWeightedEmbedding.lean`](formalization/Erdos625/Section9ActualResidualWeightedEmbedding.lean) -then proves its exact one-sided weighted `ENNReal` inclusion into the all-even -finite sum; it does not turn the separate real polymer theorem into an -`ENNReal` theorem. [`Section9ChooseTwoMass.lean`](formalization/Erdos625/Section9ChooseTwoMass.lean) -proves (9.21) in a division-free form, while -[`Section9CycleRankResidual.lean`](formalization/Erdos625/Section9CycleRankResidual.lean) -proves that a matching plus a residual relation has cycle rank at most the -number of residual cells. -[`Section9CycleRankConfigurationAssembly.lean`](formalization/Erdos625/Section9CycleRankConfigurationAssembly.lean) -identifies the literal residual-support finset and proves the full finite chain -`cycleRank ≤ |E(H_res)| ≤ m₀ / 2`. A separate accepted real-valued polymer -theorem constructs a recoverable disjoint minimal-even decomposition. The -actual family has the one-sided finite weighted embedding above, but an -`ENNReal` polymer specialization, concrete cycle-to-walk encoding and -weight/kernel transfer, instantiation of the accepted eventual-`tau` bridge, -attachment bound, and final Section 9 assembly -remain open; the exact binary cycle-space count and abstract traversal kernel -are proved below. - -[`Section9SmallResidualDeterministic.lean`](formalization/Erdos625/Section9SmallResidualDeterministic.lean) -proves the finite arithmetic conclusion (9.22). Given the literal -cap/no-return table event, the exact demand-plus-residual split, residual mass, -and the separated cycle-rank estimate, it bounds the component factor times -the complete local sign-reward product by `2^(U*m₀/2)`. It does not yet -identify the conditioned random residual table or close the full attachment -expectation in Lemma 9.1. - -[`Section9CycleSpaceCardinality.lean`](formalization/Erdos625/Section9CycleSpaceCardinality.lean) -proves the exact binary cycle-space count: finite even edge subsets are -equivalent to the `ZMod 2` incidence kernel and number exactly -`2 ^ cycleRank`. [`Section9TraversalKernel.lean`](formalization/Erdos625/Section9TraversalKernel.lean) -proves the finite row-norm walk estimate, the one-time marked-start factor, and -the positive/even geometric tails behind (9.16)--(9.18). What remains is the -actual-family specialization and cycle-to-walk encoding, the concrete -weight/kernel transfer and attachment assembly. - -[`Section9CappedFixedFExpansion.lean`](formalization/Erdos625/Section9CappedFixedFExpansion.lean) -proves the faithful capped/no-return prescribed-demand expansion for one fixed -`F`. [`Section9CyclePolymerBound.lean`](formalization/Erdos625/Section9CyclePolymerBound.lean) -constructs the recoverable disjoint minimal-even decomposition and proves the -finite real polymer product/exponential bound. -[`Section9FiniteAnalyticEndpoint.lean`](formalization/Erdos625/Section9FiniteAnalyticEndpoint.lean) -proves one absolute-constant finite real endpoint bound for `lambda` and `q` -under its exact hypotheses. These modules do not themselves supply an -`ENNReal` polymer bound for the actual residual family, build the required -cycle-to-walk code, or supply the upstream random event. - -[`Section9RewardTelescoping.lean`](formalization/Erdos625/Section9RewardTelescoping.lean) -proves `cappedReward_telescoping`, the exact capped reward identities under -`r <= R`. [`Section9FiniteFamilyAlgebra.lean`](formalization/Erdos625/Section9FiniteFamilyAlgebra.lean) -proves `finiteInjectiveFamily_product_exp_bound` under explicit injectivity and -pointwise nonnegative product bounds. -[`Section9AttachmentAsymptotics.lean`](formalization/Erdos625/Section9AttachmentAsymptotics.lean) -proves `eventually_tau_lt_one_third` from the stated large-residual profile -inequalities and `exists_uniform_twoRegime_error` from assumed large-/small- -residual attachment estimates. It does not supply the required cycle-to-walk -and weight encodings, those upstream finite estimates, the conditioned probability -bound, or the global Section 9 assembly. - -The newest Sections 10--11 checkpoint adds eight accepted source units. -[`QuarterDensityDegree.lean`](formalization/Erdos625/QuarterDensityDegree.lean) -proves both the fixed-size-to-larger quarter-density lift and the high-degree -vertex step, and -[`QuarterRecurrence.lean`](formalization/Erdos625/QuarterRecurrence.lean) -proves the exact real recurrence (10.3a). -[`Section11EventAssembly.lean`](formalization/Erdos625/Section11EventAssembly.lean) -proves two pointwise threshold-intersection inclusions, including the explicit -constant and strict-event `+1`. -[`Section10AmplificationScales.lean`](formalization/Erdos625/Section10AmplificationScales.lean) -proves growth of the chosen radius together with the seed, transformed-radius, -real cube-root, and additive-constant little-o terms on the -`n/(log n)^3` scale. Its `amplificationError_isLittleO_gapBase` now assembles -the exact displayed deterministic error from those four components. -[`Section11AsymptoticAssembly.lean`](formalization/Erdos625/Section11AsymptoticAssembly.lean) -proves the generic full-sequence intersection, eventual threshold, and scale- -divergence lemmas. Its `fixedThreshold_tail_of_movingThreshold` proves the -generic implication from an assumed diverging moving tail to every fixed -threshold, including for `n`-dependent sample spaces. -[`Section10QuarterUnionDecay.lean`](formalization/Erdos625/Section10QuarterUnionDecay.lean) -proves `quarterDensity_unionBound_tendsto_zero`, the full-sequence deterministic -union-cost decay at -`u₀ = ceil(n^(1/4))`, while -[`Section10ComplementInvariance.lean`](formalization/Erdos625/Section10ComplementInvariance.lean) -proves that graph complementation preserves the ambient finite `G(n,1/2)` law -exactly. This symmetry does not provide the still-missing fixed induced- -restriction pushforward. -[`Section10SimultaneousGreedyColoring.lean`](formalization/Erdos625/Section10SimultaneousGreedyColoring.lean) -proves `simultaneous_induced_chromatic_bound`, the internal-`forall U` greedy -chromatic bound from one graph-uniform independent-block hypothesis. These -atoms do not prove the random event -supplying that hypothesis, Lemma 10.1, Lemma 10.2, the actual Section 11 -sequence/tail instantiation, or the final theorem. The exact remaining DAG, -quantifier order, and the declaration-scoped Aristotle request ledger are -recorded in the -[`Sections X--XI breakdown`](formalization/SECTIONS_10_11_BREAKDOWN_2026-07-14.md). - -The newly named Section 8--11 leaves have local Lean 4.31 warning-fatal builds. -This is statement-scoped acceptance of their deterministic, algebraic, or -conditional content, not completion of a manuscript section or the target. - -[`Section10_11ConditionalAssembly.lean`](formalization/Erdos625/Section10_11ConditionalAssembly.lean) -adds three auditable seams: the rounded capacity-deficit tail from explicit -seed, rounding, and radius hypotheses; a single leftover-colouring event whose -definition contains the required internal `forall W`; and the conditional -implication `erdos625Statement_of_capacity_leftover_thresholds`. The latter -assumes `hCapacityTail`, `hLeftoverTail`, `hChromaticTail`, -`hCochromaticThreshold`, and `hGapThreshold`. It is therefore **not** a proof -of `Erdos625Statement`; the corresponding probabilistic tails and concrete -threshold comparisons must still be established. - -The asymptotic target is deliberately recorded as an **unproved proposition**; -the current development is a verified partial formalization, not a completed -Lean proof of the manuscript. Growing-support moments, compact-uniform -optimizer-tilt convergence, variance stability, and generic root/rounding -interfaces are kernel-checked. In Section 4, the concrete phase objective, -its center/slope corridor, its integer decrement, and the resulting probability -limit remain open; the -signed first-moment certificate, unordered/sign-summed overlap assembly, asymptotic -partial-diagonal ranges, manuscript-specific specialization of the exact -fixed-demand canonical conditional law and probability factorization, the -skeleton quotient/estimates, and full Section 8 assembly, actual-family and -`ENNReal` polymer/weight specialization beyond the proved one-sided subfamily -inclusion, concrete -cycle-to-walk encoding and weight transfer, finite residual attachment and -conditioned probability control, and full Section 9 assembly, Section 10's -simultaneous leftover tail and concrete -seed-amplification instantiation, and Section 11's actual chromatic tail and -threshold/limit instantiation also remain open. -See the [`formalization ledger`](formalization/FORMALIZATION_LEDGER.md) for the -declaration-by-declaration status and remaining dependency graph. Reproduced -milestone evidence is recorded in the audit files under -[`formalization/`](formalization/); the latest growing-support, compact-tilt, -variance, and root-interface checkpoint is the -[`M7 audit`](formalization/M7_GROWING_SUPPORT_TILT_CORRIDOR_AUDIT_2026-07-14.md). The -complete dependency/import policy is in -[`DEPENDENCY_REPRODUCIBILITY.md`](formalization/DEPENDENCY_REPRODUCIBILITY.md). -The current Sections 6--9 atomization, Aristotle quarantine status, and exact -non-atomic obligations are tracked in the -[`Sections 6--9 breakdown`](formalization/SECTIONS_6_9_BREAKDOWN_2026-07-14.md). -The simultaneous-leftover, amplification, and final event/limit obligations -are tracked separately in the -[`Sections X--XI breakdown`](formalization/SECTIONS_10_11_BREAKDOWN_2026-07-14.md). - -## Current status - -`proofs/COMPLETE_PROOF_SELF_CONTAINED.md` contains a proposed all-`n` positive -resolution with the explicit bound +# Erdős Problem 625 candidate-proof dossier + +This directory contains a candidate full-sequence solution of Erdős Problem 625, +its publication artifacts, finite diagnostics, internal audits, and an +incremental Lean 4 formalization. + +## Status + +The current mathematical claim is a **candidate result**. It has undergone +substantial internal checking, but it has not been externally peer reviewed or +fully formalized. In particular: + +- the manuscript gives a self-contained proof of a polynomial-scale + chromatic--cochromatic gap for `G(n,1/2)`; +- the internal audits report no presently known blocking logical defect; +- finite computations are diagnostics only and are not proof of the asymptotic + theorem; +- the Lean development verifies many exact finite and asymptotic components, + but `Erdos625Statement` remains unproved. + +The accurate public description is therefore: + +> **Candidate full-sequence solution, internally audited, with a substantial +> partial Lean formalization; not external peer review and not a completed +> machine-checked proof.** + +## Start here + +- [Reviewer guide](REVIEW_GUIDE.md) +- [Canonical self-contained manuscript (Markdown)](proofs/COMPLETE_PROOF_SELF_CONTAINED.md) +- [Generated self-contained manuscript (TeX)](output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex) +- [Self-contained proof PDF](COMPLETE_PROOF_SELF_CONTAINED.pdf) +- [Publication-layout preprint PDF](arxiv_625.pdf) +- [Formalization ledger](formalization/FORMALIZATION_LEDGER.md) +- [Final internal verification record](FINAL_VERIFICATION.md) + +A review-focused rewrite of the most concentrated passages is available in +both formats: + +- [Markdown replacement text for Sections 7--9](proofs/SECTIONS_7_9_REVIEW_REWRITE.md) +- [TeX replacement text for Sections 7--9](proofs/SECTIONS_7_9_REVIEW_REWRITE.tex) + +These rewrite files preserve the current mathematical route while making the +partial-diagonal rate, canonical high-cell decomposition, high-skeleton sum, +and cycle-to-walk argument more explicit. They are proposed integration text, +not an additional independent proof verdict. + +## Exact target + +For `G_n ~ G(n,1/2)`, the manuscript claims \[ - \chi(G(n,1/2))-\zeta(G(n,1/2)) - \ge \frac{(\ln2)^2\ln(200/153)}{32} - \frac{n}{(\ln n)^3} - \quad\text{with high probability}. + \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 decisive overlap components passed focused independent audits, and four -independent end-to-end reconstructions each returned PASS. A fresh -severity-ranked adversarial review on 2026-07-13 then found a circular signed- -root localization in the written proof, an unstated globalization step in the -high-skeleton sum, and a one-sided/two-sided overclaim in the residual lemma. -All three were repaired without changing the theorem or constant, and three -independent regression reviews returned PASS on the corrected passages. See -[`audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md`](audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md). -The concise draft and the focused first-moment, dense-overlap, residual, and -amplification notes were subsequently synchronized to those repairs. Their -cross-document mapping is recorded in -[`audits/PROOF_COMPONENT_SYNCHRONIZATION_AUDIT_2026-07-13.md`](audits/PROOF_COMPONENT_SYNCHRONIZATION_AUDIT_2026-07-13.md). -This is internal validation of a new argument, not external peer review, -publication, priority confirmation, or community acceptance. - -A further user-supplied review dated 2026-07-12 reports **provisional internal -verification: PASS** and no blocking mathematical error. Its separately -written checker reproduces five groups of finite diagnostic tests from -Sections 6 and 8. The report, checker, reproduced output, provenance, and -limitations are indexed in [`verification/`](verification/). This is -additional internal evidence, not external peer review or machine -verification, and the finite tests do not prove the asymptotic theorem. - -As of 2026-07-12, the [public Problem 625 page](https://www.erdosproblems.com/625) -still labels the problem `OPEN`. This repository presents a proposed -resolution for scrutiny and does not claim an official status change. - -The current complete packaged dossier is available at -[`releases/Erdos-625-complete-dossier-2026-07-14.zip`](releases/Erdos-625-complete-dossier-2026-07-14.zip). -It includes the arXiv source library and the pinned Lean source project while -excluding local build/service caches and copyrighted historical-source PDFs. - -## Publication artifacts - -The canonical dossier manuscript attributes co-authorship to **Samuil Petkov -& ChatGPT 5.6**. The separate publication-layout preprint lists **Samuil -Petkov** as author and gives explicit AI-assistance and ethics disclosures. - -- [`COMPLETE_PROOF_SELF_CONTAINED.pdf`](COMPLETE_PROOF_SELF_CONTAINED.pdf) - - top-level convenience copy for immediate viewing on GitHub; byte-identical - to the compiled PDF under `output/pdf/`. -- [`proofs/COMPLETE_PROOF_SELF_CONTAINED.md`](proofs/COMPLETE_PROOF_SELF_CONTAINED.md) - - canonical self-contained Markdown manuscript. -- [`output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex`](output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex) - - generated standalone TeX source with color-coded lemma/proposition boxes. -- [`output/pdf/COMPLETE_PROOF_SELF_CONTAINED.pdf`](output/pdf/COMPLETE_PROOF_SELF_CONTAINED.pdf) - - compiled 30-page A4 PDF with proofs kept outside the statement boxes. -- [`output/README.md`](output/README.md) - build versions, hashes, and PDF QA. -- [`arxiv/`](arxiv/) - publication-layout TeX, bibliography, `.bbl`, build - notes, and compiled 35-page preprint. -- [`arxiv_625.pdf`](arxiv_625.pdf) - top-level convenience copy of the - publication-layout preprint. - -## Proof authority and synchronized support - -`proofs/COMPLETE_PROOF_SELF_CONTAINED.md` is the sole authoritative proof. -The TeX and PDF are generated publication forms of that manuscript. The -component notes below retain focused derivations and route history; they have -been synchronized to the 2026-07-13 repairs but are supporting explanations, -not a second proof whose wording overrides the canonical manuscript. If a -future discrepancy appears, the canonical manuscript controls and the -discrepancy must be logged. - -- `proofs/COMPLETE_PROOF_DRAFT.md` — concise synchronized map of the theorem - and its proof obligations. -- `proofs/ALPHA_MINUS_TWO_ROUTE.md` — synchronized support for the uniform - root corridor, first-moment comparison, explicit constants, unrestricted - chromatic lower location, and tangent-rounded integer profile. -- `proofs/FOUR_SIZE_PARTIAL_RATES.md` — exact common-diagonal sum `1+o(1)`. -- `proofs/DENSE_FOUR_TYPE_MATCHING.md` — synchronized support for all - unequal-type containments, near-containments, the mixed middle strip, and - the conditioned global sum over high skeletons. -- `proofs/RESIDUAL_ATTACHMENT.md` — synchronized one-sided upper bound for - residual local and even-subgraph attachments after the large-cell matching - is exposed. -- `proofs/ALON_CONCENTRATION_EXTENSION.md` — synchronized rare-event-to-whp - transfer with the growing deterministic error/failure sequence used in the - final event intersection. - -## Independent audits - -- `audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md` — severity-ranked fresh - audit, repair register, and independent regression results; internal pass - after revision. -- `audits/PROOF_COMPONENT_SYNCHRONIZATION_AUDIT_2026-07-13.md` — traceability - matrix confirming that the focused component notes reflect those repairs; - no change to the canonical TeX/PDF content. -- `audits/RARE_EVENT_AMPLIFICATION_AUDIT.md` — pass. -- `audits/RESIDUAL_ATTACHMENT_AUDIT.md` and - `audits/DENSE_FOUR_TYPE_MATCHING_AUDIT.md` — preserved internal 2026-07-12 - verdicts on the earlier component bytes; their top notices delimit scope. -- `audits/FULL_PROOF_AUDIT_1.md` through `_4.md` — preserved independent - 2026-07-12 reconstructions; all four passed the bytes then reviewed, and - their top notices make clear that they are not reviews of later bytes. -- `verification/erdos625_verification_report.md` — additional provisional - internal verification; pass, with formalization targets identified. -- `verification/erdos625_independent_checks.py` — separately written finite - diagnostic checker; all five supplied check groups pass. - -## Literature and known results - -- `sources/SOURCE_LEDGER.md` -- `sources/RECENT_WORK_AUDIT.md` -- `sources/HISTORICAL_SOURCE_AUDIT.md` -- `sources/ERDOS625_REFERENCES.bib` -- reusable BibTeX for every reference - cited in the canonical manuscript. -- `proofs/KNOWN_RESULTS_RECONSTRUCTION.md` -- `proofs/EXCEPTIONAL_REGIME.md` - -The ledger records every source version and probability quantifier. Every -historical Problem 625 source cited in the manuscript has been checked directly -for the claim attributed to it, with pages and SHA-256 identifiers recorded in -the historical audit. Bibliographic metadata for the standard bounded- -differences and concentration references was verified against the publisher -and arXiv records. The copyrighted PDFs remain local and are not redistributed -in this repository or its release archives. - -## Reproducibility - -- `experiments/alpha_minus_two_route.py` — phase-uniform entropy losses and - certified constants. -- `experiments/dense_transport_scan.py` — exact finite falling-factorial - diagnostics for dense typed transports. -- `experiments/constrained_profile_certify.py` and - `experiments/finite_slack_profile.py` — exceptional-profile calculations. -- `experiments/exact_chi_zeta.py`, CSV, and report — certified finite graph - computations (diagnostic only). -- `experiments/render_erdos625_animation.py` — deterministic GIF/MP4 renderer - that revalidates the fixed graph and its exact partition witnesses before - producing the supplementary animation artifacts. - -`WORK_LOG.md` and `MECHANISM_REGISTRY.md` record the investigation history, -failed routes, redirections, and precise remaining status. -`FINAL_VERIFICATION.md` records the full audit history, the 2026-07-13 -adversarial repairs and regression results, the 2026-07-14 publication and -Lean-checkpoint refresh, the additional user-supplied verification, -reproducibility checks, final hashes, and the completed historical-source -audit. - -## Citation and license - -The original repository material is licensed under -[CC BY 4.0](../LICENSE). When the license requires attribution, credit -**Samuil Petkov** and follow the repository-level -[scope and attribution notice](../LICENSE_SCOPE.md). Scholarly citation -metadata are provided in [`CITATION.cff`](../CITATION.cff). +Here `chi` is the chromatic number and `zeta` is the cochromatic number. + +## Artifact map + +### Canonical proof + +- `proofs/COMPLETE_PROOF_SELF_CONTAINED.md` is the editable canonical + mathematical manuscript. +- `output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex` is the generated TeX source. +- `COMPLETE_PROOF_SELF_CONTAINED.pdf` is the compiled internal-layout PDF. + +### Publication package + +- `arxiv/` contains the publication-layout source, bibliography, build notes, + and compiled PDF. +- `arxiv_625.pdf` is the top-level publication-layout PDF. +- `../arxiv_preprints/arxiv_625/` contains the synchronized public preprint + package. + +### Audits and diagnostics + +- `audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md` records the later adversarial + review and the repairs made after the original full-chain audits. +- `FINAL_VERIFICATION.md` records artifact synchronization, diagnostic runs, + scope limitations, and hashes. +- `verification/erdos625_independent_checks.py` checks selected exact finite + identities and inequalities. +- `experiments/` contains finite examples and asymptotic diagnostics. None of + these computations substitutes for proof. + +### Lean formalization + +- `formalization/Erdos625/Target.lean` defines the exact probability target. +- `formalization/FORMALIZATION_LEDGER.md` is the authoritative declaration-level + status record. +- `formalization/Erdos625SelfContained.lean` is a generated single-file form of + the accepted import closure. +- `formalization/SELF_CONTAINED_BUILD.md` records regeneration, compilation, + and axiom checks. + +The single-file checkpoint is a **partial formalization**. Successful +compilation does not prove the manuscript theorem unless the ledger records a +proved final endpoint. + +## Review priorities + +The most valuable independent checks are concentrated in four places: + +1. the uniform root and optimizer corridor in Section 3; +2. the complete partial-diagonal rate in Lemma 7.1; +3. the conditioned canonical high-skeleton expansion in Section 8; +4. the weighted residual cycle expansion and mixed-cycle traversal in + Lemma 9.1. + +The reviewer guide gives exact entry points and a checklist for each. + +## Trust and provenance + +The manuscript names Samuil Petkov as sole author and discloses AI assistance. +Raw proof-search outputs are not treated as authoritative. Only reviewed Lean +source that passes the repository's placeholder, axiom, warning, and build +gates enters the accepted formalization. + +Internal documents labelled `PASS` are scoped to the bytes and dates stated in +those documents. They are not external peer review, professional +certification, bibliographic priority verification, or community acceptance. + +## Licensing + +See [`../LICENSE_SCOPE.md`](../LICENSE_SCOPE.md) for the scope of the repository +license and the treatment of third-party material. From b9e85da3f7f501d2c76815e4522d6d51d9d07301 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 23 Jul 2026 11:36:02 +0300 Subject: [PATCH 02/29] Add Problem 625 reviewer guide --- 625/REVIEW_GUIDE.md | 255 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 255 insertions(+) create mode 100644 625/REVIEW_GUIDE.md diff --git a/625/REVIEW_GUIDE.md b/625/REVIEW_GUIDE.md new file mode 100644 index 00000000..ef99eed8 --- /dev/null +++ b/625/REVIEW_GUIDE.md @@ -0,0 +1,255 @@ +# 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 branch containing this guide was cut from repository commit +`ddeabbf8b23b5a89b269cf5fae4ed18549a8001d`. + +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. + +## 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` | + +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 the replacement text in +[`proofs/SECTIONS_7_9_REVIEW_REWRITE.md`](proofs/SECTIONS_7_9_REVIEW_REWRITE.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. 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. Check: + +- local reward telescoping and the fact that threshold alternatives do not + double-charge triple cells; +- the total local increment and row/column norm estimates; +- the deterministic cycle decomposition used to pass from even subgraphs to a + product over simple cycles; +- residual-only cycle enumeration; +- mixed cycles meeting the high matching, including why only the first marked + matching edge costs a factor `2|M|`; +- both residual-mass regimes and the uniformity in the skeleton. + +### 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 cycle expansion + +The mixed-cycle bound must exhibit an encoding from every simple cycle meeting +the high matching to: + +- one marked and oriented matching edge; +- a sequence of nonempty residual paths; +- deterministic matching transitions. + +After the first marked edge, each matching transition is determined by the +current endpoint, so no new factor `|M|` is introduced. The replacement text +states this as a finite kernel lemma. + +## 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 traversal | row/column degree lists and matching size | +| 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 +``` + +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. From 603c6846417fb6955a3c3f695573a0e435a19643 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 23 Jul 2026 11:37:23 +0300 Subject: [PATCH 03/29] Add review-focused Markdown rewrite for Sections 7-9 --- 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md | 699 ++++++++++++++++++++++ 1 file changed, 699 insertions(+) create mode 100644 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md diff --git a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md new file mode 100644 index 00000000..83fec536 --- /dev/null +++ b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md @@ -0,0 +1,699 @@ +# Review-focused replacement text for Sections 7--9 + +**Status.** This file supplies drop-in replacement passages for the most +concentrated parts of the canonical manuscript. It does not change the theorem, +constant, four class sizes, or proof architecture. Its purpose is to make the +quantifiers, finite decompositions, and multiplicity accounting explicit enough +for independent review and later formalization. + +The text is organized as replacement blocks rather than as a second complete +manuscript. Equation numbers refer to the canonical manuscript. + +## Global notation and uniformity edits + +Use + +\[ + q=\ln2,\qquad N=\ln n,\qquad w=\ln N. +\] + +Rename the affine coefficient in equation (3.12) from `B_n` to +\(b_n^{\mathrm{aff}}\). Reserve + +\[ + \mathcal B_n:=\frac{n}{N^4} +\] + +for the amplification scale currently called `B_n` in equation (10.10). + +Unless a statement says otherwise, every asymptotic estimate in the replacement +text is uniform over: + +1. the complete phase interval \(0\le\delta<1\); +2. the exact tangent-rounded four-size profile from Section 5; +3. every feasible subprofile or canonical skeleton in the displayed finite + sum; +4. every residual degree list satisfying the displayed cap and total-mass + hypotheses. + +The constants may depend on fixed numerical corridor widths, but not on the +phase, profile coordinates, skeleton, or residual table. + +--- + +## 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}{5000} + \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}{5000} +\] + +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.053, + \qquad + f(47/100)<-0.010, +\] + +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/200)(1-R). +\] + +This function is convex, \(h(1)=0\), and a direct evaluation gives +\(h(47/100)<-0.0058\). 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}{200} + \le-\frac{1-R}{5000}. +\] + +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}{5000} + +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. + +--- + +## 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) + +Fix row degrees \((s_a)_a\) and column degrees \((t_b)_b\), each summing to +\(n\), and let \(r=(r_{ab})\) be a feasible overlap table. Put + +\[ + U=\alpha-2, + \qquad + R_0=\lfloor U/2\rfloor, + \qquad + M(r)=\{(a,b):r_{ab}>R_0\}. +\] + +Then the following hold. + +1. **Matching property.** The support \(M(r)\) is a partial matching. Indeed, + two cells in one row or column, each larger than \(U/2\), would use more + than the available degree, which is at most \(U\). + +2. **Canonical demand.** For \(e=(a,b)\in M(r)\), set \(j_e=r_{ab}\) and + \(J=\sum_{e\in M(r)}j_e\). Remove the selected \(j_e\) row and column stubs + and their prescribed pairings. The residual degree lists are + + \[ + s_a'=s_a-\sum_{b:(a,b)\in M(r)}j_{ab}, + \qquad + t_b'=t_b-\sum_{a:(a,b)\in M(r)}j_{ab}, + \] + + and both sum to \(n-J\). + +3. **Residual table.** Define + + \[ + r'_{ab}= + \begin{cases} + 0,&(a,b)\in M(r),\\ + r_{ab},&(a,b)\notin M(r). + \end{cases} + \] + + Then \(r'\) has margins \((s_a')\) and \((t_b')\), it vanishes on the + exposed matching, and \(r'_{ab}\le R_0\) off the matching. + +4. **Unique reconstruction.** Conversely, the tuple consisting of the + matching \(M\), the demands \((j_e)_{e\in M}\), the selected labelled stub + pairs, and a residual matching satisfying the zero-on-\(M\) and cap-off-\(M\) + conditions reconstructs one full matching and one overlap table. Applying + the canonical extraction to that table recovers the same tuple. + +5. **Exact mass cancellation.** The incidence of the exposed cells 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! + }, + \qquad + d_a=\sum_{b:(a,b)\in M}j_{ab}, + \quad + d_b'=\sum_{a:(a,b)\in M}j_{ab}. + \tag{8.3a} + \] + + The residual contingency-table mass is + + \[ + p_{res}(r')= + \frac{ + \prod_a(s_a-d_a)! + \prod_b(t_b-d_b')! + }{ + (n-J)!\prod_{a,b}r'_{ab}! + }. + \tag{8.3b} + \] + + Since \((s)_d=s!/(s-d)!\) and \((n)_J=n!/(n-J)!\), multiplication gives + + \[ + \begin{split} + \pi(M,j)p_{res}(r') + &= + \frac{\prod_a s_a!\prod_b t_b!} + {n!\prod_{e\in M}j_e!\prod_{a,b}r'_{ab}!}\\ + &= + \frac{\prod_a s_a!\prod_b t_b!} + {n!\prod_{a,b}r_{ab}!} + =p(r). + \end{split} + \tag{8.3c} + \] + +Hence the canonical exposure is an exact finite partition of the overlap law: +every table appears once, with no hidden multiplicity and no proportionality +constant. \(\square\) + +### Definition 8.0A (bare canonical-skeleton weight) + +For a feasible canonical skeleton \((M,j)\), define its **bare weight** to be +its exact exposure incidence multiplied by the local high-cell rewards, + +\[ + \operatorname{Bare}(M,j) + =\pi(M,j)\prod_{e\in M}g(j_e), + \tag{8.3d} +\] + +with the residual cap and no-return event retained in the residual law but with +the capped residual local/cycle factor postponed to Section 9. + +When the proof below dominates an unfinished high-cell completion by the full +residual integrand, it is using a larger nonnegative quantity only to bound the +bare completion sum. That domination does not redefine +\(\operatorname{Bare}(M,j)\), and Section 9 is still applied exactly once to the +true residual factor. + +--- + +## Replacement block C: split form of Lemma 8.3 + +Replace Lemma 8.3 by the following four lemmas and final proposition. The +calculation is the same as the canonical proof, but every summation level is +named explicitly. + +### Lemma 8.3A (one-cell near-containment sum) + +Let the smaller slot have size \(m\), the larger size \(m+d\), where +\(0\le d\le3\). Replacing an endpoint multiplicity \(m\) by \(m-e\) has the +exact local ratio + +\[ + R_{m,d}(e)= + \frac{\binom me}{(d+1)\cdots(d+e)} + 2^{-em+e(e+1)/2}. + \tag{8.21} +\] + +After charging the possible loss of \(e\) units in the one global falling +factorial by \(n^e\), one has, uniformly in the four cell types, + +\[ + \sum_{1\le e0 + \tag{8.24a} +\] + +on \(0\le e\le m/4\) for all sufficiently large \(m\). Thus the ratios are +log-convex and attain their maximum at an endpoint. At \(e=0\), equation +(8.15) gives \(\rho_0=O(N^3/n)\); at \(e=\lfloor m/4\rfloor\), +\(\rho_e=n^{-1/2+o(1)}\). Both are eventually below \(1/2\), uniformly in the +cell type, so the series is geometrically decreasing and (8.25) follows. +\(\square\) + +### Lemma 8.3B (global product over near-containment decorations) + +Fix a typed full-containment table \(L\). Temporarily distinguish every +endpoint cell occurrence of \(L\). For each occurrence \(c\), independently +choose either deficit \(e_c=0\) or \(1\le e_c0\) such that, for all sufficiently large +\(n\), every summand satisfies + +\[ + \log_2\left[ + k_{co}^2g(j)\frac{(ea^2/m_0)^j}{j!} + \right] + \le-c_0(\log_2n)^2. + \tag{8.28a} +\] + +Consequently \(\Xi_4=2^{-\Omega((\log n)^2)}\), uniformly in \(S\). + +#### Proof + +Expand over distinct residual cells and threshold demands before dropping any +constraints. Lemma 6.2 applies jointly and yields (8.26a)--(8.27). Put +\(L_2=\log_2n\) and \(j=xL_2\). The hypotheses imply + +\[ + 1+o(1)\le x\le3/2+o(1), + \qquad + \log_2m_0\ge L_2-6\log_2N. +\] + +Using \(g(j)\le2^{j^2/2}\), \(k_{co}\le n\), and +\(\log_2(j!)\ge0\), + +\[ + \log_2\left[ + k_{co}^2g(j)\frac{(ea^2/m_0)^j}{j!} + \right] + \le + 2L_2+\left(\frac{x^2}{2}-x\right)L_2^2 + +O(L_2\log L_2). +\] + +On the limiting interval \([1,3/2]\), +\(x^2/2-x\le-3/8\). Choose, for example, \(c_0=1/4\); the lower-order term is +smaller than \(L_2^2/8\) for all sufficiently large \(n\), uniformly over the +floor perturbations and the four cell types. This proves (8.28a). +\(\square\) + +### Lemma 8.3D (small residual completion) + +If \(m_0 Date: Thu, 23 Jul 2026 11:38:34 +0300 Subject: [PATCH 04/29] Add review-focused TeX rewrite for Sections 7-9 --- 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex | 552 +++++++++++++++++++++ 1 file changed, 552 insertions(+) create mode 100644 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex diff --git a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex new file mode 100644 index 00000000..4a273bbd --- /dev/null +++ b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex @@ -0,0 +1,552 @@ +\documentclass[11pt]{article} +\usepackage[margin=1in]{geometry} +\usepackage{amsmath,amssymb,amsthm,mathtools} +\usepackage[hidelinks]{hyperref} +\usepackage{enumitem} + +\newtheorem{lemma}{Lemma} +\newtheorem{proposition}{Proposition} +\theoremstyle{definition} +\newtheorem{definition}{Definition} + +\newcommand{\E}{\mathbb E} +\newcommand{\Prb}{\mathbb P} +\newcommand{\Bare}{\operatorname{Bare}} + +\title{Review-Focused Replacement Text for Sections 7--9} +\author{Companion revision for the Erd\H{o}s Problem 625 candidate manuscript} +\date{23 July 2026} + +\begin{document} +\maketitle + +\paragraph{Status.} +This file supplies drop-in replacement passages for the most concentrated +parts of the canonical manuscript. It does not change the theorem, constant, +four class sizes, or proof architecture. Its purpose is to make the +quantifiers, finite decompositions, and multiplicity accounting explicit +enough for independent review and later formalization. Equation numbers refer +to the canonical manuscript. + +\section*{Global notation and uniformity edits} + +Use +\[ + q=\ln2,\qquad N=\ln n,\qquad w=\ln N. +\] +Rename the affine coefficient in equation (3.12) from $B_n$ to +$b_n^{\mathrm{aff}}$. Reserve +\[ + \mathcal B_n:=\frac{n}{N^4} +\] +for the amplification scale currently called $B_n$ in equation (10.10). + +Unless a statement says otherwise, every asymptotic estimate below is uniform +over the complete phase interval $0\le\delta<1$, the exact tangent-rounded +four-size profile, every feasible subprofile or canonical skeleton in the +displayed finite sum, and every residual degree list satisfying the displayed +cap and total-mass hypotheses. Constants may depend on fixed numerical +corridor widths, but not on the phase, profile coordinates, skeleton, or +residual table. + +\section*{Replacement A: the central rate in Lemma 7.1} + +\begin{lemma}[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 $0\ln0=0$, one has +\[ + \Phi_T(z)\le-\frac{Y}{5000} + \qquad\text{whenever}\qquad + \frac1{64}\le R\le1. + \tag{7.21a} +\] +\end{lemma} + +\begin{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}{5000} +\] +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.053, + \qquad + f(47/100)<-0.010, +\] +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/200)(1-R). +\] +This function is convex, $h(1)=0$, and direct evaluation gives +$h(47/100)<-0.0058$. 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}{200} + \le-\frac{1-R}{5000}. +\] +\end{proof} + +\paragraph{Completion of the central range.} +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$. Equation (7.20) and the lemma give +\[ + \ln D(\ell) + \le-\frac{k_{co}\alpha Y}{5000} + +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. After increasing the eventual threshold for $n$, the error terms +are at most half of the leading negative term. Hence, for an absolute $c>0$, +\[ + D(\ell)\le \exp(-c k_{co}w). + \tag{7.25} +\] +The at most $(k_{co}+1)^4$ central vectors therefore contribute $o(1)$. + +\section*{Replacement B: exact canonical exposure at the start of Section 8} + +\begin{proposition}[Canonical high-cell exposure identity] +Fix row degrees $(s_a)_a$ and column degrees $(t_b)_b$, each summing to $n$, +and let $r=(r_{ab})$ be a feasible overlap table. Put +\[ + U=\alpha-2, + \qquad + R_0=\lfloor U/2\rfloor, + \qquad + M(r)=\{(a,b):r_{ab}>R_0\}. +\] +Then: +\begin{enumerate}[label=\arabic*.] +\item $M(r)$ is a partial matching. +\item For $e=(a,b)\in M(r)$, set $j_e=r_{ab}$ and +$J=\sum_{e\in M(r)}j_e$. The residual degrees are +\[ + s_a'=s_a-\sum_{b:(a,b)\in M(r)}j_{ab}, + \qquad + t_b'=t_b-\sum_{a:(a,b)\in M(r)}j_{ab}. +\] +\item The residual table +\[ + r'_{ab}= + \begin{cases} + 0,&(a,b)\in M(r),\\ + r_{ab},&(a,b)\notin M(r) + \end{cases} +\] +has those residual margins, vanishes on $M(r)$, and is at most $R_0$ off the +matching. +\item The matching, demands, selected labelled stub pairs, and capped residual +matching reconstruct the original matching uniquely. +\item The exposure incidence times the residual contingency law equals the +original table law exactly. +\end{enumerate} +\end{proposition} + +\begin{proof} +The matching property follows because every row and column degree is at most +$U$, while two cells larger than $U/2$ in one row or column would use more than +$U$ stubs. The margin and cap statements follow directly from the definition. +Reconstruction is by adjoining the selected labelled pairs to the residual +matching; canonical extraction recovers the same data. + +Write +\[ + d_a=\sum_{b:(a,b)\in M}j_{ab}, + \qquad + d_b'=\sum_{a:(a,b)\in M}j_{ab}. +\] +The exposure incidence 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.3a} +\] +The residual table mass is +\[ + p_{res}(r')= + \frac{ + \prod_a(s_a-d_a)! + \prod_b(t_b-d_b')! + }{ + (n-J)!\prod_{a,b}r'_{ab}! + }. + \tag{8.3b} +\] +Using $(s)_d=s!/(s-d)!$ and $(n)_J=n!/(n-J)!$ gives +\[ +\begin{split} + \pi(M,j)p_{res}(r') + &=\frac{\prod_a s_a!\prod_b t_b!} + {n!\prod_{e\in M}j_e!\prod_{a,b}r'_{ab}!}\\ + &=\frac{\prod_a s_a!\prod_b t_b!} + {n!\prod_{a,b}r_{ab}!} + =p(r). +\end{split} +\tag{8.3c} +\] +Thus every table appears once, with no hidden multiplicity or proportionality +constant. +\end{proof} + +\begin{definition}[Bare canonical-skeleton weight] +For a feasible canonical skeleton $(M,j)$, set +\[ + \Bare(M,j)=\pi(M,j)\prod_{e\in M}g(j_e). + \tag{8.3d} +\] +The residual cap and no-return event remain in the residual law, while the +capped residual local/cycle factor is postponed to Section 9. +\end{definition} + +When an unfinished high-cell completion is dominated below by the full +residual integrand, the latter is only a larger nonnegative numerical +majorant. It does not redefine $\Bare(M,j)$, and the Section 9 residual factor +is still applied exactly once. + +\section*{Replacement C: split form of Lemma 8.3} + +\begin{lemma}[One-cell near-containment sum] +Let the smaller slot have size $m$, the larger size $m+d$, where +$0\le d\le3$. Replacing endpoint multiplicity $m$ by $m-e$ has exact ratio +\[ + R_{m,d}(e)= + \frac{\binom me}{(d+1)\cdots(d+e)} + 2^{-em+e(e+1)/2}. + \tag{8.21} +\] +Uniformly in the four cell types, +\[ + \sum_{1\le e0 + \tag{8.24a} +\] +on $0\le e\le m/4$ for all sufficiently large $m$. Thus the ratios are +log-convex and attain their maximum at an endpoint. At $e=0$ the ratio is +$O(N^3/n)$, and at $e=\lfloor m/4\rfloor$ it is $n^{-1/2+o(1)}$. Both are +eventually below $1/2$, uniformly, so the series is geometrically decreasing. +\end{proof} + +\begin{lemma}[Global product over near-containment decorations] +Fix a typed full-containment table $L$ and temporarily distinguish every +endpoint cell occurrence. Let $\mathcal S(L)$ be the family obtained by +choosing for each occurrence either deficit $0$ or $1\le e0$ such that, eventually and uniformly, +\[ + \log_2\left[ + k_{co}^2g(j)\frac{(ea^2/m_0)^j}{j!} + \right] + \le-c_0(\log_2n)^2. + \tag{8.28a} +\] +Thus $\Xi_4=2^{-\Omega((\log n)^2)}$. +\end{lemma} + +\begin{proof} +Expand over distinct residual cells and threshold demands before dropping any +constraints. Lemma 6.2 gives (8.26a)--(8.27). Put $L_2=\log_2n$ and +$j=xL_2$. Then +\[ + 1+o(1)\le x\le3/2+o(1), + \qquad + \log_2m_0\ge L_2-6\log_2N. +\] +Using $g(j)\le2^{j^2/2}$ and $k_{co}\le n$, +\[ + \log_2\left[ + k_{co}^2g(j)\frac{(ea^2/m_0)^j}{j!} + \right] + \le2L_2+ + \left(\frac{x^2}{2}-x\right)L_2^2 + +O(L_2\log L_2). +\] +On $[1,3/2]$, $x^2/2-x\le-3/8$. Taking $c_0=1/4$, the lower-order term is +smaller than $L_2^2/8$ for all sufficiently large $n$, uniformly over the floor +perturbations and cell types. +\end{proof} + +\begin{lemma}[Small residual completion] +If $m_0 Date: Thu, 23 Jul 2026 11:42:30 +0300 Subject: [PATCH 05/29] Clarify residual majorant wording --- 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex index 4a273bbd..ff1f94e6 100644 --- a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex +++ b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex @@ -260,7 +260,7 @@ \section*{Replacement B: exact canonical exposure at the start of Section 8} capped residual local/cycle factor is postponed to Section 9. \end{definition} -When an unfinished high-cell completion is dominated below by the full +When an unfinished high-cell completion is bounded above by the full residual integrand, the latter is only a larger nonnegative numerical majorant. It does not redefine $\Bare(M,j)$, and the Section 9 residual factor is still applied exactly once. From 783adee0cd38c40325175c92573cc17947eafbaa Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 23 Jul 2026 11:44:10 +0300 Subject: [PATCH 06/29] Preserve the detailed Problem 625 README --- 625/README.md | 635 ++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 511 insertions(+), 124 deletions(-) diff --git a/625/README.md b/625/README.md index f278c5db..4196d1a3 100644 --- a/625/README.md +++ b/625/README.md @@ -1,128 +1,515 @@ -# Erdős Problem 625 candidate-proof dossier - -This directory contains a candidate full-sequence solution of Erdős Problem 625, -its publication artifacts, finite diagnostics, internal audits, and an -incremental Lean 4 formalization. - -## Status - -The current mathematical claim is a **candidate result**. It has undergone -substantial internal checking, but it has not been externally peer reviewed or -fully formalized. In particular: - -- the manuscript gives a self-contained proof of a polynomial-scale - chromatic--cochromatic gap for `G(n,1/2)`; -- the internal audits report no presently known blocking logical defect; -- finite computations are diagnostics only and are not proof of the asymptotic - theorem; -- the Lean development verifies many exact finite and asymptotic components, - but `Erdos625Statement` remains unproved. - -The accurate public description is therefore: - -> **Candidate full-sequence solution, internally audited, with a substantial -> partial Lean formalization; not external peer review and not a completed -> machine-checked proof.** - -## Start here - -- [Reviewer guide](REVIEW_GUIDE.md) -- [Canonical self-contained manuscript (Markdown)](proofs/COMPLETE_PROOF_SELF_CONTAINED.md) -- [Generated self-contained manuscript (TeX)](output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex) -- [Self-contained proof PDF](COMPLETE_PROOF_SELF_CONTAINED.pdf) -- [Publication-layout preprint PDF](arxiv_625.pdf) -- [Formalization ledger](formalization/FORMALIZATION_LEDGER.md) -- [Final internal verification record](FINAL_VERIFICATION.md) - -A review-focused rewrite of the most concentrated passages is available in -both formats: - -- [Markdown replacement text for Sections 7--9](proofs/SECTIONS_7_9_REVIEW_REWRITE.md) -- [TeX replacement text for Sections 7--9](proofs/SECTIONS_7_9_REVIEW_REWRITE.tex) - -These rewrite files preserve the current mathematical route while making the -partial-diagonal rate, canonical high-cell decomposition, high-skeleton sum, -and cycle-to-walk argument more explicit. They are proposed integration text, -not an additional independent proof verdict. - -## Exact target - -For `G_n ~ G(n,1/2)`, the manuscript claims +# Erdős Problem 625 research dossier + +## Complete proof + +**[Open the complete proof PDF](COMPLETE_PROOF_SELF_CONTAINED.pdf)** + +**[Open the publication-layout preprint PDF](arxiv_625.pdf)** + +The publication-layout PDF is dated 20 July 2026 and lists Samuil Petkov as +the sole author, with explicit AI-assistance, Aristotle-use, funding, and +competing-interests disclosures. It remains a candidate preprint while the +full Lean target is open. + +Its editable source, author--year bibliography, arXiv-ready `.bbl`, build +notes, and byte-identical PDF are collected in the [`arxiv/`](arxiv/) folder. + +The editable canonical manuscript is +[`proofs/COMPLETE_PROOF_SELF_CONTAINED.md`](proofs/COMPLETE_PROOF_SELF_CONTAINED.md), +and the generated TeX is +[`output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex`](output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex). + +## Supplementary exact example + +An [MP4 animation](assets/animations/erdos625-coloring-example.mp4) shows an +exact coloring and cochromatic partition of a fixed 12-vertex graph. It is an +illustrative example, not statistical or asymptotic proof evidence. + +## Lean formalization + +[`formalization/`](formalization/) contains the pinned Lean 4 formalization, +authored by **Samuil Petkov** and developed with disclosed AI assistance. The accepted project is checked +locally with Lean/mathlib `v4.31.0`. Raw Aristotle outputs remain quarantined; +only manually reviewed Lean 4.31 ports or reconstructions that pass the local +repository gates enter the accepted project. The verified closure includes +the labelled finite-graph and `G(n,1/2)` model, chromatic/cochromatic semantics, +exact phase and independent-set asymptotics, Boolean-cube and variable-block +bounded differences, induced-capacity amplification bricks, and finite +four-support entropy/optimizer continuity. + +For audit convenience, the generated +[`Erdos625SelfContained.lean`](formalization/Erdos625SelfContained.lean) +packages the current transitive local import closure into one Lean source +file; its regeneration and independent compile record are in +[`SELF_CONTAINED_BUILD.md`](formalization/SELF_CONTAINED_BUILD.md). This is a +single-file **partial checkpoint**, not a full formal proof of Sections 8--9 +or of `Erdos625Statement`. + +The Section 4 layer now proves the exact unordered profile enumeration and +first-moment formula (4.2), zero-safe factorial/log-weight bounds, the finite +`(n+1)^b` aggregate exponential estimate, and exact equivalence with the +expanded discrete profile objective. Natural profiles now embed exactly in +the constrained real profile space, and an abstract variational-envelope +theorem supplies the finite expectation interface. A zero-safe Gibbs +inequality gives an explicit one-parameter dual domination for positive +support and part count and is composed with the sharp shifted finite + probability bound. The Gibbs mean now has its two endpoint limits and a + unique interior target tilt; its positive optimizer exactly attains the fixed + finite real-profile maximum. The support is reindexed exactly by deficits + with normalized tilt `λ=B_α-t`, and the inverse, entropy, and part-count + envelope derivatives are kernel-checked. The exceptional top residual is + evaluated exactly and the full finite support has a pointwise Gaussian score + bound. Exact support reversal plus finite Gaussian-tail lemmas now give + explicit growing-support partition, first-moment, and second-moment envelopes + on every supplied bounded tilt interval, with a uniform denominator lower + bound from the zero-deficit atom. The limiting deficit Gaussian is defined + with summable moments through order two and a strictly positive partition; + its normalized mean has derivative equal to a strictly positive variance and + has endpoint limits `-1` and `+∞`. Hence every limiting target above `-1` + has a unique finite tilt and compact target intervals admit fixed brackets. +The final phase-cap squeeze interface is also kernel-checked. The layer +also constructs a nonempty kernel +partition from a coloring, refines it to exactly `k` parts, extracts the +bounded profile, and proves the deterministic event containment used in +(4.5), including all zero endpoints. Finite-space Markov and union bounds +then give the exact probability reduction and its conditional +`(n+1)^b exp(L)+μ(n,b+1)` form. + +The current Sections 6--8 checkpoint now includes the exact fixed-row ordered +overlap law (6.1)--(6.2), the uniform configuration-model prescribed-cell bound +(6.8), the effective +falling-factorial estimate (6.10), and the all-cases cellwise product bound +(6.9), including a proof that the excessive-total event is empty. The exact +partial-diagonal algebra, endpoint factorization, and recurrences (7.1)--(7.6) +are kernel-checked. Exact row and column margins of the configuration cell +table also instantiate the concrete high-cell matching assertion before +(8.2). Extending a fixed exposed witness is moreover equivalent to a bijection +of its unused stubs, with exact remaining cardinalities. The unused fibres +are now identified class-preservingly with standard residual stub types having +the exact residual degrees, so the fixed-witness extension subtype is +equivalent to the corresponding residual `ConfigurationMatching` space and +its uniform law pushes forward to the residual uniform law. Generic finite +uniform conditioning is also proved. The target-fibre and class-preservation +lemmas culminate in the exact per-cell fixed-witness identity +`full configurationCellCount = demand + residual configurationCellCount`. +The accepted cell-constraint module separately identifies `full = demand` +with residual count zero through a cap-free arithmetic lemma. Its packaged +configuration theorem assumes `hcap : demand a b <= cap` and returns that +equivalence together with `full <= cap` iff +`residual <= cap - demand`. High-skeleton cells use the zero branch; an +off-skeleton application of the unshifted residual cap first needs +`demand a b = 0`. These fixed-witness results do not by themselves select the +canonical high skeleton or package the constraints as the full Section 8 +conditional event. + +[`Section8FixedWitnessAssembly.lean`](formalization/Erdos625/Section8FixedWitnessAssembly.lean) +now composes those leaves for one fixed labelled witness: conditioning the +ambient uniform law on its extension event, transporting that law to the +residual configuration, splitting every full cell count as demand plus +residual count, and imposing the cap/no-additional-pair constraints +simultaneously. This is a fixed-witness seam theorem under its explicit +nonemptiness and `demand <= cap` hypotheses. It still does not select the +canonical high skeleton or estimate the probability of the canonical skeleton +event. + +[`Section8CanonicalSkeleton.lean`](formalization/Erdos625/Section8CanonicalSkeleton.lean) +now defines the deterministic canonical high demand and proves that its support +is a partial matching with exact on- and off-support values. It also proves +compatibility uniqueness after the selected fibres are fixed, that zero +residual mass makes a selected fibre the whole fibre, and an exact generic +translation of support-indexed cap/no-return constraints. The added theorem +`canonicalHighDemand_eq_iff_exact_support_and_capped_off` characterizes the +same cutoff by exact support values and the off-support `U/2` cap. +[`Section8CanonicalLabelledWitness.lean`](formalization/Erdos625/Section8CanonicalLabelledWitness.lean) +then proves `existsUnique_canonicalHighDemandWitness`: for one fixed +configuration matching, its literal canonical high-cell demand has a unique +labelled prescribed-demand witness extended by that matching. This is a +deterministic fixed-matching identification, not a count or probability for +the global canonical event. +[`Section8LabelledIncidence.lean`](formalization/Erdos625/Section8LabelledIncidence.lean) +proves `labelledWitnessIncidence_eq`, the normalized labelled-witness +descending-factorial identity, while +[`Section8NearSkeletonExpansion.lean`](formalization/Erdos625/Section8NearSkeletonExpansion.lean) +proves `sum_nearSkeletonChoiceWeight_eq_product` for distinguishable optional +deficit choices. These are deterministic/counting leaves. For a fixed demand, +the formalization also proves the exact finite canonical conditional-law +transport: under its strict high-demand and nonemptiness hypotheses, the +ambient conditional law is the uniform joint law of a labelled witness and a +residual-event fibre. With a reference witness this becomes a product law, +and the standardized residual coordinate has the uniform finite marginal. +The corresponding exact event-probability factorization is also proved as +labelled-witness incidence times the fixed residual-event probability. None +of these facts proves event nonemptiness or a quantitative skeleton estimate; +the unlabelled typed-skeleton multiplicity bridge, ratio bounds, and the +endpoint/near/middle estimates of Lemma 8.3 remain open. + +At the ambient level, +[`Section8CanonicalDemandGlobalResidual.lean`](formalization/Erdos625/Section8CanonicalDemandGlobalResidual.lean) +now decomposes every configuration matching by its attained canonical-demand +table, its labelled witness, and its demand-dependent residual event. It +transports the ambient uniform law to this dependent sigma space and proves +that a demand table has mass proportional to its exact fibre cardinality. It +also factors that fibre into its labelled-witness cardinality times one +demand-specific residual-fibre cardinality. It does not claim that demands +are uniformly distributed, that one residual law works across all demands, or +that any canonical event is likely. + +The companion marginal theorem states this directly as the labelled-witness +cardinality times that demand-specific residual-fibre cardinality, divided by +the ambient matching-space cardinality. + +[`Section9GlobalCanonicalResidualBridge.lean`](formalization/Erdos625/Section9GlobalCanonicalResidualBridge.lean) +then retypes every residual fibre by its literal Section 9 cap/no-return +event and transports the ambient uniform matching PMF exactly to the uniform +PMF on that tagged Section 9 sigma family. The attained demand and labelled +witness remain explicit tags, so this is not an untagged residual +distribution, conditioning statement, expectation bound, or asymptotic +estimate. + +For Section 9, restriction to the residual relation is proved injective for +even matrices supported on the union of that relation with a row matching, +giving a generic `2 ^ |R|` cardinal bound. Finite bipartite edge sets now have +an injective zero-one incidence-matrix encoding over `ZMod 2`, with matrix +parity equivalent to even row and column fibres. The number of cells of an +actual configuration matching with multiplicity at least two is at most the +total row-stub count divided by two. The explicitly defined actual residual +even-edge family is now connected to the generic restriction theorem, giving +the precise `2 ^ |R|` support bound, and the division-free finite choose-two +mass estimate (9.21) is proved. It also has an exact one-sided `ENNReal` +weighted embedding into the finite sum over all even bipartite edge sets, for +arbitrary cell weights. This is a subfamily comparison, not an `ENNReal` +polymer estimate. The finite forest-plus-residual-edge +cycle-rank inequality in (9.20) is also kernel-checked, including its literal +configuration-support and `m₀ / 2` forms. The exact finite binary cycle-space +cardinality, a recoverable real-valued minimal-even polymer decomposition, and +the abstract row-norm/geometric traversal kernel are also proved. The accepted +[`Section9MatchingTraversalBridge.lean`](formalization/Erdos625/Section9MatchingTraversalBridge.lean) +adds the relaxed finite matching-operator/walk-mass bridge: matching traversal +preserves the residual row bound, oriented starts cost exactly `2 * |M|`, and +the finite block-walk sum has the stated geometric bound. It does not build +the positive residual kernel from `q` or an injective, weight-preserving +cycle-to-walk encoding. The exact finite subfamily embedding is checked, but +an `ENNReal` polymer bound, the cycle-to-walk weight transfer, instantiation +of the accepted eventual-`tau` bridge, +the finite attachment estimates, and the global Lemma +9.1/Proposition 9.2 +assembly remain open. Aristotle is used only for redundant +isolated candidate generation; reviewed local Lean 4.31 source is +authoritative. +The capped degree moments and exact theta factorizations/bounds behind +(9.13)--(9.14) are also kernel-checked. The literal residual `q` now has a +finite degree-cap row/column norm bound, and hence its symmetric bipartite +cell kernel has the corresponding row norm; this still supplies neither a +conditioned residual law nor a cycle-to-walk encoding. + +[`Section9EncodingAssembly.lean`](formalization/Erdos625/Section9EncodingAssembly.lean) +packages the generic counting seam. An explicit injective even-matrix +encoding supported on a row matching together with a residual relation gives +the bound `2 ^ |R|`; when that residual relation is the actual configuration +support already bounded above, the exponent is at most half the row-stub +count. These are conditional cardinality theorems under the displayed +encoding, evenness, and support hypotheses. +[`Section9ActualResidualFamily.lean`](formalization/Erdos625/Section9ActualResidualFamily.lean) +discharges those encoding/evenness/support hypotheses for the literal finite +family of even edge sets supported on the high matching or multiplicity-at- +least-two cells. [`Section9ActualResidualWeightedEmbedding.lean`](formalization/Erdos625/Section9ActualResidualWeightedEmbedding.lean) +then proves its exact one-sided weighted `ENNReal` inclusion into the all-even +finite sum; it does not turn the separate real polymer theorem into an +`ENNReal` theorem. [`Section9ChooseTwoMass.lean`](formalization/Erdos625/Section9ChooseTwoMass.lean) +proves (9.21) in a division-free form, while +[`Section9CycleRankResidual.lean`](formalization/Erdos625/Section9CycleRankResidual.lean) +proves that a matching plus a residual relation has cycle rank at most the +number of residual cells. +[`Section9CycleRankConfigurationAssembly.lean`](formalization/Erdos625/Section9CycleRankConfigurationAssembly.lean) +identifies the literal residual-support finset and proves the full finite chain +`cycleRank ≤ |E(H_res)| ≤ m₀ / 2`. A separate accepted real-valued polymer +theorem constructs a recoverable disjoint minimal-even decomposition. The +actual family has the one-sided finite weighted embedding above, but an +`ENNReal` polymer specialization, concrete cycle-to-walk encoding and +weight/kernel transfer, instantiation of the accepted eventual-`tau` bridge, +attachment bound, and final Section 9 assembly +remain open; the exact binary cycle-space count and abstract traversal kernel +are proved below. + +[`Section9SmallResidualDeterministic.lean`](formalization/Erdos625/Section9SmallResidualDeterministic.lean) +proves the finite arithmetic conclusion (9.22). Given the literal +cap/no-return table event, the exact demand-plus-residual split, residual mass, +and the separated cycle-rank estimate, it bounds the component factor times +the complete local sign-reward product by `2^(U*m₀/2)`. It does not yet +identify the conditioned random residual table or close the full attachment +expectation in Lemma 9.1. + +[`Section9CycleSpaceCardinality.lean`](formalization/Erdos625/Section9CycleSpaceCardinality.lean) +proves the exact binary cycle-space count: finite even edge subsets are +equivalent to the `ZMod 2` incidence kernel and number exactly +`2 ^ cycleRank`. [`Section9TraversalKernel.lean`](formalization/Erdos625/Section9TraversalKernel.lean) +proves the finite row-norm walk estimate, the one-time marked-start factor, and +the positive/even geometric tails behind (9.16)--(9.18). What remains is the +actual-family specialization and cycle-to-walk encoding, the concrete +weight/kernel transfer and attachment assembly. + +[`Section9CappedFixedFExpansion.lean`](formalization/Erdos625/Section9CappedFixedFExpansion.lean) +proves the faithful capped/no-return prescribed-demand expansion for one fixed +`F`. [`Section9CyclePolymerBound.lean`](formalization/Erdos625/Section9CyclePolymerBound.lean) +constructs the recoverable disjoint minimal-even decomposition and proves the +finite real polymer product/exponential bound. +[`Section9FiniteAnalyticEndpoint.lean`](formalization/Erdos625/Section9FiniteAnalyticEndpoint.lean) +proves one absolute-constant finite real endpoint bound for `lambda` and `q` +under its exact hypotheses. These modules do not themselves supply an +`ENNReal` polymer bound for the actual residual family, build the required +cycle-to-walk code, or supply the upstream random event. + +[`Section9RewardTelescoping.lean`](formalization/Erdos625/Section9RewardTelescoping.lean) +proves `cappedReward_telescoping`, the exact capped reward identities under +`r <= R`. [`Section9FiniteFamilyAlgebra.lean`](formalization/Erdos625/Section9FiniteFamilyAlgebra.lean) +proves `finiteInjectiveFamily_product_exp_bound` under explicit injectivity and +pointwise nonnegative product bounds. +[`Section9AttachmentAsymptotics.lean`](formalization/Erdos625/Section9AttachmentAsymptotics.lean) +proves `eventually_tau_lt_one_third` from the stated large-residual profile +inequalities and `exists_uniform_twoRegime_error` from assumed large-/small- +residual attachment estimates. It does not supply the required cycle-to-walk +and weight encodings, those upstream finite estimates, the conditioned probability +bound, or the global Section 9 assembly. + +The newest Sections 10--11 checkpoint adds eight accepted source units. +[`QuarterDensityDegree.lean`](formalization/Erdos625/QuarterDensityDegree.lean) +proves both the fixed-size-to-larger quarter-density lift and the high-degree +vertex step, and +[`QuarterRecurrence.lean`](formalization/Erdos625/QuarterRecurrence.lean) +proves the exact real recurrence (10.3a). +[`Section11EventAssembly.lean`](formalization/Erdos625/Section11EventAssembly.lean) +proves two pointwise threshold-intersection inclusions, including the explicit +constant and strict-event `+1`. +[`Section10AmplificationScales.lean`](formalization/Erdos625/Section10AmplificationScales.lean) +proves growth of the chosen radius together with the seed, transformed-radius, +real cube-root, and additive-constant little-o terms on the +`n/(log n)^3` scale. Its `amplificationError_isLittleO_gapBase` now assembles +the exact displayed deterministic error from those four components. +[`Section11AsymptoticAssembly.lean`](formalization/Erdos625/Section11AsymptoticAssembly.lean) +proves the generic full-sequence intersection, eventual threshold, and scale- +divergence lemmas. Its `fixedThreshold_tail_of_movingThreshold` proves the +generic implication from an assumed diverging moving tail to every fixed +threshold, including for `n`-dependent sample spaces. +[`Section10QuarterUnionDecay.lean`](formalization/Erdos625/Section10QuarterUnionDecay.lean) +proves `quarterDensity_unionBound_tendsto_zero`, the full-sequence deterministic +union-cost decay at +`u₀ = ceil(n^(1/4))`, while +[`Section10ComplementInvariance.lean`](formalization/Erdos625/Section10ComplementInvariance.lean) +proves that graph complementation preserves the ambient finite `G(n,1/2)` law +exactly. This symmetry does not provide the still-missing fixed induced- +restriction pushforward. +[`Section10SimultaneousGreedyColoring.lean`](formalization/Erdos625/Section10SimultaneousGreedyColoring.lean) +proves `simultaneous_induced_chromatic_bound`, the internal-`forall U` greedy +chromatic bound from one graph-uniform independent-block hypothesis. These +atoms do not prove the random event +supplying that hypothesis, Lemma 10.1, Lemma 10.2, the actual Section 11 +sequence/tail instantiation, or the final theorem. The exact remaining DAG, +quantifier order, and the declaration-scoped Aristotle request ledger are +recorded in the +[`Sections X--XI breakdown`](formalization/SECTIONS_10_11_BREAKDOWN_2026-07-14.md). + +The newly named Section 8--11 leaves have local Lean 4.31 warning-fatal builds. +This is statement-scoped acceptance of their deterministic, algebraic, or +conditional content, not completion of a manuscript section or the target. + +[`Section10_11ConditionalAssembly.lean`](formalization/Erdos625/Section10_11ConditionalAssembly.lean) +adds three auditable seams: the rounded capacity-deficit tail from explicit +seed, rounding, and radius hypotheses; a single leftover-colouring event whose +definition contains the required internal `forall W`; and the conditional +implication `erdos625Statement_of_capacity_leftover_thresholds`. The latter +assumes `hCapacityTail`, `hLeftoverTail`, `hChromaticTail`, +`hCochromaticThreshold`, and `hGapThreshold`. It is therefore **not** a proof +of `Erdos625Statement`; the corresponding probabilistic tails and concrete +threshold comparisons must still be established. + +The asymptotic target is deliberately recorded as an **unproved proposition**; +the current development is a verified partial formalization, not a completed +Lean proof of the manuscript. Growing-support moments, compact-uniform +optimizer-tilt convergence, variance stability, and generic root/rounding +interfaces are kernel-checked. In Section 4, the concrete phase objective, +its center/slope corridor, its integer decrement, and the resulting probability +limit remain open; the +signed first-moment certificate, unordered/sign-summed overlap assembly, asymptotic +partial-diagonal ranges, manuscript-specific specialization of the exact +fixed-demand canonical conditional law and probability factorization, the +skeleton quotient/estimates, and full Section 8 assembly, actual-family and +`ENNReal` polymer/weight specialization beyond the proved one-sided subfamily +inclusion, concrete +cycle-to-walk encoding and weight transfer, finite residual attachment and +conditioned probability control, and full Section 9 assembly, Section 10's +simultaneous leftover tail and concrete +seed-amplification instantiation, and Section 11's actual chromatic tail and +threshold/limit instantiation also remain open. +See the [`formalization ledger`](formalization/FORMALIZATION_LEDGER.md) for the +declaration-by-declaration status and remaining dependency graph. Reproduced +milestone evidence is recorded in the audit files under +[`formalization/`](formalization/); the latest growing-support, compact-tilt, +variance, and root-interface checkpoint is the +[`M7 audit`](formalization/M7_GROWING_SUPPORT_TILT_CORRIDOR_AUDIT_2026-07-14.md). The +complete dependency/import policy is in +[`DEPENDENCY_REPRODUCIBILITY.md`](formalization/DEPENDENCY_REPRODUCIBILITY.md). +The current Sections 6--9 atomization, Aristotle quarantine status, and exact +non-atomic obligations are tracked in the +[`Sections 6--9 breakdown`](formalization/SECTIONS_6_9_BREAKDOWN_2026-07-14.md). +The simultaneous-leftover, amplification, and final event/limit obligations +are tracked separately in the +[`Sections X--XI breakdown`](formalization/SECTIONS_10_11_BREAKDOWN_2026-07-14.md). + +## Current status + +`proofs/COMPLETE_PROOF_SELF_CONTAINED.md` contains a proposed all-`n` positive +resolution with the explicit bound \[ - \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. + \chi(G(n,1/2))-\zeta(G(n,1/2)) + \ge \frac{(\ln2)^2\ln(200/153)}{32} + \frac{n}{(\ln n)^3} + \quad\text{with high probability}. \] -Here `chi` is the chromatic number and `zeta` is the cochromatic number. - -## Artifact map - -### Canonical proof - -- `proofs/COMPLETE_PROOF_SELF_CONTAINED.md` is the editable canonical - mathematical manuscript. -- `output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex` is the generated TeX source. -- `COMPLETE_PROOF_SELF_CONTAINED.pdf` is the compiled internal-layout PDF. - -### Publication package - -- `arxiv/` contains the publication-layout source, bibliography, build notes, - and compiled PDF. -- `arxiv_625.pdf` is the top-level publication-layout PDF. -- `../arxiv_preprints/arxiv_625/` contains the synchronized public preprint - package. - -### Audits and diagnostics - -- `audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md` records the later adversarial - review and the repairs made after the original full-chain audits. -- `FINAL_VERIFICATION.md` records artifact synchronization, diagnostic runs, - scope limitations, and hashes. -- `verification/erdos625_independent_checks.py` checks selected exact finite - identities and inequalities. -- `experiments/` contains finite examples and asymptotic diagnostics. None of - these computations substitutes for proof. - -### Lean formalization - -- `formalization/Erdos625/Target.lean` defines the exact probability target. -- `formalization/FORMALIZATION_LEDGER.md` is the authoritative declaration-level - status record. -- `formalization/Erdos625SelfContained.lean` is a generated single-file form of - the accepted import closure. -- `formalization/SELF_CONTAINED_BUILD.md` records regeneration, compilation, - and axiom checks. - -The single-file checkpoint is a **partial formalization**. Successful -compilation does not prove the manuscript theorem unless the ledger records a -proved final endpoint. - -## Review priorities - -The most valuable independent checks are concentrated in four places: - -1. the uniform root and optimizer corridor in Section 3; -2. the complete partial-diagonal rate in Lemma 7.1; -3. the conditioned canonical high-skeleton expansion in Section 8; -4. the weighted residual cycle expansion and mixed-cycle traversal in - Lemma 9.1. - -The reviewer guide gives exact entry points and a checklist for each. - -## Trust and provenance - -The manuscript names Samuil Petkov as sole author and discloses AI assistance. -Raw proof-search outputs are not treated as authoritative. Only reviewed Lean -source that passes the repository's placeholder, axiom, warning, and build -gates enters the accepted formalization. - -Internal documents labelled `PASS` are scoped to the bytes and dates stated in -those documents. They are not external peer review, professional -certification, bibliographic priority verification, or community acceptance. - -## Licensing - -See [`../LICENSE_SCOPE.md`](../LICENSE_SCOPE.md) for the scope of the repository -license and the treatment of third-party material. +The decisive overlap components passed focused independent audits, and four +independent end-to-end reconstructions each returned PASS. A fresh +severity-ranked adversarial review on 2026-07-13 then found a circular signed- +root localization in the written proof, an unstated globalization step in the +high-skeleton sum, and a one-sided/two-sided overclaim in the residual lemma. +All three were repaired without changing the theorem or constant, and three +independent regression reviews returned PASS on the corrected passages. See +[`audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md`](audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md). +The concise draft and the focused first-moment, dense-overlap, residual, and +amplification notes were subsequently synchronized to those repairs. Their +cross-document mapping is recorded in +[`audits/PROOF_COMPONENT_SYNCHRONIZATION_AUDIT_2026-07-13.md`](audits/PROOF_COMPONENT_SYNCHRONIZATION_AUDIT_2026-07-13.md). +This is internal validation of a new argument, not external peer review, +publication, priority confirmation, or community acceptance. + +A further user-supplied review dated 2026-07-12 reports **provisional internal +verification: PASS** and no blocking mathematical error. Its separately +written checker reproduces five groups of finite diagnostic tests from +Sections 6 and 8. The report, checker, reproduced output, provenance, and +limitations are indexed in [`verification/`](verification/). This is +additional internal evidence, not external peer review or machine +verification, and the finite tests do not prove the asymptotic theorem. + +As of 2026-07-12, the [public Problem 625 page](https://www.erdosproblems.com/625) +still labels the problem `OPEN`. This repository presents a proposed +resolution for scrutiny and does not claim an official status change. + +The current complete packaged dossier is available at +[`releases/Erdos-625-complete-dossier-2026-07-14.zip`](releases/Erdos-625-complete-dossier-2026-07-14.zip). +It includes the arXiv source library and the pinned Lean source project while +excluding local build/service caches and copyrighted historical-source PDFs. + +## Publication artifacts + +The canonical dossier manuscript attributes co-authorship to **Samuil Petkov +& ChatGPT 5.6**. The separate publication-layout preprint lists **Samuil +Petkov** as author and gives explicit AI-assistance and ethics disclosures. + +- [`COMPLETE_PROOF_SELF_CONTAINED.pdf`](COMPLETE_PROOF_SELF_CONTAINED.pdf) + - top-level convenience copy for immediate viewing on GitHub; byte-identical + to the compiled PDF under `output/pdf/`. +- [`proofs/COMPLETE_PROOF_SELF_CONTAINED.md`](proofs/COMPLETE_PROOF_SELF_CONTAINED.md) + - canonical self-contained Markdown manuscript. +- [`output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex`](output/tex/COMPLETE_PROOF_SELF_CONTAINED.tex) + - generated standalone TeX source with color-coded lemma/proposition boxes. +- [`output/pdf/COMPLETE_PROOF_SELF_CONTAINED.pdf`](output/pdf/COMPLETE_PROOF_SELF_CONTAINED.pdf) + - compiled 30-page A4 PDF with proofs kept outside the statement boxes. +- [`output/README.md`](output/README.md) - build versions, hashes, and PDF QA. +- [`arxiv/`](arxiv/) - publication-layout TeX, bibliography, `.bbl`, build + notes, and compiled 35-page preprint. +- [`arxiv_625.pdf`](arxiv_625.pdf) - top-level convenience copy of the + publication-layout preprint. + +## Proof authority and synchronized support + +`proofs/COMPLETE_PROOF_SELF_CONTAINED.md` is the sole authoritative proof. +The TeX and PDF are generated publication forms of that manuscript. The +component notes below retain focused derivations and route history; they have +been synchronized to the 2026-07-13 repairs but are supporting explanations, +not a second proof whose wording overrides the canonical manuscript. If a +future discrepancy appears, the canonical manuscript controls and the +discrepancy must be logged. + +- `proofs/COMPLETE_PROOF_DRAFT.md` — concise synchronized map of the theorem + and its proof obligations. +- `proofs/ALPHA_MINUS_TWO_ROUTE.md` — synchronized support for the uniform + root corridor, first-moment comparison, explicit constants, unrestricted + chromatic lower location, and tangent-rounded integer profile. +- `proofs/FOUR_SIZE_PARTIAL_RATES.md` — exact common-diagonal sum `1+o(1)`. +- `proofs/DENSE_FOUR_TYPE_MATCHING.md` — synchronized support for all + unequal-type containments, near-containments, the mixed middle strip, and + the conditioned global sum over high skeletons. +- `proofs/RESIDUAL_ATTACHMENT.md` — synchronized one-sided upper bound for + residual local and even-subgraph attachments after the large-cell matching + is exposed. +- `proofs/ALON_CONCENTRATION_EXTENSION.md` — synchronized rare-event-to-whp + transfer with the growing deterministic error/failure sequence used in the + final event intersection. + +## Independent audits + +- `audits/ADVERSARIAL_LEAP_AUDIT_2026-07-13.md` — severity-ranked fresh + audit, repair register, and independent regression results; internal pass + after revision. +- `audits/PROOF_COMPONENT_SYNCHRONIZATION_AUDIT_2026-07-13.md` — traceability + matrix confirming that the focused component notes reflect those repairs; + no change to the canonical TeX/PDF content. +- `audits/RARE_EVENT_AMPLIFICATION_AUDIT.md` — pass. +- `audits/RESIDUAL_ATTACHMENT_AUDIT.md` and + `audits/DENSE_FOUR_TYPE_MATCHING_AUDIT.md` — preserved internal 2026-07-12 + verdicts on the earlier component bytes; their top notices delimit scope. +- `audits/FULL_PROOF_AUDIT_1.md` through `_4.md` — preserved independent + 2026-07-12 reconstructions; all four passed the bytes then reviewed, and + their top notices make clear that they are not reviews of later bytes. +- `verification/erdos625_verification_report.md` — additional provisional + internal verification; pass, with formalization targets identified. +- `verification/erdos625_independent_checks.py` — separately written finite + diagnostic checker; all five supplied check groups pass. + +## Literature and known results + +- `sources/SOURCE_LEDGER.md` +- `sources/RECENT_WORK_AUDIT.md` +- `sources/HISTORICAL_SOURCE_AUDIT.md` +- `sources/ERDOS625_REFERENCES.bib` -- reusable BibTeX for every reference + cited in the canonical manuscript. +- `proofs/KNOWN_RESULTS_RECONSTRUCTION.md` +- `proofs/EXCEPTIONAL_REGIME.md` + +The ledger records every source version and probability quantifier. Every +historical Problem 625 source cited in the manuscript has been checked directly +for the claim attributed to it, with pages and SHA-256 identifiers recorded in +the historical audit. Bibliographic metadata for the standard bounded- +differences and concentration references was verified against the publisher +and arXiv records. The copyrighted PDFs remain local and are not redistributed +in this repository or its release archives. + +## Reproducibility + +- `experiments/alpha_minus_two_route.py` — phase-uniform entropy losses and + certified constants. +- `experiments/dense_transport_scan.py` — exact finite falling-factorial + diagnostics for dense typed transports. +- `experiments/constrained_profile_certify.py` and + `experiments/finite_slack_profile.py` — exceptional-profile calculations. +- `experiments/exact_chi_zeta.py`, CSV, and report — certified finite graph + computations (diagnostic only). +- `experiments/render_erdos625_animation.py` — deterministic GIF/MP4 renderer + that revalidates the fixed graph and its exact partition witnesses before + producing the supplementary animation artifacts. + +`WORK_LOG.md` and `MECHANISM_REGISTRY.md` record the investigation history, +failed routes, redirections, and precise remaining status. +`FINAL_VERIFICATION.md` records the full audit history, the 2026-07-13 +adversarial repairs and regression results, the 2026-07-14 publication and +Lean-checkpoint refresh, the additional user-supplied verification, +reproducibility checks, final hashes, and the completed historical-source +audit. + +## Citation and license + +The original repository material is licensed under +[CC BY 4.0](../LICENSE). When the license requires attribution, credit +**Samuil Petkov** and follow the repository-level +[scope and attribution notice](../LICENSE_SCOPE.md). Scholarly citation +metadata are provided in [`CITATION.cff`](../CITATION.cff). From a0fc394dacc0f8f3d550292b0b0f87ff125b2b21 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 18:06:27 +0300 Subject: [PATCH 07/29] Simplify the residual attachment bound --- 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md | 203 ++++++++++------------ 1 file changed, 94 insertions(+), 109 deletions(-) diff --git a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md index 83fec536..8148649f 100644 --- a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md +++ b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md @@ -73,7 +73,7 @@ For with the convention \(0\ln0=0\), one has \[ - \Phi_T(z)\le-\frac{Y}{5000} + \Phi_T(z)\le-\frac{Y}{100} \qquad\text{whenever}\qquad \frac1{64}\le R\le1. \tag{7.21a} @@ -107,16 +107,16 @@ First suppose \(1/64\le R\le47/100\). Since \(T\ge2/q\), The function \[ - f(R)=R\{\ln R+5q/2-1\}+\frac{1-R}{5000} + 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.053, + f(1/64)<-0.0436, \qquad - f(47/100)<-0.010, + f(47/100)<-0.0051, \] so \(f(R)<0\) throughout the interval. @@ -133,16 +133,15 @@ Now suppose \(47/100\le R\le1\). Since Set \[ - h(R)=R\ln R+(1-q/2+1/200)(1-R). + 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.0058\). Convexity therefore places \(h\) below the chord joining +\(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}{200} - \le-\frac{1-R}{5000}. + \Phi_T(z)\le-\frac{1-R}{100}. \] Combining the two ranges proves (7.21a). \(\square\) @@ -163,7 +162,7 @@ therefore give \[ \ln D(\ell) - \le-\frac{k_{co}\alpha Y}{5000} + \le-\frac{k_{co}\alpha Y}{100} +Ck_{co}Y\ln(e/Y)+CN. \tag{7.24a} \] @@ -535,150 +534,136 @@ no-further-near-cell event. --- -## Replacement block D: finite cycle expansion in Lemma 9.1 +## Replacement block D: residual-restriction product bound in Lemma 9.1 -Replace the compressed discussion surrounding equations (9.15)--(9.18) by the -following lemmas. +Replace the cycle decomposition and traversal discussion surrounding equations +(9.15)--(9.18) by the following two finite lemmas. -### Lemma 9.1A (even subgraphs to a simple-cycle product) +### Lemma 9.1A (an even matching completion is unique) -Let \(G\) be a finite graph with nonnegative edge weights \((w_e)\). For every -even edge set \(F\), fix deterministically an edge-disjoint decomposition -\(\mathcal D(F)\) into simple cycles. Then +Let \(M\) be a matching and let \(R\) be any finite residual edge set. Write \[ - \sum_{F\text{ even}}\prod_{e\in F}w_e - \le - \prod_{C\text{ simple cycle}} - \left(1+\prod_{e\in C}w_e\right) - \le - \exp\left\{\sum_{C\text{ simple cycle}}\prod_{e\in C}w_e\right\}. - \tag{9.15a} + \mathcal C_{\rm even}(M,R) + =\{F\subseteq M\cup R:\deg_F(v)\text{ is even for every }v\}. \] -#### Proof - -Because the cycles in \(\mathcal D(F)\) are edge-disjoint, they are distinct, -and +Then the restriction map \[ - \prod_{e\in F}w_e - =\prod_{C\in\mathcal D(F)}\prod_{e\in C}w_e. + \rho:\mathcal C_{\rm even}(M,R) + \longrightarrow\mathcal P(R\setminus M), + \qquad + \rho(F)=F\setminus M, + \tag{9.15a} \] -The map \(F\mapsto\mathcal D(F)\) is injective after forgetting the chosen -ordering, since the union of the cycles recovers \(F\). Dropping the -disjointness condition enlarges the image to all subsets of the finite set of -simple cycles. Summing over those subsets gives the first product, and -\(1+x\le e^x\) gives the second inequality. \(\square\) +is injective. + +#### Proof + +Suppose \(\rho(F)=\rho(F')\). Then the symmetric difference +\(F\mathbin\triangle F'\) is contained in \(M\). It is also even, because +symmetric difference preserves vertex parity. A nonempty subset of a matching +has degree one at every incident vertex, and therefore cannot be even. Hence +\(F\mathbin\triangle F'=\varnothing\), so \(F=F'\). \(\square\) -Apply the lemma to \(G=M\cup R\), with matching-edge weight one and residual -edge weight \(q_e\). This gives equation (9.15) with no implicit multiplicity -factor. +Equivalently, once the residual edges are specified, parity forces every +matching edge that can occur. Some residual subsets have no even completion, +but none has two. -### Lemma 9.1B (cycles disjoint from the high matching) +### Lemma 9.1B (weighted restriction product) -Let \(Q\) be the symmetric weighted adjacency kernel of the residual bipartite -graph, with edge weights \(q_e\). If every row and column sum is at most -\(\tau<1\), then +Let \(q_e\ge0\) for residual edges and put \(q_e=0\) on \(M\). Then \[ - \sum_{C:C\cap M=\varnothing}\prod_{e\in C}q_e - \le - \frac{n\tau^4}{1-\tau^2}. - \tag{9.16} + \begin{split} + \sum_{F\in\mathcal C_{\rm even}(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). + \end{split} + \tag{9.15b} \] #### Proof -A residual-only bipartite cycle has even length \(2s\ge4\). Mark one row -vertex on the cycle, forget simplicity, and forget the closing constraint. -For each marked row start, the total mass of all length-\(2s\) walks is at most -\(\tau^{2s}\) by repeated use of the row-sum norm. There are at most \(n\) -possible marked row starts. Therefore +Apply Lemma 9.1A and enlarge the image of \(\rho\) to the full power set. The +middle identity is the finite subset-product expansion, and the last inequality +uses \(1+x\le e^x\). \(\square\) -\[ - \sum_{C:C\cap M=\varnothing}\prod_{e\in C}q_e - \le n\sum_{s\ge2}\tau^{2s} - =\frac{n\tau^4}{1-\tau^2}. -\] +The two finite ingredients are already represented in the Lean development by +`residualRestriction_injective` and +`finiteInjectiveFamily_product_exp_bound`. -The marking may count a cycle more than once, which is harmless for an upper -bound. \(\square\) - -### Lemma 9.1C (cycles meeting the high matching) +### Completion of the large-residual branch -Let \(M\) be a bipartite matching of size \(h\). Let \(Q\) be a nonnegative -symmetric residual kernel on the same row and column vertex sets, zero on -\(M\), with row-sum norm at most \(\tau<1/3\). Put +Equation (9.12) and Lemma 9.1B give \[ - P=Q+Q^2+Q^3+\cdots, - \qquad - b=\|P\|_{\infty} - \le\frac{\tau}{1-\tau}. - \tag{9.17a} + \mathcal A(M,j) + \le\exp\left(\Lambda_0+\sum_e q_e\right). + \tag{9.16} \] -Then +By (9.6), \[ - \sum_{C:C\cap M\ne\varnothing}\prod_{e\in C\setminus M}q_e - \le2h\sum_{r\ge1}b^r - =\frac{2hb}{1-b} - \le C h\tau. - \tag{9.18a} + \sum_e q_e + =\frac12\sum_{a,b}\theta_{ab}^2+\Lambda_0. + \tag{9.17} \] -#### Proof - -Fix a total order on the oriented matching edges. For every simple cycle that -meets \(M\), mark the least oriented matching edge occurring on that cycle. -This costs at most \(2h\) choices and removes rotation and orientation -ambiguity. - -Suppose the cycle uses \(r\ge1\) matching edges. Cutting the cycle at all of -those edges leaves \(r\) nonempty residual paths. Encode each path by its -ordered sequence of residual vertices. Between consecutive residual paths, -the next matching edge is determined by the current endpoint because \(M\) is -a matching. Thus matching traversal is a partial permutation operator of -row-sum norm one; it introduces no new factor \(h\). +The square sum factorizes exactly: -After dropping simplicity, vertex-disjointness, and the final closing -constraint, the total mass of the first residual path is at most \(b\), and the -same is true after every deterministic matching transition. Hence the total -mass of relaxed codes with exactly \(r\) matching edges is at most -\(2h b^r\). Summing over \(r\ge1\) proves (9.18a). \(\square\) - -### Completion of the large-residual branch +\[ + \sum_{a,b}\theta_{ab}^2 + =\frac{e^2}{m_0^2} + \left(\sum_a d_a^2\right) + \left(\sum_b(d'_b)^2\right). + \tag{9.18} +\] -Equations (9.12)--(9.14) give +Every residual degree is at most \(U\), and both degree sums equal \(m_0\). +Consequently \[ - \Lambda_0\le C U^4/m_0, + \sum_a d_a^2\le Um_0, \qquad - \tau\le C U^3/m_0. + \sum_b(d'_b)^2\le Um_0, + \qquad + \sum_{a,b}\theta_{ab}^2\le e^2U^2. + \tag{9.18a} \] -For \(m_0\ge n/N^6\), one has \(\tau<1/3\) eventually, uniformly over every -feasible canonical skeleton. Lemmas 9.1A--9.1C and \(h<2n/U\) therefore yield +Combining this with (9.13) yields the uniform one-sided bound \[ + \boxed{ \mathcal A(M,j) \le - \exp\left[ - C\left\{ - \frac{U^4}{m_0} - +n\tau^4 - +h\tau - \right\} - \right] - \le\exp(C'N^8). + \exp\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} \tag{9.19} \] -This is a one-sided bound. No lower estimate for \(\mathcal A(M,j)\) is used -or asserted. +If \(m_0\ge n/N^6\), then \(U=O(N)\) and +\(U^4/m_0=O(N^{10}/n)=o(1)\). Thus + +\[ + \mathcal A(M,j)\le\exp(C'N^2) + =\exp\{o(n/N^4)\}, + \tag{9.19a} +\] + +uniformly over every feasible canonical skeleton. + +This argument removes the simple-cycle decomposition, residual-only walk sum, +mixed matching-cycle encoding, the parameter \(\tau\), and the factor +\(h\tau\). It is deliberately coarser than the bounded-cell estimate in the +separate overlap note, but it is far sharper than needed for Proposition 9.2. +No lower estimate for \(\mathcal A(M,j)\) is asserted or used. --- @@ -690,7 +675,7 @@ When incorporating these blocks into the canonical Markdown and generated TeX: paragraph leading to (7.25); 2. insert Proposition 8.0 and Definition 8.0A immediately after (8.3); 3. replace the current Lemma 8.3 by Lemmas 8.3A--8.3D and Proposition 8.4; -4. insert Lemmas 9.1A--9.1C between (9.14) and the large-residual conclusion; +4. replace the cycle/traversal passage by Lemmas 9.1A--9.1B and the global square-sum estimate; 5. rename the two unrelated uses of `B_n`; 6. regenerate the TeX and PDFs from the canonical source; 7. rerun display-tag, citation, finite-diagnostic, and formalization-status From 6ad62e5755f52be4004961e7ecf14f069bbaef53 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 18:09:02 +0300 Subject: [PATCH 08/29] Synchronize the simplified residual attachment proof --- 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex | 170 ++++++++++----------- 1 file changed, 78 insertions(+), 92 deletions(-) diff --git a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex index ff1f94e6..14077ab0 100644 --- a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex +++ b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex @@ -72,7 +72,7 @@ \section*{Replacement A: the central rate in Lemma 7.1} \] with $0\ln0=0$, one has \[ - \Phi_T(z)\le-\frac{Y}{5000} + \Phi_T(z)\le-\frac{Y}{100} \qquad\text{whenever}\qquad \frac1{64}\le R\le1. \tag{7.21a} @@ -99,14 +99,14 @@ \section*{Replacement A: the central rate in Lemma 7.1} \] The function \[ - f(R)=R\{\ln R+5q/2-1\}+\frac{1-R}{5000} + 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.053, + f(1/64)<-0.0436, \qquad - f(47/100)<-0.010, + f(47/100)<-0.0051, \] so $f(R)<0$ throughout the interval. @@ -119,14 +119,13 @@ \section*{Replacement A: the central rate in Lemma 7.1} \] Set \[ - h(R)=R\ln R+(1-q/2+1/200)(1-R). + h(R)=R\ln R+(1-q/2+1/100)(1-R). \] This function is convex, $h(1)=0$, and direct evaluation gives -$h(47/100)<-0.0058$. Convexity therefore places $h$ below the chord joining +$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}{200} - \le-\frac{1-R}{5000}. + \Phi_T(z)\le-\frac{1-R}{100}. \] \end{proof} @@ -141,7 +140,7 @@ \section*{Replacement A: the central rate in Lemma 7.1} the selected mass satisfies $Y\ge\eta/2$. Equation (7.20) and the lemma give \[ \ln D(\ell) - \le-\frac{k_{co}\alpha Y}{5000} + \le-\frac{k_{co}\alpha Y}{100} +Ck_{co}Y\ln(e/Y)+CN. \tag{7.24a} \] @@ -423,113 +422,101 @@ \section*{Replacement C: split form of Lemma 8.3} expansion under the no-further-near-cell event. Hence every multiplicity is included exactly once. -\section*{Replacement D: finite cycle expansion in Lemma 9.1} +\section*{Replacement D: residual-restriction product bound in Lemma 9.1} -\begin{lemma}[Even subgraphs to a simple-cycle product] -Let $G$ be a finite graph with nonnegative edge weights $(w_e)$. For every -even edge set $F$, fix deterministically an edge-disjoint decomposition -$\mathcal D(F)$ into simple cycles. Then +\begin{lemma}[An even matching completion is unique] +Let $M$ be a matching and $R$ any finite residual edge set. Put \[ - \sum_{F\text{ even}}\prod_{e\in F}w_e - \le - \prod_{C\text{ simple cycle}} - \left(1+\prod_{e\in C}w_e\right) - \le - \exp\left\{\sum_{C\text{ simple cycle}}\prod_{e\in C}w_e\right\}. + \mathcal C_{\rm even}(M,R) + =\{F\subseteq M\cup R:\deg_F(v)\text{ is even for every }v\}. +\] +Then +\[ + \rho:\mathcal C_{\rm even}(M,R)\to\mathcal P(R\setminus M), + \qquad \rho(F)=F\setminus M \tag{9.15a} \] +is injective. \end{lemma} \begin{proof} -The cycles in $\mathcal D(F)$ are edge-disjoint and therefore distinct, and -\[ - \prod_{e\in F}w_e - =\prod_{C\in\mathcal D(F)}\prod_{e\in C}w_e. -\] -The union of the cycles recovers $F$, so the map to the resulting cycle set is -injective. Dropping edge-disjointness enlarges the image to all subsets of the -finite simple-cycle set. Summing those subsets gives the first product, and -$1+x\le e^x$ gives the second inequality. +If $\rho(F)=\rho(F')$, then +$F\mathbin\triangle F'\subseteq M$. The symmetric difference is even. A +nonempty subset of a matching has degree one at every incident vertex, so it is +not even. Therefore $F\mathbin\triangle F'=\varnothing$. \end{proof} -Apply the lemma to $G=M\cup R$, with matching-edge weight one and residual-edge -weight $q_e$. - -\begin{lemma}[Cycles disjoint from the high matching] -Let $Q$ be the symmetric weighted adjacency kernel of the residual bipartite -graph. If every row and column sum is at most $\tau<1$, then +\begin{lemma}[Weighted restriction product] +For nonnegative residual weights $q_e$, extended by zero on $M$, \[ - \sum_{C:C\cap M=\varnothing}\prod_{e\in C}q_e - \le\frac{n\tau^4}{1-\tau^2}. - \tag{9.16} + \begin{split} + \sum_{F\in\mathcal C_{\rm even}(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). + \end{split} + \tag{9.15b} \] \end{lemma} \begin{proof} -A residual-only bipartite cycle has length $2s\ge4$. Mark one row vertex, -forget simplicity, and forget the closing constraint. For each marked start, -the total mass of length-$2s$ walks is at most $\tau^{2s}$. There are at most -$n$ marked starts, so summing $s\ge2$ gives the result. +Use the preceding injection and enlarge its image to the full power set. The +middle equality is the finite subset-product expansion, and $1+x\le e^x$ gives +the last inequality. \end{proof} -\begin{lemma}[Cycles meeting the high matching] -Let $M$ be a bipartite matching of size $h$. Let $Q$ be a nonnegative symmetric -residual kernel, zero on $M$, with row-sum norm at most $\tau<1/3$. Put +The corresponding finite ingredients already occur in the Lean development: +\begin{center} +\small\ttfamily +residualRestriction\_injective\\ +finiteInjectiveFamily\_product\_exp\_bound +\end{center} + +\paragraph{Completion of the large-residual branch.} +Equation (9.12) gives \[ - P=Q+Q^2+Q^3+\cdots, - \qquad - b=\|P\|_{\infty}\le\frac{\tau}{1-\tau}. - \tag{9.17a} + \mathcal A(M,j)\le\exp\left(\Lambda_0+\sum_eq_e\right). + \tag{9.16} \] -Then +By (9.6), \[ - \sum_{C:C\cap M\ne\varnothing}\prod_{e\in C\setminus M}q_e - \le2h\sum_{r\ge1}b^r - =\frac{2hb}{1-b} - \le Ch\tau. - \tag{9.18a} + \sum_eq_e=\frac12\sum_{a,b}\theta_{ab}^2+\Lambda_0. + \tag{9.17} \] -\end{lemma} - -\begin{proof} -Fix a total order on the oriented matching edges. For every simple cycle -meeting $M$, mark the least oriented matching edge on the cycle. This costs at -most $2h$ choices and removes rotation and orientation ambiguity. - -If the cycle uses $r\ge1$ matching edges, cutting at them leaves $r$ nonempty -residual paths. Between consecutive residual paths, the next matching edge is -determined by the current endpoint because $M$ is a matching. Matching -traversal is therefore a partial permutation of row-sum norm one and introduces -no new factor $h$. - -After dropping simplicity, vertex-disjointness, and the final closing -constraint, each residual path contributes total mass at most $b$. Relaxed -codes with exactly $r$ matching edges therefore have total mass at most -$2hb^r$. Summing over $r$ proves the claim. -\end{proof} - -\paragraph{Completion of the large-residual branch.} -Equations (9.12)--(9.14) give +Moreover \[ - \Lambda_0\le C U^4/m_0, + \sum_{a,b}\theta_{ab}^2 + =\frac{e^2}{m_0^2} + \left(\sum_ad_a^2\right) + \left(\sum_b(d'_b)^2\right). + \tag{9.18} +\] +Every residual degree is at most $U$, while both degree sums are $m_0$. +Therefore +\[ + \sum_ad_a^2\le Um_0, + \qquad + \sum_b(d'_b)^2\le Um_0, \qquad - \tau\le C U^3/m_0. + \sum_{a,b}\theta_{ab}^2\le e^2U^2. + \tag{9.18a} \] -For $m_0\ge n/N^6$, one has $\tau<1/3$ eventually, uniformly over every -feasible canonical skeleton. The preceding lemmas and $h<2n/U$ yield +Together with (9.13), \[ - \mathcal A(M,j) - \le - \exp\left[ - C\left\{ - \frac{U^4}{m_0}+n\tau^4+h\tau - \right\} - \right] - \le\exp(C'N^8). + \boxed{\mathcal A(M,j) + \le\exp\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} \tag{9.19} \] -This is a one-sided bound. No lower estimate for $\mathcal A(M,j)$ is asserted -or used. +If $m_0\ge n/N^6$, then $U=O(N)$ and +$U^4/m_0=O(N^{10}/n)=o(1)$, so +\[ + \mathcal A(M,j)\le\exp(C'N^2)=\exp\{o(n/N^4)\}. + \tag{9.19a} +\] +This removes the cycle decomposition, residual and mixed walk sums, $\tau$, +and the $h\tau$ term. No lower estimate for $\mathcal A(M,j)$ is asserted or +used. \section*{Integration checklist} @@ -539,8 +526,7 @@ \section*{Integration checklist} \item Insert the canonical exposure proposition and bare-weight definition after (8.3). \item Replace the current Lemma 8.3 by the split lemmas and final proposition. -\item Insert the three cycle lemmas between (9.14) and the large-residual -conclusion. +\item Replace the cycle/traversal passage by the matching-restriction lemmas and global square-sum estimate. \item Rename the two unrelated uses of $B_n$. \item Regenerate the TeX and PDFs from the canonical source. \item Rerun display-tag, citation, finite-diagnostic, and formalization-status From 20eba91ce5af12ec04cd4ea32b1a494ee9dca684 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 18:11:19 +0300 Subject: [PATCH 09/29] =?UTF-8?q?Record=20Erd=C5=91s=20625=20extensions=20?= =?UTF-8?q?and=20simplifications?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md | 604 ++++++++++++++++++ 1 file changed, 604 insertions(+) create mode 100644 625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md diff --git a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md new file mode 100644 index 00000000..4b9e9246 --- /dev/null +++ b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md @@ -0,0 +1,604 @@ +# 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} +\] + +Using the definitions in (9.5)--(9.6), + +\[ + \sum_e q_e + =\frac12\sum_{a,b}\theta_{ab}^2+\Lambda_0. + \tag{1.5} +\] + +The degree sums factor exactly: + +\[ + \sum_{a,b}\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}\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 second-order estimates for `G(n,1/2)` give + +\[ + h(G)=2\log_2n-2\log_2\log_2n+O(1) + \tag{7.2} +\] + +and + +\[ + \chi(G)= + \frac{n}{2\log_2n-2\log_2\log_2n+O(1)} + \tag{7.3} +\] + +with high probability. The two denominators differ by only `O(1)`, hence + +\[ + \boxed{\chi(G)-\zeta(G)=O\left(\frac{n}{(\ln n)^2}\right)} + \tag{7.4} +\] + +with high probability. + +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. A possible three-size simplification + +Numerical optimization over the full phase interval shows that the support + +\[ + S_3=\{2,3,5\} + \tag{8.1} +\] + +still has a positive uniform signed advantage: + +\[ + \min_T\{q-(\mathcal F_{S_+}(T)-\mathcal F_{S_3}(T))\} + \approx0.0921449643. + \tag{8.2} +\] + +This support is structurally attractive: + +- it retains deficits `2` and `3`, so the unimodular integer correction in + (5.16) still works; +- its minimum and maximum deficits remain `2` and `5`, so the central-rate + inequalities are unchanged; +- the maximum type displacement remains three; +- the dense transportation table becomes `3 by 3` rather than `4 by 4`. + +The proof would therefore become shorter in Sections 5, 7, and 8. However, +(8.2) is currently a numerical diagnostic, not a replacement proof. A uniform +analytic entropy certificate and a complete replay of the endpoint and +residual estimates are required before adopting this route. + +Adding deficit `1` gives a larger first-moment advantage but is not a safe +simplification: the empty-corner activity + +\[ + k_1^2/\mu_{\alpha-1}(n) +\] + +is not uniformly `o(1)` through the phase cycle. Deficit `2` is the natural +largest-class cutoff for the current partial-diagonal method. + +--- + +## 9. Root placement can probably be optimized + +The midpoint in (5.13) is convenient but not intrinsic. For a fixed +`theta in (0,1)`, consider + +\[ + k_\theta + =\left\lceil r_4^{co}+\theta(r_+-r_4^{co})\right\rceil. + \tag{9.1} +\] + +The signed first-moment margin remains `exp(c_theta n/N)` for a fixed +`c_theta>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. 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. From 3a0de6b95cff8998c802dea05a5d66ecdbcb869a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 18:12:14 +0300 Subject: [PATCH 10/29] =?UTF-8?q?Add=20TeX=20companion=20for=20Erd=C5=91s?= =?UTF-8?q?=20625=20extensions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...RDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex | 270 ++++++++++++++++++ 1 file changed, 270 insertions(+) create mode 100644 625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex diff --git a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex new file mode 100644 index 00000000..adf81b3b --- /dev/null +++ b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex @@ -0,0 +1,270 @@ +\documentclass[11pt]{article} +\usepackage[margin=1in]{geometry} +\usepackage{amsmath,amssymb,amsthm,mathtools} +\usepackage[hidelinks]{hyperref} +\usepackage{enumitem} +\newtheorem{lemma}{Lemma} +\newtheorem{proposition}{Proposition} +\newtheorem{corollary}{Corollary} +\newcommand{\E}{\mathbb E} +\newcommand{\cE}{\mathcal E} +\newcommand{\cP}{\mathcal P} +\title{Erd\H{o}s Problem 625: Result Extensions and Proof Simplifications} +\author{Research note for the candidate manuscript} +\date{24 July 2026} +\begin{document} +\maketitle + +\paragraph{Status.} +This note records exact deductions, finite rational certificates, and +architectural alternatives obtained by re-examining the candidate manuscript +at repository main commit +\begin{center} +\small\ttfamily cda78922ea6c87bfc81f9bf693374dd045dac624 +\end{center} +It is not external peer review, priority verification, or a completed Lean +proof of the final target. Put $q=\ln2$ and $N=\ln n$. + +\section{Exact simplification of the large-residual attachment bound} + +\begin{lemma}[An even completion of residual edges is unique] +Let $M$ be a matching and $R$ any other finite edge set. Put +\[ + \cE(M,R)=\{F\subseteq M\cup R:\deg_F(v)\equiv0\pmod2\text{ for every }v\}. +\] +Then +\[ + \rho:\cE(M,R)\to\cP(R\setminus M),\qquad \rho(F)=F\setminus M + \tag{1.1} +\] +is injective. +\end{lemma} + +\begin{proof} +If $\rho(F)=\rho(F')$, then $F\mathbin\triangle F'\subseteq M$. The symmetric +difference is even. A nonempty subset of a matching has degree one at every +incident vertex, so it is not even. Thus $F\mathbin\triangle F'=\varnothing$. +\end{proof} + +\begin{corollary}[Weighted product bound] +For nonnegative residual weights $(q_e)$, extended by zero on $M$, +\[ + \sum_{F\in\cE(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 q_e\right). + \tag{1.2} +\] +\end{corollary} + +Equation (9.12) therefore gives +\[ + \mathcal A(M,j)\le\exp\left(\Lambda_0+\sum_eq_e\right). + \tag{1.3} +\] +Since +\[ + \sum_eq_e=\frac12\sum_{a,b}\theta_{ab}^2+\Lambda_0 + \tag{1.4} +\] +and +\[ + \sum_{a,b}\theta_{ab}^2 + =\frac{e^2}{m_0^2} + \left(\sum_ad_a^2\right)\left(\sum_b(d'_b)^2\right) + \le e^2U^2, + \tag{1.5} +\] +while $\Lambda_0\le CU^4/m_0$, we obtain +\[ + \boxed{\mathcal A(M,j) + \le\exp\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} + \tag{1.6} +\] +For $m_0\ge n/N^6$ and $U=O(N)$ this is $\exp(CN^2)$, stronger than the +current $\exp(CN^8)$ bound. It removes the simple-cycle decomposition, +residual and mixed walk enumeration, $\tau$, and equations (9.15)--(9.18). + +\section{A stronger central partial-diagonal rate} + +\begin{lemma} +Under the hypotheses of Lemma 7.1A, +\[ + \Phi_T(z)\le-\frac{1-R}{100}\qquad(1/64\le R\le1). + \tag{2.1} +\] +\end{lemma} + +\begin{proof} +On $[1/64,47/100]$ use +\[ + \Phi_T(z)\le R\ln R+(5q/2-1)R. +\] +The convex function +\[ + f(R)=R\ln R+(5q/2-1)R+\frac{1-R}{100} +\] +has $f(1/64)<-0.0436$ and $f(47/100)<-0.0051$. On +$[47/100,1]$ use +\[ + \Phi_T(z)\le R\ln R+(1-q/2)(1-R). +\] +The convex function +\[ + h(R)=R\ln R+(1-q/2+1/100)(1-R) +\] +has $h(47/100)<-0.0032$ and $h(1)=0$. +\end{proof} + +\section{Carry the phase-resolved displacement to the theorem} + +Put +\[ + A(\delta)=q-D_4(\delta),\qquad + A_*=\min_{0\le\delta\le1}A(\delta). + \tag{3.1} +\] +Continuity and Lemma 5.1 give $A_*>\gamma_4$, where +$\gamma_4=\ln(200/153)$. Equation (5.11), the midpoint construction, and the +$o(n/N^3)$ amplification loss give +\[ + \boxed{\chi(G_n)-\zeta(G_n) + \ge\left(\frac{q^2}{8}A(\delta_n)-o(1)\right)\frac{n}{N^3}} + \tag{3.2} +\] +with high probability. Thus the fixed displayed constant can be increased +from $q^2\gamma_4/32$ to $q^2\gamma_4/8$ without changing the witness or +second-moment argument. + +\section{A stronger four-support entropy certificate} + +\begin{proposition} +For every phase, +\[ + \frac{12}{5}q<\lambda_4<\frac{21}{5}q. + \tag{4.1} +\] +Moreover +\[ + L(12q/5)<3/10,\quad H(3q)<1/50, + \quad L(3q)<3/25,\quad H(21q/5)<1/5. + \tag{4.2} +\] +Consequently +\[ + D_4(\delta)<\ln(33/25),\qquad q-D_4(\delta)>\ln(50/33). + \tag{4.3} +\] +\end{proposition} + +Put $x=2^{1/10}$. The rational intervals +\[ + 0.6931471/2$ this is a direct lower bound on $\chi(G)-\zeta(G)$; for $p<1/2$ +it applies to the complementary chromatic gap. Thus $p=1/2$ is the unique +fixed-density point where the first-order comparison cancels. + +\section{A standard upper bound} + +If $h(G)=\max\{\alpha(G),\omega(G)\}$, then $\zeta(G)\ge n/h(G)$. The standard +second-order estimates at $p=1/2$ give +\[ + h(G)=2\log_2n-2\log_2\log_2n+O(1) +\] +and +\[ + \chi(G)=\frac{n}{2\log_2n-2\log_2\log_2n+O(1)}. +\] +Hence +\[ + \boxed{\chi(G)-\zeta(G)=O\left(\frac{n}{(\ln n)^2}\right)} + \tag{7.1} +\] +with high probability. + +\section{Architectural alternatives} + +Numerical optimization shows that the three-size support $\{2,3,5\}$ still has +uniform positive signed advantage, approximately $0.0921449643$. It preserves +the unimodular correction coordinates $2,3$, the central-rate endpoints $2,5$, +and maximum type displacement three, while reducing the transportation table +from $4\times4$ to $3\times3$. This is a diagnostic, not yet a proved +replacement route. + +The midpoint can also be replaced by +\[ + k_\theta=\left\lceil r_4^{co}+\theta(r_+-r_4^{co})\right\rceil +\] +for fixed $\theta\in(0,1)$. The retained gap would be +\[ + \left((1-\theta)\frac{q^2}{4}A(\delta)+o(1)\right)\frac{n}{N^3}, +\] +while the signed first moment keeps a fixed positive exponential margin. This +requires a route-by-route replay of every use of $c_Z$ before being promoted to +a theorem. + +\section{Recommended order} +\begin{enumerate} +\item Replace the large-residual cycle expansion by the restriction injection. +\item Strengthen the central rate. +\item Carry equation (5.11) directly to the conclusion. +\item Review and insert the exact entropy certificate. +\item Add the complement and fixed-density corollaries. +\item Keep the three-size and non-midpoint variants on experimental branches. +\end{enumerate} +\end{document} From 32d4dd6d55a5dc94ba1397d7d9199e375fdb84b5 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 18:12:54 +0300 Subject: [PATCH 11/29] Add exact entropy certificate diagnostics --- .../entropy_certificate_upgrade.py | 165 ++++++++++++++++++ 1 file changed, 165 insertions(+) create mode 100644 625/experiments/entropy_certificate_upgrade.py diff --git a/625/experiments/entropy_certificate_upgrade.py b/625/experiments/entropy_certificate_upgrade.py new file mode 100644 index 00000000..7052d55e --- /dev/null +++ b/625/experiments/entropy_certificate_upgrade.py @@ -0,0 +1,165 @@ +#!/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 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}") + print(f" carry-(5.11)+new certificate = {q*q*new_gamma/8:.12f}") + + +def main() -> None: + certify_log_two_interval() + certify_tenth_root_interval() + certify_tilt_bracket() + certify_omitted_weight_bounds() + print("EXACT CERTIFICATE CHECKS: PASS") + scan_supports() + + +if __name__ == "__main__": + main() From b26c1a14dbd0cdf73d09144ed36c91dc43ed3c0c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 18:22:31 +0300 Subject: [PATCH 12/29] Certify the three-size entropy alternative --- .../entropy_certificate_upgrade.py | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) diff --git a/625/experiments/entropy_certificate_upgrade.py b/625/experiments/entropy_certificate_upgrade.py index 7052d55e..f64fc28e 100644 --- a/625/experiments/entropy_certificate_upgrade.py +++ b/625/experiments/entropy_certificate_upgrade.py @@ -90,6 +90,55 @@ def certify_omitted_weight_bounds() -> None: 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]: @@ -149,7 +198,10 @@ def scan_supports() -> None: 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: @@ -157,6 +209,7 @@ def main() -> None: certify_tenth_root_interval() certify_tilt_bracket() certify_omitted_weight_bounds() + certify_three_support_certificate() print("EXACT CERTIFICATE CHECKS: PASS") scan_supports() From 21005062cd47831f016a1950331f8cb652797bce Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 18:24:16 +0300 Subject: [PATCH 13/29] Prove a three-size entropy certificate --- ...ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md | 176 +++++++++++++++--- 1 file changed, 155 insertions(+), 21 deletions(-) diff --git a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md index 4b9e9246..373766bf 100644 --- a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md +++ b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md @@ -517,46 +517,180 @@ moment. --- -## 8. A possible three-size simplification +## 8. An exactly certified three-size first-moment alternative -Numerical optimization over the full phase interval shows that the support +Let \[ - S_3=\{2,3,5\} + S_3=\{2,3,5\}, + \qquad + D_3(\delta)=\mathcal F_{S_+}(T_0)-\mathcal F_{S_3}(T_0). \tag{8.1} \] -still has a positive uniform signed advantage: +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}) Date: Fri, 24 Jul 2026 18:25:27 +0300 Subject: [PATCH 14/29] Add the exact three-size entropy route to TeX --- ...RDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex | 78 +++++++++++++++++-- 1 file changed, 70 insertions(+), 8 deletions(-) diff --git a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex index adf81b3b..d08f7906 100644 --- a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex +++ b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex @@ -237,16 +237,78 @@ \section{A standard upper bound} \] with high probability. -\section{Architectural alternatives} +\section{An exactly certified three-size alternative} -Numerical optimization shows that the three-size support $\{2,3,5\}$ still has -uniform positive signed advantage, approximately $0.0921449643$. It preserves -the unimodular correction coordinates $2,3$, the central-rate endpoints $2,5$, -and maximum type displacement three, while reducing the transportation table -from $4\times4$ to $3\times3$. This is a diagnostic, not yet a proved -replacement route. +Let $S_3=\{2,3,5\}$ and +\[ + D_3(\delta)=\mathcal F_{S_+}(T_0)-\mathcal F_{S_3}(T_0). +\] +The same omitted-mass method gives a rigorous positive advantage. + +\begin{proposition} +For every target $2/q\le T\le1+2/q$, the $S_3$ tilt satisfies +\[ + \frac{29}{10}q<\lambda_3<\frac{21}{5}q. + \tag{8.1} +\] +Moreover +\[ + D_3(\delta)<\ln\frac{391}{200}, + \qquad + q-D_3(\delta)>\ln\frac{400}{391}>0. + \tag{8.2} +\] +\end{proposition} + +Let $L_3$ be the omitted ratio from deficits $-1,0,1$, let $M_4$ be the +ratio of the deficit-4 weight, and let $H_3$ be the ratio of the tail from six +onward. Exact rational comparisons give +\[ + L_3(29q/10)<\frac15, + \quad H_3(7q/2)<\frac2{25}, + \quad M_4(7q/2)=\frac12, + \tag{8.3} +\] +and +\[ + L_3(7q/2)<\frac2{25}, + \quad H_3(21q/5)<\frac14, + \quad M_4(21q/5)<\frac58. + \tag{8.4} +\] +The low ratio decreases with the tilt, the high ratio increases, and $M_4$ +increases because the retained mean stays below four. Splitting at $7q/2$ +therefore bounds the total omitted ratio by $191/200$. + +With $x=2^{1/10}$, the endpoint checks reduce to integer powers. Two of the +load-bearing inequalities are +\[ + 5(1+x^{34}+x^{58}) Date: Fri, 24 Jul 2026 20:04:46 +0300 Subject: [PATCH 15/29] Split and verify the Section 7 rate replacement --- 625/proofs/PR27_SECTION7_CENTRAL_RATE.md | 160 +++++++++++++++++++++++ 1 file changed, 160 insertions(+) create mode 100644 625/proofs/PR27_SECTION7_CENTRAL_RATE.md 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. + +--- From 6eeebdab027d418723ff19023afae17dd651c2b4 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:06:27 +0300 Subject: [PATCH 16/29] Add the TeX companion for the Section 7 rate --- 625/proofs/PR27_SECTION7_CENTRAL_RATE.tex | 159 ++++++++++++++++++++++ 1 file changed, 159 insertions(+) create mode 100644 625/proofs/PR27_SECTION7_CENTRAL_RATE.tex 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} From a6e153b00582bceea0bafd5a5de5b17c42a817eb Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:06:59 +0300 Subject: [PATCH 17/29] State the exact Section 8 exposure with degree caps --- 625/proofs/PR27_SECTION8_EXPOSURE.md | 130 +++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 625/proofs/PR27_SECTION8_EXPOSURE.md 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. + +--- From 1eff8f1b452d66a3435871f3186302e2c32315ce Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:07:28 +0300 Subject: [PATCH 18/29] Add the TeX companion for exact Section 8 exposure --- 625/proofs/PR27_SECTION8_EXPOSURE.tex | 125 ++++++++++++++++++++++++++ 1 file changed, 125 insertions(+) create mode 100644 625/proofs/PR27_SECTION8_EXPOSURE.tex 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} From 2f93b4a23d848ed68254c378738e091e2bcf139e Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:08:26 +0300 Subject: [PATCH 19/29] Make the Section 8 high-skeleton sum finite and explicit --- 625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md | 266 ++++++++++++++++++ 1 file changed, 266 insertions(+) create mode 100644 625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.md 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_0 Date: Fri, 24 Jul 2026 20:09:30 +0300 Subject: [PATCH 20/29] Add the TeX companion for the explicit high-skeleton sum --- .../PR27_SECTION8_HIGH_SKELETON_SUM.tex | 239 ++++++++++++++++++ 1 file changed, 239 insertions(+) create mode 100644 625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.tex diff --git a/625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.tex b/625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.tex new file mode 100644 index 00000000..e87607e5 --- /dev/null +++ b/625/proofs/PR27_SECTION8_HIGH_SKELETON_SUM.tex @@ -0,0 +1,239 @@ +\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: split high-skeleton summation} +\author{Companion revision for the Erd\H{o}s Problem 625 candidate manuscript} +\date{24 July 2026} +\begin{document} +\maketitle +\section{PR \#27: split high-skeleton summation}\label{pr-27-split-high-skeleton-summation} + +\textbf{Status.} Candidate replacement text, audited against current \texttt{main} on 24 July 2026. Exact finite tests are recorded in the PR verification report; the asymptotic chain still requires independent review. + +\subsection{Replacement block C: split form of Lemma 8.3}\label{replacement-block-c-split-form-of-lemma-8.3} + +\subsubsection{Lemma 8.3A (one-cell near-containment series)}\label{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} +\] + +\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 Date: Fri, 24 Jul 2026 20:10:13 +0300 Subject: [PATCH 21/29] Replace the Section 9 cycle route by residual restriction --- .../PR27_SECTION9_RESIDUAL_RESTRICTION.md | 116 ++++++++++++++++++ 1 file changed, 116 insertions(+) create mode 100644 625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.md diff --git a/625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.md b/625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.md new file mode 100644 index 00000000..c4808abd --- /dev/null +++ b/625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.md @@ -0,0 +1,116 @@ +# PR #27: residual-restriction replacement for Lemma 9.1 + +**Status.** Candidate replacement text. The finite restriction injection and product algebra have Lean counterparts, but their full probabilistic specialization is not claimed as formally complete. + +## Replacement block D: residual-restriction product bound in Lemma 9.1 + +Replace the cycle decomposition and traversal discussion surrounding equations +(9.15)--(9.18) by the following two finite lemmas. + +### Lemma 9.1A (an even matching completion is unique) + +Let \(M\) be a matching and let \(R\) be any finite residual edge set. Write + +\[ + \mathcal C_{\rm even}(M,R) + =\{F\subseteq M\cup R:\deg_F(v)\text{ is even for every }v\}. +\] + +Then the restriction map + +\[ + \rho:\mathcal C_{\rm even}(M,R)\longrightarrow\mathcal P(R\setminus M), + \qquad \rho(F)=F\setminus M, + \tag{9.15a} +\] + +is injective. + +#### Proof + +If \(\rho(F)=\rho(F')\), then \(F\mathbin\triangle F'\subseteq M\). The +symmetric difference is even. A nonempty subset of a matching has degree one +at every incident vertex and cannot be even. Hence \(F=F'\). \(\square\) + +### Lemma 9.1B (weighted restriction product) + +For nonnegative residual weights \(q_e\), + +\[ + \begin{split} + \sum_{F\in\mathcal C_{\rm even}(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\in R\setminus M}q_e\right). + \end{split} + \tag{9.15b} +\] + +This is the weighted form of the finite restriction injection already present in +the Lean development. + +### Completion of the large-residual branch + +Equation (9.12) gives + +\[ + \mathcal A(M,j) + \le\exp\left(\Lambda_0+ + \sum_{e\in R\setminus M}q_e\right). + \tag{9.16} +\] + +For every off-matching cell put +\(\widetilde\theta_{ab}=e d_ad_b'/m_0\). Since \(q=0\) on \(M\), equation +(9.6) gives + +\[ + \sum_{e\in R\setminus M}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{9.17} +\] + +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{9.18} +\] + +Every residual degree is at most \(U\), and both degree sums equal \(m_0\), so + +\[ + \sum_a d_a^2\le Um_0, + \qquad + \sum_b(d_b')^2\le Um_0, + \qquad + \sum_{a,b}\widetilde\theta_{ab}^{\,2}\le e^2U^2. + \tag{9.18a} +\] + +Together with \(\Lambda_0\le CU^4/m_0\), this proves + +\[ + \boxed{\mathcal A(M,j) + \le\exp\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} + \tag{9.19} +\] + +If \(m_0\ge n/N^6\), then \(U=O(N)\) and +\(U^4/m_0=O(N^{10}/n)=o(1)\). Hence + +\[ + \mathcal A(M,j)\le e^{C'N^2}=\exp\{o(n/N^4)\} + \tag{9.19a} +\] + +uniformly over every feasible skeleton. This removes the simple-cycle +partition, residual-walk enumeration, matching-cycle encoding, \(\tau\), and +the \(h\tau\) term. + +--- From 364004a2336e4ca72eef3dfdd935dadb62f56dd5 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:10:58 +0300 Subject: [PATCH 22/29] Add the TeX companion for residual restriction --- .../PR27_SECTION9_RESIDUAL_RESTRICTION.tex | 123 ++++++++++++++++++ 1 file changed, 123 insertions(+) create mode 100644 625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.tex diff --git a/625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.tex b/625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.tex new file mode 100644 index 00000000..2049cf5a --- /dev/null +++ b/625/proofs/PR27_SECTION9_RESIDUAL_RESTRICTION.tex @@ -0,0 +1,123 @@ +\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: residual-restriction replacement for Lemma 9.1} +\author{Companion revision for the Erd\H{o}s Problem 625 candidate manuscript} +\date{24 July 2026} +\begin{document} +\maketitle +\section{PR \#27: residual-restriction replacement for Lemma 9.1}\label{pr-27-residual-restriction-replacement-for-lemma-9.1} + +\textbf{Status.} Candidate replacement text. The finite restriction injection and product algebra have Lean counterparts, but their full probabilistic specialization is not claimed as formally complete. + +\subsection{Replacement block D: residual-restriction product bound in Lemma 9.1}\label{replacement-block-d-residual-restriction-product-bound-in-lemma-9.1} + +Replace the cycle decomposition and traversal discussion surrounding equations (9.15)--(9.18) by the following two finite lemmas. + +\subsubsection{Lemma 9.1A (an even matching completion is unique)}\label{lemma-9.1a-an-even-matching-completion-is-unique} + +Let \(M\) be a matching and let \(R\) be any finite residual edge set. Write + +\[ + \mathcal C_{\rm even}(M,R) + =\{F\subseteq M\cup R:\deg_F(v)\text{ is even for every }v\}. +\] + +Then the restriction map + +\[ + \rho:\mathcal C_{\rm even}(M,R)\longrightarrow\mathcal P(R\setminus M), + \qquad \rho(F)=F\setminus M, + \tag{9.15a} +\] + +is injective. + +\paragraph{Proof}\label{proof} + +If \(\rho(F)=\rho(F')\), then \(F\mathbin\triangle F'\subseteq M\). The symmetric difference is even. A nonempty subset of a matching has degree one at every incident vertex and cannot be even. Hence \(F=F'\). \(\square\) + +\subsubsection{Lemma 9.1B (weighted restriction product)}\label{lemma-9.1b-weighted-restriction-product} + +For nonnegative residual weights \(q_e\), + +\[ + \begin{split} + \sum_{F\in\mathcal C_{\rm even}(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\in R\setminus M}q_e\right). + \end{split} + \tag{9.15b} +\] + +This is the weighted form of the finite restriction injection already present in the Lean development. + +\subsubsection{Completion of the large-residual branch}\label{completion-of-the-large-residual-branch} + +Equation (9.12) gives + +\[ + \mathcal A(M,j) + \le\exp\left(\Lambda_0+ + \sum_{e\in R\setminus M}q_e\right). + \tag{9.16} +\] + +For every off-matching cell put \(\widetilde\theta_{ab}=e d_ad_b'/m_0\). Since \(q=0\) on \(M\), equation (9.6) gives + +\[ + \sum_{e\in R\setminus M}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{9.17} +\] + +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{9.18} +\] + +Every residual degree is at most \(U\), and both degree sums equal \(m_0\), so + +\[ + \sum_a d_a^2\le Um_0, + \qquad + \sum_b(d_b')^2\le Um_0, + \qquad + \sum_{a,b}\widetilde\theta_{ab}^{\,2}\le e^2U^2. + \tag{9.18a} +\] + +Together with \(\Lambda_0\le CU^4/m_0\), this proves + +\[ + \boxed{\mathcal A(M,j) + \le\exp\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} + \tag{9.19} +\] + +If \(m_0\ge n/N^6\), then \(U=O(N)\) and \(U^4/m_0=O(N^{10}/n)=o(1)\). Hence + +\[ + \mathcal A(M,j)\le e^{C'N^2}=\exp\{o(n/N^4)\} + \tag{9.19a} +\] + +uniformly over every feasible skeleton. This removes the simple-cycle partition, residual-walk enumeration, matching-cycle encoding, \(\tau\), and the \(h\tau\) term. + +\begin{center}\rule{0.5\linewidth}{0.5pt}\end{center} +\end{document} From 2b068451f323785a81dd7eb1cb898ccd321c7947 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:11:40 +0300 Subject: [PATCH 23/29] Record the finite verification of PR 27 --- 625/PR27_VERIFICATION_REPORT.md | 127 ++++++++++++++++++++++++++++++++ 1 file changed, 127 insertions(+) create mode 100644 625/PR27_VERIFICATION_REPORT.md 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. From e7391d16bf8ab816076a6780295d1a54751ba249 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:12:55 +0300 Subject: [PATCH 24/29] Add exhaustive finite regression checks for PR 27 --- 625/experiments/review27_verification.py | 388 +++++++++++++++++++++++ 1 file changed, 388 insertions(+) create mode 100644 625/experiments/review27_verification.py 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() From 5dd1e7ca41c84ef156b947cd296124009499d7c0 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:13:11 +0300 Subject: [PATCH 25/29] Replace the stale monolithic rewrite with a corrected index --- 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md | 703 +--------------------- 1 file changed, 21 insertions(+), 682 deletions(-) diff --git a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md index 8148649f..b710a121 100644 --- a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md +++ b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.md @@ -1,684 +1,23 @@ # Review-focused replacement text for Sections 7--9 -**Status.** This file supplies drop-in replacement passages for the most -concentrated parts of the canonical manuscript. It does not change the theorem, -constant, four class sizes, or proof architecture. Its purpose is to make the -quantifiers, finite decompositions, and multiplicity accounting explicit enough -for independent review and later formalization. - -The text is organized as replacement blocks rather than as a second complete -manuscript. Equation numbers refer to the canonical manuscript. - -## Global notation and uniformity edits - -Use - -\[ - q=\ln2,\qquad N=\ln n,\qquad w=\ln N. -\] - -Rename the affine coefficient in equation (3.12) from `B_n` to -\(b_n^{\mathrm{aff}}\). Reserve - -\[ - \mathcal B_n:=\frac{n}{N^4} -\] - -for the amplification scale currently called `B_n` in equation (10.10). - -Unless a statement says otherwise, every asymptotic estimate in the replacement -text is uniform over: - -1. the complete phase interval \(0\le\delta<1\); -2. the exact tangent-rounded four-size profile from Section 5; -3. every feasible subprofile or canonical skeleton in the displayed finite - sum; -4. every residual degree list satisfying the displayed cap and total-mass - hypotheses. - -The constants may depend on fixed numerical corridor widths, but not on the -phase, profile coordinates, skeleton, or residual table. - ---- - -## 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. - ---- - -## 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) - -Fix row degrees \((s_a)_a\) and column degrees \((t_b)_b\), each summing to -\(n\), and let \(r=(r_{ab})\) be a feasible overlap table. Put - -\[ - U=\alpha-2, - \qquad - R_0=\lfloor U/2\rfloor, - \qquad - M(r)=\{(a,b):r_{ab}>R_0\}. -\] - -Then the following hold. - -1. **Matching property.** The support \(M(r)\) is a partial matching. Indeed, - two cells in one row or column, each larger than \(U/2\), would use more - than the available degree, which is at most \(U\). - -2. **Canonical demand.** For \(e=(a,b)\in M(r)\), set \(j_e=r_{ab}\) and - \(J=\sum_{e\in M(r)}j_e\). Remove the selected \(j_e\) row and column stubs - and their prescribed pairings. The residual degree lists are - - \[ - s_a'=s_a-\sum_{b:(a,b)\in M(r)}j_{ab}, - \qquad - t_b'=t_b-\sum_{a:(a,b)\in M(r)}j_{ab}, - \] - - and both sum to \(n-J\). - -3. **Residual table.** Define - - \[ - r'_{ab}= - \begin{cases} - 0,&(a,b)\in M(r),\\ - r_{ab},&(a,b)\notin M(r). - \end{cases} - \] - - Then \(r'\) has margins \((s_a')\) and \((t_b')\), it vanishes on the - exposed matching, and \(r'_{ab}\le R_0\) off the matching. - -4. **Unique reconstruction.** Conversely, the tuple consisting of the - matching \(M\), the demands \((j_e)_{e\in M}\), the selected labelled stub - pairs, and a residual matching satisfying the zero-on-\(M\) and cap-off-\(M\) - conditions reconstructs one full matching and one overlap table. Applying - the canonical extraction to that table recovers the same tuple. - -5. **Exact mass cancellation.** The incidence of the exposed cells 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! - }, - \qquad - d_a=\sum_{b:(a,b)\in M}j_{ab}, - \quad - d_b'=\sum_{a:(a,b)\in M}j_{ab}. - \tag{8.3a} - \] - - The residual contingency-table mass is - - \[ - p_{res}(r')= - \frac{ - \prod_a(s_a-d_a)! - \prod_b(t_b-d_b')! - }{ - (n-J)!\prod_{a,b}r'_{ab}! - }. - \tag{8.3b} - \] - - Since \((s)_d=s!/(s-d)!\) and \((n)_J=n!/(n-J)!\), multiplication gives - - \[ - \begin{split} - \pi(M,j)p_{res}(r') - &= - \frac{\prod_a s_a!\prod_b t_b!} - {n!\prod_{e\in M}j_e!\prod_{a,b}r'_{ab}!}\\ - &= - \frac{\prod_a s_a!\prod_b t_b!} - {n!\prod_{a,b}r_{ab}!} - =p(r). - \end{split} - \tag{8.3c} - \] - -Hence the canonical exposure is an exact finite partition of the overlap law: -every table appears once, with no hidden multiplicity and no proportionality -constant. \(\square\) - -### Definition 8.0A (bare canonical-skeleton weight) - -For a feasible canonical skeleton \((M,j)\), define its **bare weight** to be -its exact exposure incidence multiplied by the local high-cell rewards, - -\[ - \operatorname{Bare}(M,j) - =\pi(M,j)\prod_{e\in M}g(j_e), - \tag{8.3d} -\] - -with the residual cap and no-return event retained in the residual law but with -the capped residual local/cycle factor postponed to Section 9. - -When the proof below dominates an unfinished high-cell completion by the full -residual integrand, it is using a larger nonnegative quantity only to bound the -bare completion sum. That domination does not redefine -\(\operatorname{Bare}(M,j)\), and Section 9 is still applied exactly once to the -true residual factor. - ---- - -## Replacement block C: split form of Lemma 8.3 - -Replace Lemma 8.3 by the following four lemmas and final proposition. The -calculation is the same as the canonical proof, but every summation level is -named explicitly. - -### Lemma 8.3A (one-cell near-containment sum) - -Let the smaller slot have size \(m\), the larger size \(m+d\), where -\(0\le d\le3\). Replacing an endpoint multiplicity \(m\) by \(m-e\) has the -exact local ratio - -\[ - R_{m,d}(e)= - \frac{\binom me}{(d+1)\cdots(d+e)} - 2^{-em+e(e+1)/2}. - \tag{8.21} -\] - -After charging the possible loss of \(e\) units in the one global falling -factorial by \(n^e\), one has, uniformly in the four cell types, - -\[ - \sum_{1\le e0 - \tag{8.24a} -\] - -on \(0\le e\le m/4\) for all sufficiently large \(m\). Thus the ratios are -log-convex and attain their maximum at an endpoint. At \(e=0\), equation -(8.15) gives \(\rho_0=O(N^3/n)\); at \(e=\lfloor m/4\rfloor\), -\(\rho_e=n^{-1/2+o(1)}\). Both are eventually below \(1/2\), uniformly in the -cell type, so the series is geometrically decreasing and (8.25) follows. -\(\square\) - -### Lemma 8.3B (global product over near-containment decorations) - -Fix a typed full-containment table \(L\). Temporarily distinguish every -endpoint cell occurrence of \(L\). For each occurrence \(c\), independently -choose either deficit \(e_c=0\) or \(1\le e_c0\) such that, for all sufficiently large -\(n\), every summand satisfies - -\[ - \log_2\left[ - k_{co}^2g(j)\frac{(ea^2/m_0)^j}{j!} - \right] - \le-c_0(\log_2n)^2. - \tag{8.28a} -\] - -Consequently \(\Xi_4=2^{-\Omega((\log n)^2)}\), uniformly in \(S\). - -#### Proof - -Expand over distinct residual cells and threshold demands before dropping any -constraints. Lemma 6.2 applies jointly and yields (8.26a)--(8.27). Put -\(L_2=\log_2n\) and \(j=xL_2\). The hypotheses imply - -\[ - 1+o(1)\le x\le3/2+o(1), - \qquad - \log_2m_0\ge L_2-6\log_2N. -\] - -Using \(g(j)\le2^{j^2/2}\), \(k_{co}\le n\), and -\(\log_2(j!)\ge0\), - -\[ - \log_2\left[ - k_{co}^2g(j)\frac{(ea^2/m_0)^j}{j!} - \right] - \le - 2L_2+\left(\frac{x^2}{2}-x\right)L_2^2 - +O(L_2\log L_2). -\] - -On the limiting interval \([1,3/2]\), -\(x^2/2-x\le-3/8\). Choose, for example, \(c_0=1/4\); the lower-order term is -smaller than \(L_2^2/8\) for all sufficiently large \(n\), uniformly over the -floor perturbations and the four cell types. This proves (8.28a). -\(\square\) - -### Lemma 8.3D (small residual completion) - -If \(m_0 Date: Fri, 24 Jul 2026 20:13:23 +0300 Subject: [PATCH 26/29] Replace the stale monolithic TeX with a corrected index --- 625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex | 543 +-------------------- 1 file changed, 18 insertions(+), 525 deletions(-) diff --git a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex index 14077ab0..e7873295 100644 --- a/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex +++ b/625/proofs/SECTIONS_7_9_REVIEW_REWRITE.tex @@ -1,538 +1,31 @@ \documentclass[11pt]{article} \usepackage[margin=1in]{geometry} -\usepackage{amsmath,amssymb,amsthm,mathtools} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} \usepackage[hidelinks]{hyperref} -\usepackage{enumitem} - -\newtheorem{lemma}{Lemma} -\newtheorem{proposition}{Proposition} -\theoremstyle{definition} -\newtheorem{definition}{Definition} - -\newcommand{\E}{\mathbb E} -\newcommand{\Prb}{\mathbb P} -\newcommand{\Bare}{\operatorname{Bare}} - +\usepackage{microtype} \title{Review-Focused Replacement Text for Sections 7--9} \author{Companion revision for the Erd\H{o}s Problem 625 candidate manuscript} -\date{23 July 2026} - +\date{24 July 2026} \begin{document} \maketitle -\paragraph{Status.} -This file supplies drop-in replacement passages for the most concentrated -parts of the canonical manuscript. It does not change the theorem, constant, -four class sizes, or proof architecture. Its purpose is to make the -quantifiers, finite decompositions, and multiplicity accounting explicit -enough for independent review and later formalization. Equation numbers refer -to the canonical manuscript. - -\section*{Global notation and uniformity edits} - -Use -\[ - q=\ln2,\qquad N=\ln n,\qquad w=\ln N. -\] -Rename the affine coefficient in equation (3.12) from $B_n$ to -$b_n^{\mathrm{aff}}$. Reserve -\[ - \mathcal B_n:=\frac{n}{N^4} -\] -for the amplification scale currently called $B_n$ in equation (10.10). - -Unless a statement says otherwise, every asymptotic estimate below is uniform -over the complete phase interval $0\le\delta<1$, the exact tangent-rounded -four-size profile, every feasible subprofile or canonical skeleton in the -displayed finite sum, and every residual degree list satisfying the displayed -cap and total-mass hypotheses. Constants may depend on fixed numerical -corridor widths, but not on the phase, profile coordinates, skeleton, or -residual table. - -\section*{Replacement A: the central rate in Lemma 7.1} - -\begin{lemma}[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 $0\ln0=0$, one has -\[ - \Phi_T(z)\le-\frac{Y}{100} - \qquad\text{whenever}\qquad - \frac1{64}\le R\le1. - \tag{7.21a} -\] -\end{lemma} - -\begin{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 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}. -\] -\end{proof} - -\paragraph{Completion of the central range.} -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$. Equation (7.20) and the lemma 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. After increasing the eventual threshold for $n$, the error terms -are at most half of the leading negative term. Hence, for an absolute $c>0$, -\[ - D(\ell)\le \exp(-c k_{co}w). - \tag{7.25} -\] -The at most $(k_{co}+1)^4$ central vectors therefore contribute $o(1)$. - -\section*{Replacement B: exact canonical exposure at the start of Section 8} - -\begin{proposition}[Canonical high-cell exposure identity] -Fix row degrees $(s_a)_a$ and column degrees $(t_b)_b$, each summing to $n$, -and let $r=(r_{ab})$ be a feasible overlap table. Put -\[ - U=\alpha-2, - \qquad - R_0=\lfloor U/2\rfloor, - \qquad - M(r)=\{(a,b):r_{ab}>R_0\}. -\] -Then: -\begin{enumerate}[label=\arabic*.] -\item $M(r)$ is a partial matching. -\item For $e=(a,b)\in M(r)$, set $j_e=r_{ab}$ and -$J=\sum_{e\in M(r)}j_e$. The residual degrees are -\[ - s_a'=s_a-\sum_{b:(a,b)\in M(r)}j_{ab}, - \qquad - t_b'=t_b-\sum_{a:(a,b)\in M(r)}j_{ab}. -\] -\item The residual table -\[ - r'_{ab}= - \begin{cases} - 0,&(a,b)\in M(r),\\ - r_{ab},&(a,b)\notin M(r) - \end{cases} -\] -has those residual margins, vanishes on $M(r)$, and is at most $R_0$ off the -matching. -\item The matching, demands, selected labelled stub pairs, and capped residual -matching reconstruct the original matching uniquely. -\item The exposure incidence times the residual contingency law equals the -original table law exactly. -\end{enumerate} -\end{proposition} - -\begin{proof} -The matching property follows because every row and column degree is at most -$U$, while two cells larger than $U/2$ in one row or column would use more than -$U$ stubs. The margin and cap statements follow directly from the definition. -Reconstruction is by adjoining the selected labelled pairs to the residual -matching; canonical extraction recovers the same data. - -Write -\[ - d_a=\sum_{b:(a,b)\in M}j_{ab}, - \qquad - d_b'=\sum_{a:(a,b)\in M}j_{ab}. -\] -The exposure incidence 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.3a} -\] -The residual table mass is -\[ - p_{res}(r')= - \frac{ - \prod_a(s_a-d_a)! - \prod_b(t_b-d_b')! - }{ - (n-J)!\prod_{a,b}r'_{ab}! - }. - \tag{8.3b} -\] -Using $(s)_d=s!/(s-d)!$ and $(n)_J=n!/(n-J)!$ gives -\[ -\begin{split} - \pi(M,j)p_{res}(r') - &=\frac{\prod_a s_a!\prod_b t_b!} - {n!\prod_{e\in M}j_e!\prod_{a,b}r'_{ab}!}\\ - &=\frac{\prod_a s_a!\prod_b t_b!} - {n!\prod_{a,b}r_{ab}!} - =p(r). -\end{split} -\tag{8.3c} -\] -Thus every table appears once, with no hidden multiplicity or proportionality -constant. -\end{proof} - -\begin{definition}[Bare canonical-skeleton weight] -For a feasible canonical skeleton $(M,j)$, set -\[ - \Bare(M,j)=\pi(M,j)\prod_{e\in M}g(j_e). - \tag{8.3d} -\] -The residual cap and no-return event remain in the residual law, while the -capped residual local/cycle factor is postponed to Section 9. -\end{definition} - -When an unfinished high-cell completion is bounded above by the full -residual integrand, the latter is only a larger nonnegative numerical -majorant. It does not redefine $\Bare(M,j)$, and the Section 9 residual factor -is still applied exactly once. - -\section*{Replacement C: split form of Lemma 8.3} - -\begin{lemma}[One-cell near-containment sum] -Let the smaller slot have size $m$, the larger size $m+d$, where -$0\le d\le3$. Replacing endpoint multiplicity $m$ by $m-e$ has exact ratio -\[ - R_{m,d}(e)= - \frac{\binom me}{(d+1)\cdots(d+e)} - 2^{-em+e(e+1)/2}. - \tag{8.21} -\] -Uniformly in the four cell types, -\[ - \sum_{1\le e0 - \tag{8.24a} -\] -on $0\le e\le m/4$ for all sufficiently large $m$. Thus the ratios are -log-convex and attain their maximum at an endpoint. At $e=0$ the ratio is -$O(N^3/n)$, and at $e=\lfloor m/4\rfloor$ it is $n^{-1/2+o(1)}$. Both are -eventually below $1/2$, uniformly, so the series is geometrically decreasing. -\end{proof} - -\begin{lemma}[Global product over near-containment decorations] -Fix a typed full-containment table $L$ and temporarily distinguish every -endpoint cell occurrence. Let $\mathcal S(L)$ be the family obtained by -choosing for each occurrence either deficit $0$ or $1\le e0$ such that, eventually and uniformly, -\[ - \log_2\left[ - k_{co}^2g(j)\frac{(ea^2/m_0)^j}{j!} - \right] - \le-c_0(\log_2n)^2. - \tag{8.28a} -\] -Thus $\Xi_4=2^{-\Omega((\log n)^2)}$. -\end{lemma} - -\begin{proof} -Expand over distinct residual cells and threshold demands before dropping any -constraints. Lemma 6.2 gives (8.26a)--(8.27). Put $L_2=\log_2n$ and -$j=xL_2$. Then -\[ - 1+o(1)\le x\le3/2+o(1), - \qquad - \log_2m_0\ge L_2-6\log_2N. -\] -Using $g(j)\le2^{j^2/2}$ and $k_{co}\le n$, -\[ - \log_2\left[ - k_{co}^2g(j)\frac{(ea^2/m_0)^j}{j!} - \right] - \le2L_2+ - \left(\frac{x^2}{2}-x\right)L_2^2 - +O(L_2\log L_2). -\] -On $[1,3/2]$, $x^2/2-x\le-3/8$. Taking $c_0=1/4$, the lower-order term is -smaller than $L_2^2/8$ for all sufficiently large $n$, uniformly over the floor -perturbations and cell types. -\end{proof} - -\begin{lemma}[Small residual completion] -If $m_0 Date: Fri, 24 Jul 2026 20:15:19 +0300 Subject: [PATCH 27/29] Update the reviewer guide for the corrected split appendices --- 625/REVIEW_GUIDE.md | 72 +++++++++++++++++++++++++++++++-------------- 1 file changed, 50 insertions(+), 22 deletions(-) diff --git a/625/REVIEW_GUIDE.md b/625/REVIEW_GUIDE.md index ef99eed8..625d80f1 100644 --- a/625/REVIEW_GUIDE.md +++ b/625/REVIEW_GUIDE.md @@ -5,8 +5,10 @@ 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 branch containing this guide was cut from repository commit -`ddeabbf8b23b5a89b269cf5fae4ed18549a8001d`. +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”: @@ -21,6 +23,14 @@ The current status is deliberately narrower than “verified solution”: 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 @@ -47,6 +57,13 @@ infinite subsequence or a density-one set. | 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 @@ -97,8 +114,8 @@ Read Section 6. Check: ### Pass C: partial diagonals -Read Section 7 and the replacement text in -[`proofs/SECTIONS_7_9_REVIEW_REWRITE.md`](proofs/SECTIONS_7_9_REVIEW_REWRITE.md). +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; @@ -109,7 +126,10 @@ Check all three ranges separately: ### Pass D: canonical high skeleton -Read Section 8. The critical finite statement is the exact exposure identity: +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 @@ -125,18 +145,22 @@ Then check separately: ### Pass E: residual attachments -Read Section 9. Check: +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; -- the total local increment and row/column norm estimates; -- the deterministic cycle decomposition used to pass from even subgraphs to a - product over simple cycles; -- residual-only cycle enumeration; -- mixed cycles meeting the high matching, including why only the first marked - matching edge costs a factor `2|M|`; +- 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: @@ -179,18 +203,20 @@ nonnegative expansion that records: - cap and no-return constraints; - the split between large and small residual mass. -### 6.4 Weighted residual cycle expansion +### 6.4 Weighted residual restriction -The mixed-cycle bound must exhibit an encoding from every simple cycle meeting -the high matching to: +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 -- one marked and oriented matching edge; -- a sequence of nonempty residual paths; -- deterministic matching transitions. +\[ + \sum_{F\text{ even}}\prod_{e\in F\setminus M}q_e + \le\prod_{e\notin M}(1+q_e). +\] -After the first marked edge, each matching transition is determined by the -current endpoint, so no new factor `|M|` is introduced. The replacement text -states this as a finite kernel lemma. +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 @@ -203,7 +229,7 @@ For every load-bearing `O`, `o`, or `Omega`, record: | 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 traversal | row/column degree lists and matching size | +| 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 @@ -232,6 +258,8 @@ 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 From 92d58f1a7b7ba7667ebed40d220816961934ba3d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:17:31 +0300 Subject: [PATCH 28/29] =?UTF-8?q?Correct=20and=20expand=20the=20Erd=C5=91s?= =?UTF-8?q?=20625=20extensions=20note?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ...ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md | 79 +++++++++++++++---- 1 file changed, 62 insertions(+), 17 deletions(-) diff --git a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md index 373766bf..a0b271df 100644 --- a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md +++ b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.md @@ -100,18 +100,21 @@ Therefore Corollary 1.2 gives immediately \tag{1.4} \] -Using the definitions in (9.5)--(9.6), +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}\theta_{ab}^2+\Lambda_0. + =\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 degree sums factor exactly: +The unrestricted square sum factorizes exactly: \[ - \sum_{a,b}\theta_{ab}^2 + \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). @@ -130,7 +133,7 @@ Since every residual degree is at most `U` and both degree sums are `m_0`, so \[ - \sum_{a,b}\theta_{ab}^2\le e^2U^2. + \sum_{a,b}\widetilde\theta_{ab}^{\,2}\le e^2U^2. \tag{1.8} \] @@ -244,15 +247,15 @@ Define \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 +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`. +Consequently \(A_*>\gamma_4\). Using (5.11) directly and the midpoint definition (5.13), rather than replacing (5.11) by (5.12), gives @@ -432,7 +435,8 @@ For every deterministic graph, \tag{6.1} \] -For fixed `p in (0,1)`, the standard dense-random-graph asymptotic is +For fixed `p in (0,1)`, McDiarmid's refinement of the dense-random-graph +chromatic asymptotic gives \[ \chi(G(n,p)) @@ -440,6 +444,10 @@ For fixed `p in (0,1)`, the standard dense-random-graph asymptotic is \tag{6.2} \] +This literature-dependent extension uses C. McDiarmid, *On the chromatic +number of random graphs*, Random Structures & Algorithms 1 (1990), 435--442, +DOI [`10.1002/rsa.3240010404`](https://doi.org/10.1002/rsa.3240010404). + Applying the same formula to the complement gives \[ @@ -476,29 +484,37 @@ Every coclour class has size at most `h(G)`, so \tag{7.1} \] -The standard second-order estimates for `G(n,1/2)` give +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 +and, writing \(d_\chi(G)=n/\chi(G)\), \[ - \chi(G)= - \frac{n}{2\log_2n-2\log_2\log_2n+O(1)} + d_\chi(G)=2\log_2n-2\log_2\log_2n+O(1) \tag{7.3} \] -with high probability. The two denominators differ by only `O(1)`, hence +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 \[ - \boxed{\chi(G)-\zeta(G)=O\left(\frac{n}{(\ln n)^2}\right)} + 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} \] -with high probability. +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 @@ -726,7 +742,36 @@ leaving a substantial fixed first-moment margin. --- -## 10. Recommended integration order +## 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). From 79ad43f5ec14a9e56ea294f7e14f94415b8d9e2e Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Fri, 24 Jul 2026 20:18:16 +0300 Subject: [PATCH 29/29] Replace the extensions TeX with a corrected verified synopsis --- ...RDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex | 368 +++++------------- 1 file changed, 96 insertions(+), 272 deletions(-) diff --git a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex index d08f7906..2ae1ecf8 100644 --- a/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex +++ b/625/proofs/ERDOS625_EXTENSIONS_AND_SIMPLIFICATIONS.tex @@ -1,332 +1,156 @@ \documentclass[11pt]{article} \usepackage[margin=1in]{geometry} +\usepackage[T1]{fontenc} +\usepackage[utf8]{inputenc} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage[hidelinks]{hyperref} -\usepackage{enumitem} +\usepackage{microtype} +\setlength{\emergencystretch}{3em} \newtheorem{lemma}{Lemma} \newtheorem{proposition}{Proposition} -\newtheorem{corollary}{Corollary} -\newcommand{\E}{\mathbb E} -\newcommand{\cE}{\mathcal E} -\newcommand{\cP}{\mathcal P} -\title{Erd\H{o}s Problem 625: Result Extensions and Proof Simplifications} -\author{Research note for the candidate manuscript} +\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 note records exact deductions, finite rational certificates, and -architectural alternatives obtained by re-examining the candidate manuscript -at repository main commit -\begin{center} -\small\ttfamily cda78922ea6c87bfc81f9bf693374dd045dac624 -\end{center} -It is not external peer review, priority verification, or a completed Lean -proof of the final target. Put $q=\ln2$ and $N=\ln n$. +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}. -\section{Exact simplification of the large-residual attachment bound} +Throughout, let \(q=\ln2\) and \(N=\ln n\). -\begin{lemma}[An even completion of residual edges is unique] -Let $M$ be a matching and $R$ any other finite edge set. Put +\section{Direct residual-restriction bound} + +Let \(M\) be a matching and \(R\) a finite residual edge set. For \[ - \cE(M,R)=\{F\subseteq M\cup R:\deg_F(v)\equiv0\pmod2\text{ for every }v\}. + \mathcal E(M,R)=\{F\subseteq M\cup R:\deg_F(v)\equiv0\pmod2 + \text{ for every }v\}, \] -Then +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, \[ - \rho:\cE(M,R)\to\cP(R\setminus M),\qquad \rho(F)=F\setminus M + \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} \] -is injective. -\end{lemma} - -\begin{proof} -If $\rho(F)=\rho(F')$, then $F\mathbin\triangle F'\subseteq M$. The symmetric -difference is even. A nonempty subset of a matching has degree one at every -incident vertex, so it is not even. Thus $F\mathbin\triangle F'=\varnothing$. -\end{proof} -\begin{corollary}[Weighted product bound] -For nonnegative residual weights $(q_e)$, extended by zero on $M$, +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_{F\in\cE(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 q_e\right). + \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} \] -\end{corollary} - -Equation (9.12) therefore gives +Only the unrestricted sum factorizes: \[ - \mathcal A(M,j)\le\exp\left(\Lambda_0+\sum_eq_e\right). + \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} \] -Since +Together with \(\Lambda_0\le CU^4/m_0\), this gives \[ - \sum_eq_e=\frac12\sum_{a,b}\theta_{ab}^2+\Lambda_0 + \boxed{\mathcal A(M,j)\le + \exp\!\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} \tag{1.4} \] -and -\[ - \sum_{a,b}\theta_{ab}^2 - =\frac{e^2}{m_0^2} - \left(\sum_ad_a^2\right)\left(\sum_b(d'_b)^2\right) - \le e^2U^2, - \tag{1.5} -\] -while $\Lambda_0\le CU^4/m_0$, we obtain -\[ - \boxed{\mathcal A(M,j) - \le\exp\left\{C\left(U^2+\frac{U^4}{m_0}\right)\right\}.} - \tag{1.6} -\] -For $m_0\ge n/N^6$ and $U=O(N)$ this is $\exp(CN^2)$, stronger than the -current $\exp(CN^8)$ bound. It removes the simple-cycle decomposition, -residual and mixed walk enumeration, $\tau$, and equations (9.15)--(9.18). +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{A stronger central partial-diagonal rate} +\section{Stronger central rate} -\begin{lemma} -Under the hypotheses of Lemma 7.1A, +On the domain of the central partial-diagonal argument, \[ - \Phi_T(z)\le-\frac{1-R}{100}\qquad(1/64\le R\le1). + \boxed{\Phi_T(z)\le-\frac{1-R}{100}}, + \qquad \frac1{64}\le R\le1. \tag{2.1} \] -\end{lemma} - -\begin{proof} -On $[1/64,47/100]$ use -\[ - \Phi_T(z)\le R\ln R+(5q/2-1)R. -\] -The convex function -\[ - f(R)=R\ln R+(5q/2-1)R+\frac{1-R}{100} -\] -has $f(1/64)<-0.0436$ and $f(47/100)<-0.0051$. On -$[47/100,1]$ use -\[ - \Phi_T(z)\le R\ln R+(1-q/2)(1-R). -\] -The convex function -\[ - h(R)=R\ln R+(1-q/2+1/100)(1-R) -\] -has $h(47/100)<-0.0032$ and $h(1)=0$. -\end{proof} +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{Carry the phase-resolved displacement to the theorem} +\section{Constant propagation} -Put +Writing \(A(\delta)=q-D_4(\delta)\), equation (5.11) and the midpoint choice give \[ - A(\delta)=q-D_4(\delta),\qquad - A_*=\min_{0\le\delta\le1}A(\delta). + k_\chi^- -k_{co} + =\left(\frac{q^2}{8}A(\delta)+o(1)\right)\frac{n}{N^3}. \tag{3.1} \] -Continuity and Lemma 5.1 give $A_*>\gamma_4$, where -$\gamma_4=\ln(200/153)$. Equation (5.11), the midpoint construction, and the -$o(n/N^3)$ amplification loss give -\[ - \boxed{\chi(G_n)-\zeta(G_n) - \ge\left(\frac{q^2}{8}A(\delta_n)-o(1)\right)\frac{n}{N^3}} - \tag{3.2} -\] -with high probability. Thus the fixed displayed constant can be increased -from $q^2\gamma_4/32$ to $q^2\gamma_4/8$ without changing the witness or -second-moment argument. +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{A stronger four-support entropy certificate} +\section{Exact entropy certificates} -\begin{proposition} -For every phase, +The exact rational checker verifies the four-support bounds \[ - \frac{12}{5}q<\lambda_4<\frac{21}{5}q. + \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} \] -Moreover +Combined with (3.1), the candidate coefficient is \[ - L(12q/5)<3/10,\quad H(3q)<1/50, - \quad L(3q)<3/25,\quad H(21q/5)<1/5. + \frac{(\ln2)^2}{8}\ln\frac{50}{33} + =0.0249544559\ldots. \tag{4.2} \] -Consequently -\[ - D_4(\delta)<\ln(33/25),\qquad q-D_4(\delta)>\ln(50/33). - \tag{4.3} -\] -\end{proposition} - -Put $x=2^{1/10}$. The rational intervals -\[ - 0.6931471/2$ this is a direct lower bound on $\chi(G)-\zeta(G)$; for $p<1/2$ -it applies to the complementary chromatic gap. Thus $p=1/2$ is the unique -fixed-density point where the first-order comparison cancels. - -\section{A standard upper bound} - -If $h(G)=\max\{\alpha(G),\omega(G)\}$, then $\zeta(G)\ge n/h(G)$. The standard -second-order estimates at $p=1/2$ give -\[ - h(G)=2\log_2n-2\log_2\log_2n+O(1) -\] -and -\[ - \chi(G)=\frac{n}{2\log_2n-2\log_2\log_2n+O(1)}. -\] -Hence -\[ - \boxed{\chi(G)-\zeta(G)=O\left(\frac{n}{(\ln n)^2}\right)} - \tag{7.1} -\] -with high probability. - -\section{An exactly certified three-size alternative} - -Let $S_3=\{2,3,5\}$ and -\[ - D_3(\delta)=\mathcal F_{S_+}(T_0)-\mathcal F_{S_3}(T_0). -\] -The same omitted-mass method gives a rigorous positive advantage. - -\begin{proposition} -For every target $2/q\le T\le1+2/q$, the $S_3$ tilt satisfies -\[ - \frac{29}{10}q<\lambda_3<\frac{21}{5}q. - \tag{8.1} -\] -Moreover +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}>0. - \tag{8.2} + q-D_3(\delta)>\ln\frac{400}{391}. + \tag{4.3} \] -\end{proposition} +The three-size support reduces the transportation table from \(4\times4\) to +\(3\times3\), but its complete second-moment chain has not been replayed. -Let $L_3$ be the omitted ratio from deficits $-1,0,1$, let $M_4$ be the -ratio of the deficit-4 weight, and let $H_3$ be the ratio of the tail from six -onward. Exact rational comparisons give -\[ - L_3(29q/10)<\frac15, - \quad H_3(7q/2)<\frac2{25}, - \quad M_4(7q/2)=\frac12, - \tag{8.3} -\] -and -\[ - L_3(7q/2)<\frac2{25}, - \quad H_3(21q/5)<\frac14, - \quad M_4(21q/5)<\frac58. - \tag{8.4} -\] -The low ratio decreases with the tilt, the high ratio increases, and $M_4$ -increases because the retained mean stays below four. Splitting at $7q/2$ -therefore bounds the total omitted ratio by $191/200$. +\section{Additional consequences} -With $x=2^{1/10}$, the endpoint checks reduce to integer powers. Two of the -load-bearing inequalities are -\[ - 5(1+x^{34}+x^{58})