From e3bc89a41c4e6fba41b20914c3b427b97af626b1 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 00:13:32 +0300 Subject: [PATCH 01/47] Formalize matching-restriction product bound --- .../Section9MatchingRestrictionProduct.lean | 140 ++++++++++++++++++ 1 file changed, 140 insertions(+) create mode 100644 625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean b/625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean new file mode 100644 index 00000000..8b0b7352 --- /dev/null +++ b/625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean @@ -0,0 +1,140 @@ +import Erdos625.Section9FixedFEvenAggregation +import Erdos625.EvenMatchingRestriction +import Mathlib.Tactic + +/-! +# Section IX: direct product bound from matching restriction + +For an exposed bipartite matching `M`, an even edge set is uniquely determined +by its restriction outside `M`. This gives a direct subset-product bound for +the weighted even-family sum and avoids the cycle/polymer decomposition at the +finite algebraic level. + +The final theorem composes this injection with the already checked fixed-`F` +aggregation. It does not identify the fixed-`F` sum with the actual tagged +attachment expectation, prove the residual-`q` analytic envelope, or establish +Lemma 9.1. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +/-- On the finite family of even bipartite edge sets, deleting a matching is +injective. Equivalently, an even completion of a prescribed outside-matching +edge set is unique when it exists. -/ +theorem sdiff_matching_injective_on_bipartiteEvenEdgeSets + {A B : Type*} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (M : Finset (A × B)) (hM : IsBipartiteMatching M) : + ∀ F ∈ bipartiteEvenEdgeSets A B, + ∀ G ∈ bipartiteEvenEdgeSets A B, + F \ M = G \ M → F = G := by + intro F hF G hG hdiff + apply bipartiteEdgeMatrix_injective + apply evenMatrix_eq_of_eq_on_residual + (bipartiteEdgeMatrix F) (bipartiteEdgeMatrix G) + (fun a b => (a, b) ∈ M) (fun a b => (a, b) ∉ M) + · apply (bipartiteEdgeMatrix_even_iff F).2 + apply (bipartiteEvenEdgeSet_iff_isBipartiteEven F).2 + simpa [bipartiteEvenEdgeSets] using hF + · apply (bipartiteEdgeMatrix_even_iff G).2 + apply (bipartiteEvenEdgeSet_iff_isBipartiteEven G).2 + simpa [bipartiteEvenEdgeSets] using hG + · exact hM.1 + · intro a b _hab + by_cases hmem : (a, b) ∈ M + · exact Or.inl hmem + · exact Or.inr hmem + · intro a b _hab + by_cases hmem : (a, b) ∈ M + · exact Or.inl hmem + · exact Or.inr hmem + · intro a b hab + have hmem : ((a, b) ∈ F) ↔ ((a, b) ∈ G) := by + have h := congrArg (fun S : Finset (A × B) => (a, b) ∈ S) hdiff + simpa [hab] using h + by_cases hFmem : (a, b) ∈ F + · have hGmem : (a, b) ∈ G := hmem.mp hFmem + simp [bipartiteEdgeMatrix, hFmem, hGmem] + · have hGmem : (a, b) ∉ G := by + intro hG + exact hFmem (hmem.mpr hG) + simp [bipartiteEdgeMatrix, hFmem, hGmem] + +/-- The weighted even-family sum is bounded directly by the full subset product +on the cells outside the matching. No cycle decomposition is used. -/ +theorem weighted_evenSubgraph_ennreal_matching_product + {A B : Type*} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (q : A → B → ENNReal) (M : Finset (A × B)) + (hM : IsBipartiteMatching M) : + (∑ F ∈ bipartiteEvenEdgeSets A B, + edgeWeightOutsideENN q M F) ≤ + ∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + q e.1 e.2) := by + classical + unfold edgeWeightOutsideENN + calc + (∑ F ∈ bipartiteEvenEdgeSets A B, + ∏ e ∈ F \ M, q e.1 e.2) = + ∑ S ∈ Finset.image (fun F : Finset (A × B) => F \ M) + (bipartiteEvenEdgeSets A B), + ∏ e ∈ S, q e.1 e.2 := by + symm + rw [Finset.sum_image] + exact sdiff_matching_injective_on_bipartiteEvenEdgeSets M hM + _ ≤ ∑ S ∈ Finset.powerset + ((Finset.univ : Finset (A × B)) \ M), + ∏ e ∈ S, q e.1 e.2 := by + apply Finset.sum_le_sum_of_subset + exact Finset.image_subset_iff.mpr fun F _hF => + Finset.mem_powerset.mpr (by + intro e he + exact Finset.mem_sdiff.mpr + ⟨Finset.mem_univ e, (Finset.mem_sdiff.mp he).2⟩) + _ = ∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + q e.1 e.2) := by + simp +decide [Finset.prod_add, add_comm] + +/-- Direct matching-restriction replacement for the polymer-product endpoint +in the finite capped fixed-`F` aggregation. -/ +theorem residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct + {A B : Type*} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (M : Finset (A × B)) (R : ℕ) (row : A → ℕ) (col : B → ℕ) + (htotal : Finset.univ.sum row = Finset.univ.sum col) + (hm : 0 < Finset.univ.sum row) + (hM : IsBipartiteMatching M) : + residualCappedEvenFixedFSum M R row col htotal ≤ + (∏ a : A, ∏ b : B, + (1 + residualLambda M R row col a b)) * + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + residualQ M R row col e.1 e.2)) := by + calc + residualCappedEvenFixedFSum M R row col htotal ≤ + (∏ a : A, ∏ b : B, + (1 + residualLambda M R row col a b)) * + (∑ F ∈ bipartiteEvenEdgeSets A B, + edgeWeightOutsideENN (residualQ M R row col) M F) := + residualCappedEvenFixedFSum_le_lambdaProduct_mul_evenWeightSum + M R row col htotal hm + _ ≤ + (∏ a : A, ∏ b : B, + (1 + residualLambda M R row col a b)) * + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + residualQ M R row col e.1 e.2)) := + mul_le_mul_right + (weighted_evenSubgraph_ennreal_matching_product + (residualQ M R row col) M hM) + _ + +#print axioms sdiff_matching_injective_on_bipartiteEvenEdgeSets +#print axioms weighted_evenSubgraph_ennreal_matching_product +#print axioms residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct + +end + +end Erdos625 From 90b83d199b3f7e1e8f181e5a4368dee2edee86f7 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 00:20:00 +0300 Subject: [PATCH 02/47] Add focused Lean check for matching restriction --- .../erdos625-matching-restriction-product.yml | 41 +++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 .github/workflows/erdos625-matching-restriction-product.yml diff --git a/.github/workflows/erdos625-matching-restriction-product.yml b/.github/workflows/erdos625-matching-restriction-product.yml new file mode 100644 index 00000000..2f586929 --- /dev/null +++ b/.github/workflows/erdos625-matching-restriction-product.yml @@ -0,0 +1,41 @@ +name: Erdős 625 matching-restriction product + +on: + pull_request: + paths: + - "625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean" + - ".github/workflows/erdos625-matching-restriction-product.yml" + workflow_dispatch: + +permissions: + contents: read + +jobs: + focused-lean-check: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Reject placeholders and project axioms in the new module + shell: bash + run: | + if grep -nE \ + '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ + 625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean; then + exit 1 + fi + - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 + with: + lake-package-directory: 625/formalization + auto-config: false + build: false + use-mathlib-cache: true + use-github-cache: false + nanoda: false + - name: Compile the module warning-fatally + working-directory: 625/formalization + shell: bash + run: | + mkdir -p .lake/build/lib/lean/Erdos625 + lake env lean -DwarningAsError=true \ + Erdos625/Section9MatchingRestrictionProduct.lean \ + -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionProduct.olean From 860584001d40cfae04f85eccba0b2e7af4d7f3bb Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 00:23:00 +0300 Subject: [PATCH 03/47] Document matching-restriction formalization boundary --- .../MATCHING_RESTRICTION_PRODUCT_AUDIT.md | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md diff --git a/625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md new file mode 100644 index 00000000..0deffde8 --- /dev/null +++ b/625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md @@ -0,0 +1,66 @@ +# Matching-restriction product formalization audit + +**Date:** 25 July 2026 +**Target module:** `Erdos625/Section9MatchingRestrictionProduct.lean` +**Status:** focused finite Lean checkpoint; not Lemma 9.1 or `Erdos625Statement`. + +## Exact claims + +The module proves three finite statements. + +1. If `M` is a bipartite matching, the map + + ```text + F ↦ F \ M + ``` + + is injective on the finite family of bipartite even edge sets. + +2. For arbitrary `ENNReal` cell weights, + + ```text + sum_{F even} product_{e in F\M} q_e + <= product_{e notin M} (1 + q_e). + ``` + +3. The existing capped fixed-`F` aggregation is bounded by the common local + `residualLambda` product times this direct outside-matching product. + +## Proof dependencies + +The proof reuses only accepted finite modules: + +- `BipartiteEdgeMatrix.lean` for the injective zero-one incidence encoding and + the equivalence between even edge sets and zero row/column sums over + `ZMod 2`; +- `EvenMatchingRestriction.lean` for uniqueness of an even matrix after its + values away from a row matching are fixed; +- `Section9ActualResidualENNRealPolymerBridge.lean` for the definition of + `edgeWeightOutsideENN` and the finite even-edge family; +- `Section9FixedFEvenAggregation.lean` for the previously checked fixed-`F` + threshold expansion and aggregation. + +No cycle decomposition, walk kernel, marked-cycle encoder, asymptotic estimate, +probability conditioning, or external theorem is used. + +## Trust checks + +The source contains no `sorry`, `admit`, project-defined `axiom`, `constant`, or +`unsafe` declaration. Each public theorem is followed by `#print axioms`. +The focused workflow compiles the module with `-DwarningAsError=true`; the full +repository Lean workflow also builds every formalization module with `--wfail`. + +## Deliberate boundary + +This checkpoint does not prove the manuscript's complete large-residual +attachment estimate. Remaining bridges include: + +1. the precise tagged-law identification of the actual attachment numerator; +2. a finite bound on the direct product in terms of the total `residualQ` mass; +3. the deterministic estimate + `sum residualQ = O(U^2 + U^4/m_0)` under the large-residual hypotheses; +4. the asymptotic specialization to `exp(O((log n)^2))`; +5. the global Section 8 skeleton sum and Proposition 9.2. + +The module is therefore a genuine simplification of the finite Section IX +algebra, but not a completed proof of the theorem. From 35fa4f5aa85a12ae9ae23b7351031cd96dc6305f Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 07:41:14 +0300 Subject: [PATCH 04/47] Fix focused Lean dependency build --- .../workflows/erdos625-matching-restriction-product.yml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/erdos625-matching-restriction-product.yml b/.github/workflows/erdos625-matching-restriction-product.yml index 2f586929..61c6c4ed 100644 --- a/.github/workflows/erdos625-matching-restriction-product.yml +++ b/.github/workflows/erdos625-matching-restriction-product.yml @@ -4,6 +4,7 @@ on: pull_request: paths: - "625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean" + - "625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md" - ".github/workflows/erdos625-matching-restriction-product.yml" workflow_dispatch: @@ -27,15 +28,15 @@ jobs: with: lake-package-directory: 625/formalization auto-config: false - build: false + build: true + build-args: --wfail use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Compile the module warning-fatally + - name: Compile the module warning-fatally after dependency build working-directory: 625/formalization shell: bash run: | - mkdir -p .lake/build/lib/lean/Erdos625 lake env lean -DwarningAsError=true \ Erdos625/Section9MatchingRestrictionProduct.lean \ -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionProduct.olean From 27c97b8375deb9f794d5e0774b396f6908730744 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 07:46:19 +0300 Subject: [PATCH 05/47] Add direct Section 9 attachment envelope --- .../Section9MatchingRestrictionEnvelope.lean | 317 ++++++++++++++++++ 1 file changed, 317 insertions(+) create mode 100644 625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean new file mode 100644 index 00000000..559e23f1 --- /dev/null +++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean @@ -0,0 +1,317 @@ +import Erdos625.Section9MatchingRestrictionProduct +import Erdos625.Section9ActualResidualENNRealExpBridge +import Erdos625.Section9FixedFFubiniBridge +import Erdos625.Section9ResidualQQuadratic +import Erdos625.Section9ResidualLambdaTotalBound +import Erdos625.Section9ThetaCap +import Erdos625.ConfigurationThetaMoments +import Mathlib.Tactic + +/-! +# Section IX: direct matching-restriction attachment envelope + +This module continues the direct matching-restriction route. It first identifies +its fixed-even-family bound with the literal event-restricted attachment +numerator. It then proves the global quadratic configuration-theta estimate, +sums the literal residual-q bound at scale `U^2`, and combines the two finite +products into one exponential envelope. + +The result is pointwise in the finite residual data. It does not perform the +Section VIII skeleton sum, specialize to the midpoint profile, or prove +`Erdos625Statement`. +-/ + +universe u v + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +/-- Exact global factorization of the squared configuration-cell parameters. -/ +theorem sum_configurationCellTheta_sq_global + {A : Type u} {B : Type v} [Fintype A] [Fintype B] + (row : A → ℕ) (col : B → ℕ) (m : ℕ) : + (∑ a, ∑ b, configurationCellTheta row col m a b ^ 2) = + (eulerENNReal / (m : ENNReal)) ^ 2 * + (∑ a, (row a : ENNReal) ^ 2) * + (∑ b, (col b : ENNReal) ^ 2) := by + calc + (∑ a, ∑ b, configurationCellTheta row col m a b ^ 2) = + ∑ a, ((eulerENNReal / (m : ENNReal)) ^ 2 * + (row a : ENNReal) ^ 2) * + (∑ b, (col b : ENNReal) ^ 2) := by + apply Finset.sum_congr rfl + intro a _ + simpa only [mul_assoc] using + (sum_configurationCellTheta_sq_row row col m a) + _ = (∑ a, (eulerENNReal / (m : ENNReal)) ^ 2 * + (row a : ENNReal) ^ 2) * + (∑ b, (col b : ENNReal) ^ 2) := by + rw [Finset.sum_mul] + _ = ((eulerENNReal / (m : ENNReal)) ^ 2 * + (∑ a, (row a : ENNReal) ^ 2)) * + (∑ b, (col b : ENNReal) ^ 2) := by + rw [Finset.mul_sum] + _ = (eulerENNReal / (m : ENNReal)) ^ 2 * + (∑ a, (row a : ENNReal) ^ 2) * + (∑ b, (col b : ENNReal) ^ 2) := by + rfl + +/-- Under equal positive total mass and degree caps, the complete quadratic +configuration-theta mass is at most `e^2 U^2`. -/ +theorem sum_configurationCellTheta_sq_le_euler_sq_cap_sq + {A : Type u} {B : Type v} [Fintype A] [Fintype B] + (row : A → ℕ) (col : B → ℕ) (m U : ℕ) + (hm : 0 < m) + (hrowCap : ∀ a, row a ≤ U) (hcolCap : ∀ b, col b ≤ U) + (hrowTotal : ∑ a, row a = m) (hcolTotal : ∑ b, col b = m) : + (∑ a, ∑ b, configurationCellTheta row col m a b ^ 2) ≤ + eulerENNReal ^ 2 * (U : ENNReal) ^ 2 := by + have hrow := + degreeSquareSum_ennreal_le_cap_mul_total row U m hrowCap hrowTotal + have hcol := + degreeSquareSum_ennreal_le_cap_mul_total col U m hcolCap hcolTotal + calc + (∑ a, ∑ b, configurationCellTheta row col m a b ^ 2) = + (eulerENNReal / (m : ENNReal)) ^ 2 * + (∑ a, (row a : ENNReal) ^ 2) * + (∑ b, (col b : ENNReal) ^ 2) := + sum_configurationCellTheta_sq_global row col m + _ ≤ (eulerENNReal / (m : ENNReal)) ^ 2 * + ((U : ENNReal) * (m : ENNReal)) * + (∑ b, (col b : ENNReal) ^ 2) := + mul_le_mul_left + (mul_le_mul_right hrow + ((eulerENNReal / (m : ENNReal)) ^ 2)) + (∑ b, (col b : ENNReal) ^ 2) + _ ≤ (eulerENNReal / (m : ENNReal)) ^ 2 * + ((U : ENNReal) * (m : ENNReal)) * + ((U : ENNReal) * (m : ENNReal)) := + mul_le_mul_right hcol + ((eulerENNReal / (m : ENNReal)) ^ 2 * + ((U : ENNReal) * (m : ENNReal))) + _ = eulerENNReal ^ 2 * (U : ENNReal) ^ 2 := by + have hm0 : (m : ENNReal) ≠ 0 := by + exact_mod_cast hm.ne' + have hmt : (m : ENNReal) ≠ ∞ := ENNReal.natCast_ne_top m + rw [div_eq_mul_inv] + calc + (eulerENNReal * (m : ENNReal)⁻¹) ^ 2 * + ((U : ENNReal) * (m : ENNReal)) * + ((U : ENNReal) * (m : ENNReal)) = + eulerENNReal ^ 2 * (U : ENNReal) ^ 2 * + ((m : ENNReal) * (m : ENNReal)⁻¹) ^ 2 := by + ring + _ = eulerENNReal ^ 2 * (U : ENNReal) ^ 2 := by + rw [ENNReal.mul_inv_cancel hm0 hmt, one_pow, mul_one] + +/-- One absolute finite constant bounds the total literal residual-q mass at +scale `U^2`, with no factor depending on the number of row or column types. -/ +theorem existsAbsoluteResidualQTotalBound_of_degreeCaps : + ∃ κ : ENNReal, 0 < κ ∧ κ ≠ ∞ ∧ + ∀ {A : Type u} {B : Type v} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (M : Finset (A × B)) (U R m : ℕ) + (row : A → ℕ) (col : B → ℕ), + 0 < m → + (∑ a, row a) = m → + (∑ b, col b) = m → + (∀ a, row a ≤ U) → + (∀ b, col b ≤ U) → + R = U / 2 → + 2 ^ U ≤ m ^ 3 → + (∑ a, ∑ b, residualQ M R row col a b) ≤ + κ * (U : ENNReal) ^ 2 := by + obtain ⟨K, hKpos, hKtop, hquadratic⟩ := + existsAbsoluteResidualQQuadraticBound + have heulerPos : 0 < eulerENNReal := by + rw [eulerENNReal, ENNReal.ofReal_pos] + exact Real.exp_pos 1 + have heulerTop : eulerENNReal ≠ ∞ := ENNReal.ofReal_ne_top + refine ⟨K * eulerENNReal ^ 2, + ENNReal.mul_pos hKpos.ne' (pow_ne_zero 2 heulerPos.ne'), + ENNReal.mul_ne_top hKtop (ENNReal.pow_ne_top heulerTop), ?_⟩ + intro A B _ _ _ _ M U R m row col hm hrowTotal hcolTotal + hrowCap hcolCap hR hpow + have htheta : ∀ a b, (a, b) ∉ M → + (configurationCellTheta row col m a b).toReal ≤ + Real.exp 1 * (U : ℝ) ^ 2 / (m : ℝ) := by + intro a b _ + exact configurationCellTheta_toReal_le_of_caps + row col m U a b hm (hrowCap a) (hcolCap b) + have hqtheta : ∀ a b, + residualQ M R row col a b ≤ + K * configurationCellTheta row col m a b ^ 2 := + hquadratic M U R m row col hm hrowTotal hR htheta hpow + calc + (∑ a, ∑ b, residualQ M R row col a b) ≤ + ∑ a, ∑ b, + K * configurationCellTheta row col m a b ^ 2 := by + exact Finset.sum_le_sum fun a _ => + Finset.sum_le_sum fun b _ => hqtheta a b + _ = K * (∑ a, ∑ b, + configurationCellTheta row col m a b ^ 2) := by + rw [Finset.mul_sum] + apply Finset.sum_congr rfl + intro a _ + rw [Finset.mul_sum] + _ ≤ K * (eulerENNReal ^ 2 * (U : ENNReal) ^ 2) := + mul_le_mul_right + (sum_configurationCellTheta_sq_le_euler_sq_cap_sq + row col m U hm hrowCap hcolCap hrowTotal hcolTotal) K + _ = (K * eulerENNReal ^ 2) * (U : ENNReal) ^ 2 := by + ring + +/-- The literal event-restricted attachment numerator inherits the direct +matching-restriction product bound through the exact fixed-family Fubini +identity. -/ +theorem residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct + {A B : Type*} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (M : Finset (A × B)) (R : ℕ) (row : A → ℕ) (col : B → ℕ) + (htotal : Finset.univ.sum row = Finset.univ.sum col) + (hm : 0 < Finset.univ.sum row) + (hM : IsBipartiteMatching M) : + residualActualAttachmentNumerator M R row col htotal ≤ + (∏ a : A, ∏ b : B, (1 + residualLambda M R row col a b)) * + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + residualQ M R row col e.1 e.2)) := by + rw [residualActualAttachmentNumerator_eq_residualCappedEvenFixedFSum] + exact residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct + M R row col htotal hm hM + +/-- Generic exponential endpoint for the lambda product and the direct +outside-matching residual-q product. -/ +theorem lambda_matching_products_le_exp_of_sum_bounds + {A B : Type*} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (lambda q : A → B → ENNReal) (M : Finset (A × B)) + (lambdaBound qBound : ENNReal) + (hlambda : (∑ a, ∑ b, lambda a b) ≤ lambdaBound) + (hq : (∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + q e.1 e.2) ≤ qBound) : + ((∏ a, ∏ b, (1 + lambda a b)) * + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + q e.1 e.2))) ≤ + EReal.exp (((lambdaBound + qBound : ENNReal) : EReal)) := by + have hlambdaProduct : + (∏ a, ∏ b, (1 + lambda a b)) ≤ + EReal.exp (((∑ a, ∑ b, lambda a b : ENNReal) : EReal)) := by + rw [← Fintype.prod_prod_type', ← Fintype.sum_prod_type'] + exact ennreal_polymer_product_le_ereal_exp_sum + (Finset.univ : Finset (A × B)) (fun x => lambda x.1 x.2) + have hqProduct : + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + q e.1 e.2)) ≤ + EReal.exp (((∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + q e.1 e.2 : ENNReal) : EReal)) := + ennreal_polymer_product_le_ereal_exp_sum + ((Finset.univ : Finset (A × B)) \ M) (fun e => q e.1 e.2) + calc + ((∏ a, ∏ b, (1 + lambda a b)) * + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + q e.1 e.2))) ≤ + EReal.exp (((∑ a, ∑ b, lambda a b : ENNReal) : EReal)) * + EReal.exp (((∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + q e.1 e.2 : ENNReal) : EReal)) := + mul_le_mul' hlambdaProduct hqProduct + _ = EReal.exp + ((((∑ a, ∑ b, lambda a b : ENNReal) : EReal)) + + (((∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + q e.1 e.2 : ENNReal) : EReal))) := by + rw [EReal.exp_add] + _ = EReal.exp + ((((∑ a, ∑ b, lambda a b : ENNReal) + + ∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + q e.1 e.2 : ENNReal) : EReal)) := by + rw [EReal.coe_ennreal_add] + _ ≤ EReal.exp (((lambdaBound + qBound : ENNReal) : EReal)) := by + rw [EReal.exp_le_exp_iff, EReal.coe_ennreal_le_coe_ennreal_iff] + exact add_le_add hlambda hq + +/-- Direct finite large-residual attachment envelope. It has no traversal +parameter and no dependence on the number of profile blocks or matching edges. -/ +theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope : + ∃ kappaLambda kappaQ : ENNReal, + 0 < kappaLambda ∧ kappaLambda ≠ ∞ ∧ + 0 < kappaQ ∧ kappaQ ≠ ∞ ∧ + ∀ {A : Type u} {B : Type v} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (M : Finset (A × B)) (U m : ℕ) + (row : A → ℕ) (col : B → ℕ) + (htotal : Finset.univ.sum row = Finset.univ.sum col), + IsBipartiteMatching M → + 0 < m → + (∑ a, row a) = m → + (∑ b, col b) = m → + (∀ a, row a ≤ U) → + (∀ b, col b ≤ U) → + 2 ^ U ≤ m ^ 3 → + ((residualActualAttachmentNumerator M (U / 2) row col htotal : + ENNReal) : EReal) ≤ + EReal.exp + (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) + + kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) := by + obtain ⟨kappaLambda, hkLpos, hkLtop, hkL⟩ := + existsAbsoluteResidualLambdaTotalBound + obtain ⟨kappaQ, hkQpos, hkQtop, hkQ⟩ := + existsAbsoluteResidualQTotalBound_of_degreeCaps + refine ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, ?_⟩ + intro A B _ _ _ _ M U m row col htotal hM hm hrow hcol + hrowCap hcolCap hpow + have hbridge := + residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct + M (U / 2) row col htotal (by simpa [hrow] using hm) hM + have hlambda := + hkL M U (U / 2) m row col hm hrow hcol hrowCap hcolCap rfl hpow + have hqAll := + hkQ M U (U / 2) m row col hm hrow hcol hrowCap hcolCap rfl hpow + have hqFull : + (∑ e : A × B, residualQ M (U / 2) row col e.1 e.2) ≤ + kappaQ * (U : ENNReal) ^ 2 := by + simpa only [Fintype.sum_prod_type'] using hqAll + have hqOutside : + (∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + residualQ M (U / 2) row col e.1 e.2) ≤ + kappaQ * (U : ENNReal) ^ 2 := by + calc + (∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + residualQ M (U / 2) row col e.1 e.2) ≤ + ∑ e ∈ (Finset.univ : Finset (A × B)), + residualQ M (U / 2) row col e.1 e.2 := by + exact Finset.sum_le_sum_of_subset Finset.sdiff_subset + _ = ∑ e : A × B, + residualQ M (U / 2) row col e.1 e.2 := by + simp + _ ≤ kappaQ * (U : ENNReal) ^ 2 := hqFull + have hproduct := + lambda_matching_products_le_exp_of_sum_bounds + (residualLambda M (U / 2) row col) + (residualQ M (U / 2) row col) M + (kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal)) + (kappaQ * (U : ENNReal) ^ 2) hlambda hqOutside + calc + ((residualActualAttachmentNumerator M (U / 2) row col htotal : + ENNReal) : EReal) ≤ + (((∏ a : A, ∏ b : B, + (1 + residualLambda M (U / 2) row col a b)) * + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + residualQ M (U / 2) row col e.1 e.2)) : ENNReal) : EReal) := by + exact_mod_cast hbridge + _ ≤ EReal.exp + (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) + + kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) := + hproduct + +#print axioms sum_configurationCellTheta_sq_global +#print axioms sum_configurationCellTheta_sq_le_euler_sq_cap_sq +#print axioms existsAbsoluteResidualQTotalBound_of_degreeCaps +#print axioms residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct +#print axioms lambda_matching_products_le_exp_of_sum_bounds +#print axioms exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope + +end + +end Erdos625 From 74b0df099da71b3a12a9cb41287d92f556af3f2d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 07:46:42 +0300 Subject: [PATCH 06/47] Document the direct attachment-envelope boundary --- .../MATCHING_RESTRICTION_ENVELOPE_AUDIT.md | 91 +++++++++++++++++++ 1 file changed, 91 insertions(+) create mode 100644 625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md diff --git a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md new file mode 100644 index 00000000..e3405ecc --- /dev/null +++ b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md @@ -0,0 +1,91 @@ +# Audit: direct matching-restriction attachment envelope + +## Scope + +This audit accompanies `Erdos625/Section9MatchingRestrictionEnvelope.lean`. +The branch is stacked on PR #34 and therefore assumes the finite +matching-restriction product theorem from +`Section9MatchingRestrictionProduct.lean`. + +## New checked targets + +The new module is intended to prove the following finite statements. + +1. The complete square mass of the configuration-cell parameters factorizes as + + \[ + \sum_{a,b}\theta_{ab}^2 + =\left(\frac e m\right)^2 + \left(\sum_a d_a^2\right) + \left(\sum_b (d_b')^2\right). + \] + +2. If both degree families have common positive total `m` and are capped by + `U`, then + + \[ + \sum_{a,b}\theta_{ab}^2\le e^2U^2. + \] + +3. The existing pointwise quadratic bound on `residualQ` therefore sums to + + \[ + \sum_{a,b}q_{ab}\le \kappa_Q U^2 + \] + + for one absolute positive finite constant. + +4. The exact fixed-family Fubini identity transports the direct product theorem + of PR #34 to the literal event-restricted attachment numerator. + +5. Combining the lambda and residual-q products gives + + \[ + \mathcal A(M,j) + \le + \exp\!\left( + \kappa_\Lambda\frac{U^4}{m} + +\kappa_Q U^2 + \right). + \] + +This statement has no traversal parameter, no factor depending on the number +of profile blocks, and no factor depending on the number of matching edges. + +## Dependencies reused + +- `residualActualAttachmentNumerator_eq_residualCappedEvenFixedFSum`; +- `residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct` from the + stacked PR #34; +- `existsAbsoluteResidualQQuadraticBound`; +- `existsAbsoluteResidualLambdaTotalBound`; +- exact degree-square and configuration-theta identities from + `ConfigurationThetaMoments.lean`; +- `ennreal_polymer_product_le_ereal_exp_sum` for finite products. + +## Trust gates + +The focused workflow: + +- rejects `sorry`, `admit`, `sorryAx`, project `axiom`/`constant`, and `unsafe`; +- builds the pinned Lean 4.31/mathlib project with warnings fatal; +- compiles the new module directly with `-DwarningAsError=true`; +- prints the axioms of every new public theorem. + +The ordinary repository Lean workflow also runs because this PR changes the +formalization tree. + +## Deliberate boundary + +This module still does not prove the complete Erdős 625 theorem. In particular +it does not: + +- sum the Section VIII bare skeleton weights; +- specialize the envelope to the midpoint profile and produce the eventual + `o(n/(log n)^4)` coefficient; +- update the root aggregate or generated self-contained checkpoint; +- prove the chromatic lower tail, rare seed, or final event intersection. + +The next integration step, after review, is a profile-level asymptotic adapter +showing that the displayed exponent is `o(amplificationBase n)` uniformly over +attained canonical demands. From 957bba7aff9cf34c3c00c738d0ec1d751d444a5f Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 07:46:55 +0300 Subject: [PATCH 07/47] Add focused Lean gate for direct attachment envelope --- ...erdos625-matching-restriction-envelope.yml | 42 +++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 .github/workflows/erdos625-matching-restriction-envelope.yml diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml new file mode 100644 index 00000000..aadd804b --- /dev/null +++ b/.github/workflows/erdos625-matching-restriction-envelope.yml @@ -0,0 +1,42 @@ +name: Erdős 625 matching-restriction envelope + +on: + pull_request: + paths: + - "625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean" + - "625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md" + - ".github/workflows/erdos625-matching-restriction-envelope.yml" + workflow_dispatch: + +permissions: + contents: read + +jobs: + focused-lean-check: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Reject placeholders and project axioms in the new module + shell: bash + run: | + if grep -nE \ + '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ + 625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean; then + exit 1 + fi + - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 + with: + lake-package-directory: 625/formalization + auto-config: false + build: true + build-args: --wfail + use-mathlib-cache: true + use-github-cache: false + nanoda: false + - name: Compile the module warning-fatally + working-directory: 625/formalization + shell: bash + run: | + lake env lean -DwarningAsError=true \ + Erdos625/Section9MatchingRestrictionEnvelope.lean \ + -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionEnvelope.olean From 75bec86ce179a37b2bd252a0744edbe7a1637807 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:00:27 +0300 Subject: [PATCH 08/47] Expose focused Lean compiler tail --- .../workflows/erdos625-matching-restriction-envelope.yml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml index aadd804b..f105f67e 100644 --- a/.github/workflows/erdos625-matching-restriction-envelope.yml +++ b/.github/workflows/erdos625-matching-restriction-envelope.yml @@ -37,6 +37,11 @@ jobs: working-directory: 625/formalization shell: bash run: | + set +e lake env lean -DwarningAsError=true \ Erdos625/Section9MatchingRestrictionEnvelope.lean \ - -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionEnvelope.olean + -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionEnvelope.olean \ + > /tmp/section9-envelope-lean.log 2>&1 + status=$? + tail -n 240 /tmp/section9-envelope-lean.log + exit $status From 4df65ce74095b9d3276cd8d5b57ee88f5738953c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:01:44 +0300 Subject: [PATCH 09/47] Use targeted Lean dependency closure --- .../workflows/erdos625-matching-restriction-envelope.yml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml index f105f67e..dbf15d37 100644 --- a/.github/workflows/erdos625-matching-restriction-envelope.yml +++ b/.github/workflows/erdos625-matching-restriction-envelope.yml @@ -28,19 +28,16 @@ jobs: with: lake-package-directory: 625/formalization auto-config: false - build: true - build-args: --wfail + build: false use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Compile the module warning-fatally + - name: Build the module and dependency closure warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake env lean -DwarningAsError=true \ - Erdos625/Section9MatchingRestrictionEnvelope.lean \ - -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionEnvelope.olean \ + lake build Erdos625.Section9MatchingRestrictionEnvelope --wfail \ > /tmp/section9-envelope-lean.log 2>&1 status=$? tail -n 240 /tmp/section9-envelope-lean.log From 425fe67e91e28f5ebced2c44b7e98028fc134d7a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:07:05 +0300 Subject: [PATCH 10/47] Upload the focused Section 9 compiler log --- .../workflows/erdos625-matching-restriction-envelope.yml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml index dbf15d37..5869a4d4 100644 --- a/.github/workflows/erdos625-matching-restriction-envelope.yml +++ b/.github/workflows/erdos625-matching-restriction-envelope.yml @@ -42,3 +42,10 @@ jobs: status=$? tail -n 240 /tmp/section9-envelope-lean.log exit $status + - name: Upload focused compiler log + if: always() + uses: actions/upload-artifact@v4 + with: + name: section9-matching-envelope-lean-log + path: /tmp/section9-envelope-lean.log + if-no-files-found: ignore From 0c5c0228a02c0978d9a2e6fde0715f011fabad2b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:15:49 +0300 Subject: [PATCH 11/47] Repair the direct attachment-envelope transport --- .../Erdos625/Section9MatchingRestrictionEnvelope.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean index 559e23f1..8d92d8bd 100644 --- a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean +++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean @@ -53,6 +53,7 @@ theorem sum_configurationCellTheta_sq_global _ = ((eulerENNReal / (m : ENNReal)) ^ 2 * (∑ a, (row a : ENNReal) ^ 2)) * (∑ b, (col b : ENNReal) ^ 2) := by + congr 1 rw [Finset.mul_sum] _ = (eulerENNReal / (m : ENNReal)) ^ 2 * (∑ a, (row a : ENNReal) ^ 2) * @@ -295,10 +296,10 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope : calc ((residualActualAttachmentNumerator M (U / 2) row col htotal : ENNReal) : EReal) ≤ - (((∏ a : A, ∏ b : B, - (1 + residualLambda M (U / 2) row col a b)) * - (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, - (1 + residualQ M (U / 2) row col e.1 e.2)) : ENNReal) : EReal) := by + ((∏ a : A, ∏ b : B, + (1 + residualLambda M (U / 2) row col a b)) : EReal) * + ((∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + residualQ M (U / 2) row col e.1 e.2)) : EReal) := by exact_mod_cast hbridge _ ≤ EReal.exp (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) + From 32750462cc5fc8b568e0a3b97dee29c0e6f33bc1 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:24:04 +0300 Subject: [PATCH 12/47] Use the exact ENNReal-to-EReal order bridge --- .../Section9MatchingRestrictionEnvelope.lean | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean index 8d92d8bd..141895a8 100644 --- a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean +++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean @@ -293,18 +293,15 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope : (residualQ M (U / 2) row col) M (kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal)) (kappaQ * (U : ENNReal) ^ 2) hlambda hqOutside - calc - ((residualActualAttachmentNumerator M (U / 2) row col htotal : + have hbridgeE : + ((residualActualAttachmentNumerator M (U / 2) row col htotal : ENNReal) : EReal) ≤ - ((∏ a : A, ∏ b : B, - (1 + residualLambda M (U / 2) row col a b)) : EReal) * - ((∏ e ∈ (Finset.univ : Finset (A × B)) \ M, - (1 + residualQ M (U / 2) row col e.1 e.2)) : EReal) := by - exact_mod_cast hbridge - _ ≤ EReal.exp - (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) + - kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) := - hproduct + (((∏ a : A, ∏ b : B, + (1 + residualLambda M (U / 2) row col a b)) * + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + residualQ M (U / 2) row col e.1 e.2)) : ENNReal) : EReal) := + EReal.coe_ennreal_le_coe_ennreal_iff.mpr hbridge + exact hbridgeE.trans hproduct #print axioms sum_configurationCellTheta_sq_global #print axioms sum_configurationCellTheta_sq_le_euler_sq_cap_sq From 0d627c270424cf12f04da30f31ccf60c9a595f1b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:29:42 +0300 Subject: [PATCH 13/47] State the direct endpoint in its native ENNReal codomain --- .../Section9MatchingRestrictionEnvelope.lean | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean index 141895a8..3e588e6d 100644 --- a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean +++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean @@ -250,8 +250,7 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope : (∀ a, row a ≤ U) → (∀ b, col b ≤ U) → 2 ^ U ≤ m ^ 3 → - ((residualActualAttachmentNumerator M (U / 2) row col htotal : - ENNReal) : EReal) ≤ + residualActualAttachmentNumerator M (U / 2) row col htotal ≤ EReal.exp (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) + kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) := by @@ -293,15 +292,7 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope : (residualQ M (U / 2) row col) M (kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal)) (kappaQ * (U : ENNReal) ^ 2) hlambda hqOutside - have hbridgeE : - ((residualActualAttachmentNumerator M (U / 2) row col htotal : - ENNReal) : EReal) ≤ - (((∏ a : A, ∏ b : B, - (1 + residualLambda M (U / 2) row col a b)) * - (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, - (1 + residualQ M (U / 2) row col e.1 e.2)) : ENNReal) : EReal) := - EReal.coe_ennreal_le_coe_ennreal_iff.mpr hbridge - exact hbridgeE.trans hproduct + exact hbridge.trans hproduct #print axioms sum_configurationCellTheta_sq_global #print axioms sum_configurationCellTheta_sq_le_euler_sq_cap_sq From 115006007ffde2c55f1ea8a25d3be7ba4ccb2e3b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:32:47 +0300 Subject: [PATCH 14/47] Specialize the direct envelope to attained profile skeletons --- ...ion9ProfileAttachmentMatchingEnvelope.lean | 68 +++++++++++++++++++ 1 file changed, 68 insertions(+) create mode 100644 625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean new file mode 100644 index 00000000..d414c389 --- /dev/null +++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean @@ -0,0 +1,68 @@ +import Erdos625.Section9MatchingRestrictionEnvelope +import Erdos625.Section9CanonicalDemandProductSpecialization +import Erdos625.Section8ProfileSkeletonWeight + +/-! +# Section IX: attained-profile matching-restriction envelope + +This module specializes the direct finite matching-restriction attachment +bound to the canonical reference witness of an attained profile high skeleton. +It keeps the literal cap/no-return attachment observable and introduces no +cycle traversal or polymer majorant. + +No asymptotic profile substitution or Section VIII skeleton summation is made. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- The direct matching-restriction envelope applies uniformly to every +attained profile high skeleton, with the residual degrees supplied by its +canonical reference witness. -/ +theorem exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope : + ∃ kappaLambda kappaQ : ENNReal, + 0 < kappaLambda ∧ kappaLambda ≠ ∞ ∧ + 0 < kappaQ ∧ kappaQ ≠ ∞ ∧ + ∀ {b n : ℕ} {k : ColoringProfile b} + (row0 : OrderedProfilePartition n k) (U m : ℕ) + (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) + (demand : ProfileCanonicalHighSkeleton k U), + m = canonicalDemandResidualTotal + (profileBlockMargin k) (profileBlockMargin k) U demand → + 0 < m → + 2 ^ U ≤ m ^ 3 → + profileHighSkeletonAttachment row0 U demand ≤ + EReal.exp + (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) + + kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) := by + obtain ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, hbound⟩ := + exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope + refine ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, ?_⟩ + intro b n k row0 U m hcap demand hm hmpos hpow + let witness := canonicalDemandReferenceWitness + (profileBlockMargin k) (profileBlockMargin k) U demand + have hparameters := canonicalReference_residual_parameters + (profileBlockMargin k) (profileBlockMargin k) U + (profileBlockMargin_total_eq_self row0) hcap hcap demand + have hrowSum : (∑ a, residualRowDegree witness a) = m := by + simpa only [canonicalDemandResidualTotal, witness] using hm.symm + have hcolSum : (∑ a, residualColumnDegree witness a) = m := by + exact hparameters.2.2.2.symm.trans hrowSum + have hactual := hbound (positiveDemandSupport demand.1) U m + (residualRowDegree witness) (residualColumnDegree witness) + (sum_residualRowDegree_eq_sum_residualColumnDegree + (profileBlockMargin_total_eq_self row0) witness) + hparameters.1 hmpos hrowSum hcolSum hparameters.2.1 hparameters.2.2.1 hpow + unfold profileHighSkeletonAttachment + simpa only [witness] using hactual + +#print axioms exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope + +end + +end Erdos625 From 388c1ac558691179b42da13369215c705b2c878b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:33:12 +0300 Subject: [PATCH 15/47] Validate the attained-profile envelope endpoint --- .../erdos625-matching-restriction-envelope.yml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml index 5869a4d4..6e4752fd 100644 --- a/.github/workflows/erdos625-matching-restriction-envelope.yml +++ b/.github/workflows/erdos625-matching-restriction-envelope.yml @@ -4,6 +4,7 @@ on: pull_request: paths: - "625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean" + - "625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean" - "625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md" - ".github/workflows/erdos625-matching-restriction-envelope.yml" workflow_dispatch: @@ -16,12 +17,13 @@ jobs: runs-on: ubuntu-24.04 steps: - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 - - name: Reject placeholders and project axioms in the new module + - name: Reject placeholders and project axioms in the new modules shell: bash run: | if grep -nE \ '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ - 625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean; then + 625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean \ + 625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -32,15 +34,15 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the module and dependency closure warning-fatally + - name: Build the profile endpoint and dependency closure warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section9MatchingRestrictionEnvelope --wfail \ + lake build Erdos625.Section9ProfileAttachmentMatchingEnvelope --wfail \ > /tmp/section9-envelope-lean.log 2>&1 status=$? - tail -n 240 /tmp/section9-envelope-lean.log + tail -n 260 /tmp/section9-envelope-lean.log exit $status - name: Upload focused compiler log if: always() From d5949794a5b80912fca8329fbf4570c87ecd993d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:33:45 +0300 Subject: [PATCH 16/47] Extend the audit through the attained-profile bridge --- .../MATCHING_RESTRICTION_ENVELOPE_AUDIT.md | 34 +++++++++++++------ 1 file changed, 23 insertions(+), 11 deletions(-) diff --git a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md index e3405ecc..8afd59ba 100644 --- a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md +++ b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md @@ -2,14 +2,18 @@ ## Scope -This audit accompanies `Erdos625/Section9MatchingRestrictionEnvelope.lean`. +This audit accompanies: + +- `Erdos625/Section9MatchingRestrictionEnvelope.lean`; +- `Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean`. + The branch is stacked on PR #34 and therefore assumes the finite matching-restriction product theorem from `Section9MatchingRestrictionProduct.lean`. ## New checked targets -The new module is intended to prove the following finite statements. +The first module is intended to prove the following finite statements. 1. The complete square mass of the configuration-cell parameters factorizes as @@ -49,8 +53,14 @@ The new module is intended to prove the following finite statements. \right). \] -This statement has no traversal parameter, no factor depending on the number -of profile blocks, and no factor depending on the number of matching edges. +The second module specializes this statement to every attained profile high +skeleton by using its canonical reference witness, literal positive-demand +matching support, residual degree caps, equal residual totals, and the exact +definition of `profileHighSkeletonAttachment`. + +The resulting profile theorem has no traversal parameter, no factor depending +on the number of profile blocks, and no factor depending on the number of +matching edges. ## Dependencies reused @@ -61,15 +71,17 @@ of profile blocks, and no factor depending on the number of matching edges. - `existsAbsoluteResidualLambdaTotalBound`; - exact degree-square and configuration-theta identities from `ConfigurationThetaMoments.lean`; -- `ennreal_polymer_product_le_ereal_exp_sum` for finite products. +- `ennreal_polymer_product_le_ereal_exp_sum` for finite products; +- `canonicalReference_residual_parameters` and + `profileBlockMargin_total_eq_self` for the attained-profile specialization. ## Trust gates The focused workflow: - rejects `sorry`, `admit`, `sorryAx`, project `axiom`/`constant`, and `unsafe`; -- builds the pinned Lean 4.31/mathlib project with warnings fatal; -- compiles the new module directly with `-DwarningAsError=true`; +- prepares the pinned Lean 4.31/mathlib project; +- builds the profile endpoint and its dependency closure with `--wfail`; - prints the axioms of every new public theorem. The ordinary repository Lean workflow also runs because this PR changes the @@ -77,12 +89,12 @@ formalization tree. ## Deliberate boundary -This module still does not prove the complete Erdős 625 theorem. In particular -it does not: +These modules still do not prove the complete Erdős 625 theorem. In particular +they do not: - sum the Section VIII bare skeleton weights; -- specialize the envelope to the midpoint profile and produce the eventual - `o(n/(log n)^4)` coefficient; +- specialize the exponent to the midpoint phase and prove the eventual + `O((log n)^2)` or `o(n/(log n)^4)` scale; - update the root aggregate or generated self-contained checkpoint; - prove the chromatic lower tail, rare seed, or final event intersection. From 64bde7cb2d6c06686c77fa9a97a25df97ac6da35 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:36:57 +0300 Subject: [PATCH 17/47] Add the direct profile log-square adapter --- ...ion9ProfileAttachmentMatchingLogScale.lean | 198 ++++++++++++++++++ 1 file changed, 198 insertions(+) create mode 100644 625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean new file mode 100644 index 00000000..64ffd228 --- /dev/null +++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean @@ -0,0 +1,198 @@ +import Erdos625.Section9ProfileAttachmentMatchingEnvelope +import Erdos625.Section9PhaseTwoPowerCorridor +import Erdos625.Section9ResidualRegimeScaleAdapters + +/-! +# Section IX: direct matching-restriction profile log scale + +This module specializes the direct attained-profile attachment envelope to the +large-residual midpoint scale. The new finite exponent + +`kappaLambda * U^4 / m + kappaQ * U^2` + +is uniformly `O((log n)^2)` when `U <= phaseNat n` and +`m >= n / (log n)^6`. No type-cardinality, matching-cardinality, or traversal +parameter remains. + +The theorem is still pointwise in an attained canonical skeleton. It does not +sum the Section VIII skeleton weights or prove the final random-graph event. +-/ + +namespace Erdos625 + +open Filter +open scoped ENNReal Topology + +noncomputable section + +set_option autoImplicit false + +/-- Exact real arithmetic for the direct matching-restriction exponent. -/ +theorem matchingRestrictionEnvelope_bound + (n L U m kappaLambda kappaQ C_U : ℝ) + (hn : 0 < n) + (hL : 0 < L) + (hU0 : 0 ≤ U) + (hm0 : 0 < m) + (hkappaLambda0 : 0 ≤ kappaLambda) + (hkappaQ0 : 0 ≤ kappaQ) + (hCU0 : 0 ≤ C_U) + (hm : n / L ^ 6 ≤ m) + (hU : U ≤ C_U * L) + (hL8 : L ^ 8 ≤ n) : + kappaLambda * U ^ 4 / m + kappaQ * U ^ 2 ≤ + (kappaLambda * C_U ^ 4 + kappaQ * C_U ^ 2) * L ^ 2 := by + have hn_le_mL6 : n ≤ m * L ^ 6 := by + rwa [div_le_iff₀ (pow_pos hL 6)] at hm + have h1m_le_L6n : 1 / m ≤ L ^ 6 / n := by + rw [div_le_div_iff₀ hm0 hn] + simpa [mul_comm] using hn_le_mL6 + have hU4 : U ^ 4 ≤ (C_U * L) ^ 4 := + pow_le_pow_left₀ hU0 hU 4 + have hL10_div_n_le_L2 : L ^ 10 / n ≤ L ^ 2 := by + rw [div_le_iff₀ hn] + calc + L ^ 10 = L ^ 2 * L ^ 8 := by ring + _ ≤ L ^ 2 * n := + mul_le_mul_of_nonneg_left hL8 (by positivity) + have hterm1Base : U ^ 4 / m ≤ C_U ^ 4 * L ^ 2 := by + calc + U ^ 4 / m = U ^ 4 * (1 / m) := by ring + _ ≤ (C_U * L) ^ 4 * (L ^ 6 / n) := + mul_le_mul hU4 h1m_le_L6n (by positivity) (by positivity) + _ = C_U ^ 4 * (L ^ 10 / n) := by ring + _ ≤ C_U ^ 4 * L ^ 2 := + mul_le_mul_of_nonneg_left hL10_div_n_le_L2 (by positivity) + have hterm1 : kappaLambda * U ^ 4 / m ≤ + kappaLambda * C_U ^ 4 * L ^ 2 := by + calc + kappaLambda * U ^ 4 / m = kappaLambda * (U ^ 4 / m) := by ring + _ ≤ kappaLambda * (C_U ^ 4 * L ^ 2) := + mul_le_mul_of_nonneg_left hterm1Base hkappaLambda0 + _ = kappaLambda * C_U ^ 4 * L ^ 2 := by ring + have hU2 : U ^ 2 ≤ (C_U * L) ^ 2 := + pow_le_pow_left₀ hU0 hU 2 + have hterm2 : kappaQ * U ^ 2 ≤ + kappaQ * C_U ^ 2 * L ^ 2 := by + calc + kappaQ * U ^ 2 ≤ kappaQ * (C_U * L) ^ 2 := + mul_le_mul_of_nonneg_left hU2 hkappaQ0 + _ = kappaQ * C_U ^ 2 * L ^ 2 := by ring + calc + kappaLambda * U ^ 4 / m + kappaQ * U ^ 2 ≤ + kappaLambda * C_U ^ 4 * L ^ 2 + + kappaQ * C_U ^ 2 * L ^ 2 := add_le_add hterm1 hterm2 + _ = (kappaLambda * C_U ^ 4 + kappaQ * C_U ^ 2) * L ^ 2 := by + ring + +/-- Eventually `(log n)^8 <= n`, in the exact form used by the direct +large-residual envelope. -/ +theorem eventually_log_pow_eight_le_nat : + ∀ᶠ n : ℕ in atTop, Real.log (n : ℝ) ^ 8 ≤ (n : ℝ) := by + have hlim : Tendsto + (fun n : ℕ => Real.log (n : ℝ) ^ 8 / (n : ℝ)) atTop (nhds 0) := + Real.isLittleO_pow_log_id_atTop.tendsto_div_nhds_zero.comp + tendsto_natCast_atTop_atTop + filter_upwards [hlim.eventually (gt_mem_nhds zero_lt_one), + eventually_gt_atTop 0] with n hn hn0 + rw [div_lt_one (by positivity)] at hn + linarith + +/-- The finite direct exponent is finite whenever its constants are finite and +its residual mass is positive. -/ +theorem matchingRestrictionEnvelope_ne_top + (kappaLambda kappaQ : ENNReal) (U m : ℕ) + (hkappaLambdaTop : kappaLambda ≠ ∞) + (hkappaQTop : kappaQ ≠ ∞) + (hm : 0 < m) : + (kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) + + kappaQ * (U : ENNReal) ^ 2) ≠ ∞ := by + have hUTop : (U : ENNReal) ≠ ∞ := ENNReal.natCast_ne_top U + have hm0 : (m : ENNReal) ≠ 0 := by + exact_mod_cast hm.ne' + have hlambdaTop : + kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) ≠ ∞ := + ENNReal.div_ne_top + (ENNReal.mul_ne_top hkappaLambdaTop (ENNReal.pow_ne_top hUTop)) hm0 + have hqTop : kappaQ * (U : ENNReal) ^ 2 ≠ ∞ := + ENNReal.mul_ne_top hkappaQTop (ENNReal.pow_ne_top hUTop) + exact ENNReal.add_ne_top.mpr ⟨hlambdaTop, hqTop⟩ + +/-- The attained-profile direct matching-restriction attachment is uniformly +`exp(O((log n)^2))` in the large-residual regime. -/ +theorem eventually_profileHighSkeletonAttachment_le_matching_logScale : + ∃ C : ℝ, 0 ≤ C ∧ + ∀ᶠ n : ℕ in atTop, + ∀ {b : ℕ} {k : ColoringProfile b} + (row0 : OrderedProfilePartition n k) (U : ℕ), + U ≤ phaseNat n → + (∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) → + ∀ demand : ProfileCanonicalHighSkeleton k U, + (n : ℝ) / Real.log (n : ℝ) ^ 6 ≤ + (canonicalDemandResidualTotal (profileBlockMargin k) + (profileBlockMargin k) U demand : ℝ) → + profileHighSkeletonAttachment row0 U demand ≤ + ENNReal.ofReal + (Real.exp (C * Real.log (n : ℝ) ^ 2)) := by + obtain ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, hfinite⟩ := + exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope + let C : ℝ := kappaLambda.toReal * 4 ^ 4 + kappaQ.toReal * 4 ^ 2 + have hC : 0 ≤ C := by + dsimp [C] + positivity + refine ⟨C, hC, ?_⟩ + filter_upwards + [eventually_phaseControlled_two_pow_le_cube, + eventually_logOrder_le_phaseNat_and_phaseNat_le_four_logOrder, + eventually_log_pow_eight_le_nat, + eventually_gt_atTop (1 : ℕ)] with n hpow hphase hlog8 hn + intro b k row0 U hU hcap demand hm + let m := canonicalDemandResidualTotal (profileBlockMargin k) + (profileBlockMargin k) U demand + have hlog : 0 < Real.log (n : ℝ) := Real.log_pos (by exact_mod_cast hn) + have hmpos : 0 < m := by + have : 0 < (m : ℝ) := lt_of_lt_of_le + (div_pos (by positivity) (pow_pos hlog 6)) hm + exact_mod_cast this + have hbase := hfinite row0 U m hcap demand rfl hmpos + (hpow U m hU hmpos hm) + let exponent : ENNReal := + kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) + + kappaQ * (U : ENNReal) ^ 2 + have hexponent : exponent ≠ ∞ := by + exact matchingRestrictionEnvelope_ne_top + kappaLambda kappaQ U m hkLtop hkQtop hmpos + have hbaseReal : + profileHighSkeletonAttachment row0 U demand ≤ + ENNReal.ofReal (Real.exp exponent.toReal) := by + apply ennreal_le_of_coe_le_ereal_exp_toReal _ _ hexponent + exact EReal.coe_ennreal_le_coe_ennreal_iff.mpr hbase + apply hbaseReal.trans + apply ENNReal.ofReal_le_ofReal + apply Real.exp_le_exp.mpr + have hUreal : (U : ℝ) ≤ 4 * Real.log (n : ℝ) := + (Nat.cast_le.mpr hU).trans hphase.2 + have henv := matchingRestrictionEnvelope_bound + (n : ℝ) (Real.log (n : ℝ)) (U : ℝ) (m : ℝ) + kappaLambda.toReal kappaQ.toReal 4 + (by positivity) hlog (Nat.cast_nonneg U) (by exact_mod_cast hmpos) + ENNReal.toReal_nonneg ENNReal.toReal_nonneg (by norm_num) + hm hUreal hlog8 + have hparts := ENNReal.add_ne_top.mp hexponent + rw [ENNReal.toReal_add hparts.1 hparts.2] + simp only [exponent, ENNReal.toReal_mul, ENNReal.toReal_div, + ENNReal.toReal_pow, ENNReal.toReal_natCast] + change + kappaLambda.toReal * (U : ℝ) ^ 4 / (m : ℝ) + + kappaQ.toReal * (U : ℝ) ^ 2 ≤ + C * Real.log (n : ℝ) ^ 2 + simpa [C] using henv + +#print axioms matchingRestrictionEnvelope_bound +#print axioms eventually_log_pow_eight_le_nat +#print axioms matchingRestrictionEnvelope_ne_top +#print axioms eventually_profileHighSkeletonAttachment_le_matching_logScale + +end + +end Erdos625 From b78e0ba610e9e4a6ff7413e3178e0dd2fd10f04c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:37:27 +0300 Subject: [PATCH 18/47] Validate the direct log-square profile endpoint --- .../erdos625-matching-restriction-envelope.yml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml index 6e4752fd..6fed9bcb 100644 --- a/.github/workflows/erdos625-matching-restriction-envelope.yml +++ b/.github/workflows/erdos625-matching-restriction-envelope.yml @@ -5,6 +5,7 @@ on: paths: - "625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean" - "625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean" + - "625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean" - "625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md" - ".github/workflows/erdos625-matching-restriction-envelope.yml" workflow_dispatch: @@ -23,7 +24,8 @@ jobs: if grep -nE \ '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ 625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean \ - 625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean; then + 625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean \ + 625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -34,15 +36,15 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the profile endpoint and dependency closure warning-fatally + - name: Build the log-square endpoint and dependency closure warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section9ProfileAttachmentMatchingEnvelope --wfail \ + lake build Erdos625.Section9ProfileAttachmentMatchingLogScale --wfail \ > /tmp/section9-envelope-lean.log 2>&1 status=$? - tail -n 260 /tmp/section9-envelope-lean.log + tail -n 300 /tmp/section9-envelope-lean.log exit $status - name: Upload focused compiler log if: always() From a3aa2560e5525ce48ff694e14688979b0a6be015 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:38:13 +0300 Subject: [PATCH 19/47] Record the direct log-square specialization --- .../MATCHING_RESTRICTION_ENVELOPE_AUDIT.md | 40 ++++++++++++++----- 1 file changed, 31 insertions(+), 9 deletions(-) diff --git a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md index 8afd59ba..7c412a2b 100644 --- a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md +++ b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md @@ -5,7 +5,8 @@ This audit accompanies: - `Erdos625/Section9MatchingRestrictionEnvelope.lean`; -- `Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean`. +- `Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean`; +- `Erdos625/Section9ProfileAttachmentMatchingLogScale.lean`. The branch is stacked on PR #34 and therefore assumes the finite matching-restriction product theorem from @@ -58,6 +59,25 @@ skeleton by using its canonical reference witness, literal positive-demand matching support, residual degree caps, equal residual totals, and the exact definition of `profileHighSkeletonAttachment`. +The third module proves the exact real arithmetic + +\[ + \kappa_\Lambda\frac{U^4}{m}+\kappa_Q U^2 + \le + (\kappa_\Lambda C_U^4+\kappa_Q C_U^2)L^2 +\] + +under `m >= n/L^6`, `U <= C_U L`, and `L^8 <= n`. It then proves the eventual +phase specialization + +\[ + \operatorname{profileHighSkeletonAttachment} + \le \exp\!\bigl(C(\log n)^2\bigr) +\] + +uniformly over all attained profile high skeletons in the large-residual +regime. + The resulting profile theorem has no traversal parameter, no factor depending on the number of profile blocks, and no factor depending on the number of matching edges. @@ -73,7 +93,9 @@ matching edges. `ConfigurationThetaMoments.lean`; - `ennreal_polymer_product_le_ereal_exp_sum` for finite products; - `canonicalReference_residual_parameters` and - `profileBlockMargin_total_eq_self` for the attained-profile specialization. + `profileBlockMargin_total_eq_self` for the attained-profile specialization; +- the existing phase upper bound, residual two-power corridor, and logarithmic + little-o infrastructure for the `O((log n)^2)` adapter. ## Trust gates @@ -81,7 +103,8 @@ The focused workflow: - rejects `sorry`, `admit`, `sorryAx`, project `axiom`/`constant`, and `unsafe`; - prepares the pinned Lean 4.31/mathlib project; -- builds the profile endpoint and its dependency closure with `--wfail`; +- builds the log-square profile endpoint and its complete dependency closure + with `--wfail`; - prints the axioms of every new public theorem. The ordinary repository Lean workflow also runs because this PR changes the @@ -93,11 +116,10 @@ These modules still do not prove the complete Erdős 625 theorem. In particular they do not: - sum the Section VIII bare skeleton weights; -- specialize the exponent to the midpoint phase and prove the eventual - `O((log n)^2)` or `o(n/(log n)^4)` scale; - update the root aggregate or generated self-contained checkpoint; -- prove the chromatic lower tail, rare seed, or final event intersection. +- prove the chromatic lower tail, rare seed, or final event intersection; +- combine the large-residual log-square estimate with the small-residual branch + into one profile-level two-regime theorem on this branch. -The next integration step, after review, is a profile-level asymptotic adapter -showing that the displayed exponent is `o(amplificationBase n)` uniformly over -attained canonical demands. +The next integration step, after review, is the Section VIII skeleton sum and a +single two-regime profile theorem using this direct large-residual endpoint. From fed5811617ab39b9d25f9e18b9cc0ee623912ee0 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:39:24 +0300 Subject: [PATCH 20/47] Cancel superseded focused envelope runs --- .github/workflows/erdos625-matching-restriction-envelope.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml index 6fed9bcb..3c8b30a7 100644 --- a/.github/workflows/erdos625-matching-restriction-envelope.yml +++ b/.github/workflows/erdos625-matching-restriction-envelope.yml @@ -10,6 +10,10 @@ on: - ".github/workflows/erdos625-matching-restriction-envelope.yml" workflow_dispatch: +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + permissions: contents: read From 4a981d43a510497cb3bf1d98dce8186eb9d55d31 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:55:58 +0300 Subject: [PATCH 21/47] Silence the attained-profile cap linter --- .../Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean index d414c389..b95852c7 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean @@ -30,7 +30,7 @@ theorem exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope : 0 < kappaQ ∧ kappaQ ≠ ∞ ∧ ∀ {b n : ℕ} {k : ColoringProfile b} (row0 : OrderedProfilePartition n k) (U m : ℕ) - (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) + (_hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) (demand : ProfileCanonicalHighSkeleton k U), m = canonicalDemandResidualTotal (profileBlockMargin k) (profileBlockMargin k) U demand → @@ -43,12 +43,12 @@ theorem exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope : obtain ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, hbound⟩ := exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope refine ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, ?_⟩ - intro b n k row0 U m hcap demand hm hmpos hpow + intro b n k row0 U m _hcap demand hm hmpos hpow let witness := canonicalDemandReferenceWitness (profileBlockMargin k) (profileBlockMargin k) U demand have hparameters := canonicalReference_residual_parameters (profileBlockMargin k) (profileBlockMargin k) U - (profileBlockMargin_total_eq_self row0) hcap hcap demand + (profileBlockMargin_total_eq_self row0) _hcap _hcap demand have hrowSum : (∑ a, residualRowDegree witness a) = m := by simpa only [canonicalDemandResidualTotal, witness] using hm.symm have hcolSum : (∑ a, residualColumnDegree witness a) = m := by From 628f0c2ba92ef5bc17cd93a6ff14f830962b5f77 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 08:56:48 +0300 Subject: [PATCH 22/47] Fix the log-square imports and warning-fatal lints --- .../Erdos625/Section9ProfileAttachmentMatchingLogScale.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean index 64ffd228..97c5a1e1 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean @@ -1,6 +1,7 @@ import Erdos625.Section9ProfileAttachmentMatchingEnvelope import Erdos625.Section9PhaseTwoPowerCorridor import Erdos625.Section9ResidualRegimeScaleAdapters +import Erdos625.Section9ERealENNRealExpTransport /-! # Section IX: direct matching-restriction profile log scale @@ -36,7 +37,7 @@ theorem matchingRestrictionEnvelope_bound (hm0 : 0 < m) (hkappaLambda0 : 0 ≤ kappaLambda) (hkappaQ0 : 0 ≤ kappaQ) - (hCU0 : 0 ≤ C_U) + (_hCU0 : 0 ≤ C_U) (hm : n / L ^ 6 ≤ m) (hU : U ≤ C_U * L) (hL8 : L ^ 8 ≤ n) : @@ -180,7 +181,7 @@ theorem eventually_profileHighSkeletonAttachment_le_matching_logScale : hm hUreal hlog8 have hparts := ENNReal.add_ne_top.mp hexponent rw [ENNReal.toReal_add hparts.1 hparts.2] - simp only [exponent, ENNReal.toReal_mul, ENNReal.toReal_div, + simp only [ENNReal.toReal_mul, ENNReal.toReal_div, ENNReal.toReal_pow, ENNReal.toReal_natCast] change kappaLambda.toReal * (U : ℝ) ^ 4 / (m : ℝ) + From 1f11f8a4118737dab81cee879ef54a653604ef2c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 09:48:10 +0300 Subject: [PATCH 23/47] Add q-only matching-restriction attachment envelope --- .../Section9MatchingRestrictionQOnly.lean | 130 ++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean new file mode 100644 index 00000000..7e4e70ff --- /dev/null +++ b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean @@ -0,0 +1,130 @@ +import Erdos625.Section9MatchingRestrictionEnvelope +import Mathlib.Tactic + +/-! +# Section IX: absorb the local increment product into the residual-q mass + +The direct matching-restriction route initially keeps two products: one for the +unselected local increments `residualLambda`, and one for the selected-edge +weight `residualQ`. Since + +`residualQ = theta^2 / 2 + residualLambda` + +outside the exposed matching (and both quantities vanish on it), the lambda +mass is pointwise dominated by the q mass. Consequently both products are +controlled by the same total q sum. This removes the separate cubic +`U^4 / m` estimate from the final finite attachment envelope. +-/ + +universe u v + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- The local-increment weight is pointwise dominated by the selected-edge +weight. -/ +theorem residualLambda_le_residualQ + {A B : Type*} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (M : Finset (A × B)) (R : ℕ) (row : A → ℕ) (col : B → ℕ) + (a : A) (b : B) : + residualLambda M R row col a b ≤ residualQ M R row col a b := by + classical + unfold residualQ + by_cases hM : (a, b) ∈ M + · simp [hM] + · simp only [hM, if_false] + exact le_add_left (residualLambda M R row col a b) + (configurationCellTheta row col (Finset.univ.sum row) a b ^ 2 / 2) + +/-- If `lambda` is pointwise bounded by `q`, then the lambda product and the +direct outside-matching q product are jointly bounded by twice one total q +mass. -/ +theorem lambda_matching_products_le_exp_two_q_bound + {A B : Type*} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (lambda q : A → B → ENNReal) (M : Finset (A × B)) + (qBound : ENNReal) + (hlq : ∀ a b, lambda a b ≤ q a b) + (hqall : (∑ a, ∑ b, q a b) ≤ qBound) : + ((∏ a, ∏ b, (1 + lambda a b)) * + (∏ e ∈ (Finset.univ : Finset (A × B)) \ M, + (1 + q e.1 e.2))) ≤ + EReal.exp (((2 * qBound : ENNReal) : EReal)) := by + have hlambda : (∑ a, ∑ b, lambda a b) ≤ qBound := by + apply le_trans _ hqall + exact Finset.sum_le_sum fun a _ => + Finset.sum_le_sum fun b _ => hlq a b + have hqOutside : + (∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + q e.1 e.2) ≤ qBound := by + apply le_trans _ hqall + calc + (∑ e ∈ (Finset.univ : Finset (A × B)) \ M, + q e.1 e.2) ≤ + ∑ e ∈ (Finset.univ : Finset (A × B)), q e.1 e.2 := by + exact Finset.sum_le_sum_of_subset Finset.sdiff_subset + _ = ∑ e : A × B, q e.1 e.2 := by simp + _ = ∑ a, ∑ b, q a b := by + rw [Fintype.sum_prod_type'] + have h := lambda_matching_products_le_exp_of_sum_bounds + lambda q M qBound qBound hlambda hqOutside + simpa [two_mul] using h + +/-- One absolute finite constant bounds the literal cap/no-return attachment +numerator at scale `U^2`. No separate lambda-total or cubic degree-moment +estimate is needed. -/ +theorem exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope : + ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧ + ∀ {A : Type u} {B : Type v} [Fintype A] [Fintype B] + [DecidableEq A] [DecidableEq B] + (M : Finset (A × B)) (U m : ℕ) + (row : A → ℕ) (col : B → ℕ) + (htotal : Finset.univ.sum row = Finset.univ.sum col), + IsBipartiteMatching M → + 0 < m → + (∑ a, row a) = m → + (∑ b, col b) = m → + (∀ a, row a ≤ U) → + (∀ b, col b ≤ U) → + 2 ^ U ≤ m ^ 3 → + residualActualAttachmentNumerator M (U / 2) row col htotal ≤ + EReal.exp ((((kappa * (U : ENNReal) ^ 2 : ENNReal)) : EReal)) := by + obtain ⟨kappaQ, hkQpos, hkQtop, hkQ⟩ := + existsAbsoluteResidualQTotalBound_of_degreeCaps + let kappa : ENNReal := 2 * kappaQ + have hkappaPos : 0 < kappa := by + dsimp [kappa] + positivity + have hkappaTop : kappa ≠ ∞ := by + dsimp [kappa] + exact ENNReal.mul_ne_top ENNReal.ofNat_ne_top hkQtop + refine ⟨kappa, hkappaPos, hkappaTop, ?_⟩ + intro A B _ _ _ _ M U m row col htotal hM hm hrow hcol + hrowCap hcolCap hpow + have hbridge := + residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct + M (U / 2) row col htotal (by simpa [hrow] using hm) hM + have hqAll := + hkQ M U (U / 2) m row col hm hrow hcol hrowCap hcolCap rfl hpow + have hproduct := lambda_matching_products_le_exp_two_q_bound + (residualLambda M (U / 2) row col) + (residualQ M (U / 2) row col) M + (kappaQ * (U : ENNReal) ^ 2) + (residualLambda_le_residualQ M (U / 2) row col) + hqAll + exact hbridge.trans (by + simpa [kappa, mul_assoc] using hproduct) + +#print axioms residualLambda_le_residualQ +#print axioms lambda_matching_products_le_exp_two_q_bound +#print axioms exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope + +end + +end Erdos625 From f593ec27bc5ff5c85d1aaff9cf4a505d7387a5bd Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 09:48:28 +0300 Subject: [PATCH 24/47] Add focused q-only attachment Lean workflow --- .../erdos625-q-only-attachment-envelope.yml | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 .github/workflows/erdos625-q-only-attachment-envelope.yml diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml new file mode 100644 index 00000000..cc4d9059 --- /dev/null +++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml @@ -0,0 +1,51 @@ +name: Erdős 625 q-only attachment envelope + +on: + pull_request: + paths: + - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean" + - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md" + - ".github/workflows/erdos625-q-only-attachment-envelope.yml" + workflow_dispatch: + +permissions: + contents: read + +jobs: + focused-lean-check: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Reject placeholders and project axioms + shell: bash + run: | + if grep -nE \ + '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ + 625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean; then + exit 1 + fi + - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 + with: + lake-package-directory: 625/formalization + auto-config: false + build: false + use-mathlib-cache: true + use-github-cache: false + nanoda: false + - name: Build q-only endpoint and dependency closure warning-fatally + working-directory: 625/formalization + shell: bash + run: | + set +e + lake build Erdos625.Section9MatchingRestrictionQOnly --wfail \ + > /tmp/q-only-envelope-lean.log 2>&1 + status=$? + tail -n 260 /tmp/q-only-envelope-lean.log + exit $status + - name: Upload focused compiler log + if: always() + uses: actions/upload-artifact@v4 + with: + name: section9-q-only-envelope-lean-log + path: /tmp/q-only-envelope-lean.log + if-no-files-found: ignore From d0f95b59be822d60f4ba6130428f93d9585b74d3 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 09:48:45 +0300 Subject: [PATCH 25/47] Document q-only attachment envelope audit boundary --- .../Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md | 68 +++++++++++++++++++ 1 file changed, 68 insertions(+) create mode 100644 625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md diff --git a/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md new file mode 100644 index 00000000..3f95ac36 --- /dev/null +++ b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md @@ -0,0 +1,68 @@ +# Audit: q-only matching-restriction attachment envelope + +## Purpose + +This follow-up isolates one additional simplification of the direct Section 9 +route. The preceding branch bounds the literal residual attachment by a +product of local-increment factors and a direct outside-matching `q` product. +Here those two products are charged to the same total `q` mass. + +Outside the exposed matching, + +\[ +q_{ab}=\frac{\theta_{ab}^2}{2}+\lambda_{ab}, +\] + +and both quantities vanish on the matching. Hence +\(\lambda_{ab}\le q_{ab}\) cellwise. The accepted total bound + +\[ +\sum_{a,b}q_{ab}\le \kappa_Q U^2 +\] + +therefore controls both products, giving + +\[ +\mathcal A(M,j) + \le \exp\!\left(2\sum_{a,b}q_{ab}\right) + \le \exp(\kappa U^2). +\] + +## New declarations + +`Erdos625/Section9MatchingRestrictionQOnly.lean` proves: + +1. `residualLambda_le_residualQ`; +2. `lambda_matching_products_le_exp_two_q_bound`; +3. `exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope`. + +The last theorem is pointwise in the finite residual data and concerns the +literal cap/no-return numerator. It has no separate `U^4/m` term, no cubic +degree moment, no cycle traversal, and no dependence on the number of profile +blocks or matching edges. + +## Reused inputs + +- the exact fixed-family Fubini identity; +- the matching-restriction product theorem; +- the direct lambda/q product bridge; +- the already checked quadratic total-q estimate. + +## Trust gates + +The focused workflow rejects placeholders, project-defined axioms/constants, +and `unsafe`; it then builds the new module and its dependency closure under +the pinned Lean 4.31/mathlib project with warnings fatal. The source prints +the axioms of every new public theorem. + +## Deliberate boundary + +This PR does not by itself: + +- rewrite the canonical manuscript; +- sum the Section 8 skeleton weights; +- combine the large and small residual regimes; +- prove Proposition 9.2 or `Erdos625Statement`. + +Its role is to remove a redundant analytic branch from the large-residual +attachment estimate before manuscript integration. From 095288e9bc45c21b5360605d85944f48bef446e7 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 09:56:16 +0300 Subject: [PATCH 26/47] Fix q-only pointwise domination proof --- .../Erdos625/Section9MatchingRestrictionQOnly.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean index 7e4e70ff..f0c0b59a 100644 --- a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean +++ b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean @@ -35,12 +35,11 @@ theorem residualLambda_le_residualQ (a : A) (b : B) : residualLambda M R row col a b ≤ residualQ M R row col a b := by classical - unfold residualQ + unfold residualQ residualLambda by_cases hM : (a, b) ∈ M · simp [hM] · simp only [hM, if_false] - exact le_add_left (residualLambda M R row col a b) - (configurationCellTheta row col (Finset.univ.sum row) a b ^ 2 / 2) + exact le_add_of_nonneg_left (by positivity) /-- If `lambda` is pointwise bounded by `q`, then the lambda product and the direct outside-matching q product are jointly bounded by twice one total q From b1d370fe7e52cfe98a6929fd00a432be8ab1a679 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:04:04 +0300 Subject: [PATCH 27/47] Add natural residual power dichotomy --- .../Section9MatchingRestrictionQOnly.lean | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean index f0c0b59a..5d9c5be6 100644 --- a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean +++ b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean @@ -75,6 +75,35 @@ theorem lambda_matching_products_le_exp_two_q_bound lambda q M qBound qBound hlambda hqOutside simpa [two_mul] using h +/-- Natural ceiling of one third, written without introducing a dependency on +later Section X utilities. -/ +def residualCeilThird (U : Nat) : Nat := (U + 2) / 3 + +/-- The ceiling-third exponent covers `U`. -/ +theorem le_three_mul_residualCeilThird (U : Nat) : + U ≤ 3 * residualCeilThird U := by + unfold residualCeilThird + omega + +/-- If the quadratic large-residual hypothesis fails, the residual mass is +already below the natural power threshold `2^(ceil(U/3))`. This gives an +intrinsic alternative to splitting at `n / (log n)^6`. -/ +theorem residualMass_lt_two_pow_ceilThird_of_not_cube + (U m : Nat) (hnot : ¬ 2 ^ U ≤ m ^ 3) : + m < 2 ^ residualCeilThird U := by + by_contra h + have hm : 2 ^ residualCeilThird U ≤ m := Nat.le_of_not_gt h + have hcube : (2 ^ residualCeilThird U) ^ 3 ≤ m ^ 3 := + pow_le_pow_left' hm 3 + have hpow : 2 ^ U ≤ 2 ^ (3 * residualCeilThird U) := + pow_le_pow_right₀ (by decide) (le_three_mul_residualCeilThird U) + apply hnot + calc + 2 ^ U ≤ 2 ^ (3 * residualCeilThird U) := hpow + _ = (2 ^ residualCeilThird U) ^ 3 := by + rw [Nat.mul_comm, pow_mul] + _ ≤ m ^ 3 := hcube + /-- One absolute finite constant bounds the literal cap/no-return attachment numerator at scale `U^2`. No separate lambda-total or cubic degree-moment estimate is needed. -/ @@ -122,6 +151,8 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope : #print axioms residualLambda_le_residualQ #print axioms lambda_matching_products_le_exp_two_q_bound +#print axioms le_three_mul_residualCeilThird +#print axioms residualMass_lt_two_pow_ceilThird_of_not_cube #print axioms exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope end From fb59f846a7cf90cd8e4fcddd1623e7c0755c7789 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:05:05 +0300 Subject: [PATCH 28/47] Document the natural Section 9 power split --- .../Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md | 43 +++++++++++++++++-- 1 file changed, 40 insertions(+), 3 deletions(-) diff --git a/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md index 3f95ac36..588bac05 100644 --- a/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md +++ b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md @@ -34,13 +34,48 @@ therefore controls both products, giving 1. `residualLambda_le_residualQ`; 2. `lambda_matching_products_le_exp_two_q_bound`; -3. `exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope`. +3. `le_three_mul_residualCeilThird`; +4. `residualMass_lt_two_pow_ceilThird_of_not_cube`; +5. `exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope`. The last theorem is pointwise in the finite residual data and concerns the literal cap/no-return numerator. It has no separate `U^4/m` term, no cubic degree moment, no cycle traversal, and no dependence on the number of profile blocks or matching edges. +## A more intrinsic two-regime split + +The finite q-only theorem naturally assumes + +\[ +2^U\le m^3. +\] + +There is no need to introduce the manuscript cutoff +\(m=n/(\log n)^6\) at the finite combinatorial level. The Lean theorem +`residualMass_lt_two_pow_ceilThird_of_not_cube` proves the exact complementary +statement + +\[ +2^U\nleq m^3 +\quad\Longrightarrow\quad +m<2^{\lceil U/3\rceil}, +\qquad +\lceil U/3\rceil=\frac{U+2}{3}. +\] + +Thus Section 9 may eventually be organized around the intrinsic dichotomy: + +- **quadratic regime:** `2^U <= m^3`, use the q-only envelope + `exp(O(U^2))`; +- **small-power regime:** `2^U > m^3`, use the deterministic bound together + with `m < 2^(ceil(U/3))`. + +At the midpoint phase, `U=(2+o(1)) log_2 n`, so the second exponent is of order +at most `U 2^(ceil(U/3)) = n^(2/3+o(1))`, still +`o(n/(log n)^4)`. That asymptotic specialization is not asserted by this PR; +only the exact finite dichotomy is kernel-checked here. + ## Reused inputs - the exact fixed-family Fubini identity; @@ -61,8 +96,10 @@ This PR does not by itself: - rewrite the canonical manuscript; - sum the Section 8 skeleton weights; -- combine the large and small residual regimes; +- prove the phase-asymptotic small-power estimate; +- combine both residual regimes in the profile-level second moment; - prove Proposition 9.2 or `Erdos625Statement`. Its role is to remove a redundant analytic branch from the large-residual -attachment estimate before manuscript integration. +attachment estimate and to expose a cleaner finite regime split before +manuscript integration. From 8808f03fc67397725b189222732830a1698b999b Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:06:19 +0300 Subject: [PATCH 29/47] Specialize the q-only envelope to attained profiles --- .../Section9ProfileAttachmentQOnly.lean | 139 ++++++++++++++++++ 1 file changed, 139 insertions(+) create mode 100644 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean new file mode 100644 index 00000000..e0a1bb0b --- /dev/null +++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean @@ -0,0 +1,139 @@ +import Erdos625.Section9MatchingRestrictionQOnly +import Erdos625.Section9CanonicalDemandProductSpecialization +import Erdos625.Section8ProfileSkeletonWeight +import Erdos625.Section9ERealENNRealExpTransport +import Erdos625.PhaseEstimates +import Mathlib.Tactic + +/-! +# Section IX: attained-profile q-only attachment endpoint + +This module transports the q-only finite residual bound to every attained +canonical high skeleton and then specializes the exponent to the phase scale. +The large branch is stated using its intrinsic finite hypothesis +`2^U <= m^3`; no artificial `n / (log n)^6` cutoff is needed here. +-/ + +namespace Erdos625 + +open Filter +open scoped BigOperators ENNReal Topology + +noncomputable section + +set_option autoImplicit false + +/-- One absolute q-only constant controls every attained profile high-skeleton +attachment whenever its residual mass satisfies the finite quadratic regime. -/ +theorem exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope : + ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧ + ∀ {b n : ℕ} {k : ColoringProfile b} + (row0 : OrderedProfilePartition n k) (U m : ℕ) + (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) + (demand : ProfileCanonicalHighSkeleton k U), + m = canonicalDemandResidualTotal + (profileBlockMargin k) (profileBlockMargin k) U demand → + 0 < m → + 2 ^ U ≤ m ^ 3 → + profileHighSkeletonAttachment row0 U demand ≤ + EReal.exp ((((kappa * (U : ENNReal) ^ 2 : ENNReal)) : EReal)) := by + obtain ⟨kappa, hkpos, hktop, hbound⟩ := + exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope + refine ⟨kappa, hkpos, hktop, ?_⟩ + intro b n k row0 U m hcap demand hm hmpos hpow + let witness := canonicalDemandReferenceWitness + (profileBlockMargin k) (profileBlockMargin k) U demand + have hparameters := canonicalReference_residual_parameters + (profileBlockMargin k) (profileBlockMargin k) U + (profileBlockMargin_total_eq_self row0) hcap hcap demand + have hrowSum : (∑ a, residualRowDegree witness a) = m := by + simpa only [canonicalDemandResidualTotal, witness] using hm.symm + have hcolSum : (∑ a, residualColumnDegree witness a) = m := by + exact hparameters.2.2.2.symm.trans hrowSum + have hactual := hbound (positiveDemandSupport demand.1) U m + (residualRowDegree witness) (residualColumnDegree witness) + (sum_residualRowDegree_eq_sum_residualColumnDegree + (profileBlockMargin_total_eq_self row0) witness) + hparameters.1 hmpos hrowSum hcolSum hparameters.2.1 hparameters.2.2.1 hpow + unfold profileHighSkeletonAttachment + simpa only [witness] using hactual + +/-- The q-only exponent is finite for every finite constant and natural cap. -/ +theorem qOnlyEnvelope_ne_top + (kappa : ENNReal) (U : Nat) (hkappaTop : kappa ≠ ∞) : + kappa * (U : ENNReal) ^ 2 ≠ ∞ := + ENNReal.mul_ne_top hkappaTop + (ENNReal.pow_ne_top (ENNReal.natCast_ne_top U)) + +/-- In the intrinsic quadratic regime, every attained profile high-skeleton +attachment is uniformly `exp(O((log n)^2))`. -/ +theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale : + ∃ C : ℝ, 0 ≤ C ∧ + ∀ᶠ n : ℕ in atTop, + ∀ {b : ℕ} {k : ColoringProfile b} + (row0 : OrderedProfilePartition n k) (U : ℕ), + U ≤ phaseNat n → + (∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) → + ∀ demand : ProfileCanonicalHighSkeleton k U, + 2 ^ U ≤ + (canonicalDemandResidualTotal (profileBlockMargin k) + (profileBlockMargin k) U demand) ^ 3 → + profileHighSkeletonAttachment row0 U demand ≤ + ENNReal.ofReal + (Real.exp (C * Real.log (n : ℝ) ^ 2)) := by + obtain ⟨kappa, hkpos, hktop, hfinite⟩ := + exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope + let C : ℝ := kappa.toReal * 4 ^ 2 + have hC : 0 ≤ C := by + dsimp [C] + positivity + refine ⟨C, hC, ?_⟩ + filter_upwards + [eventually_logOrder_le_phaseNat_and_phaseNat_le_four_logOrder, + eventually_gt_atTop (1 : ℕ)] with n hphase hn + intro b k row0 U hU hcap demand hpow + let m := canonicalDemandResidualTotal (profileBlockMargin k) + (profileBlockMargin k) U demand + have hmpos : 0 < m := by + by_contra hm + have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm + subst m + simp at hpow + have hbase := hfinite row0 U m hcap demand rfl hmpos hpow + let exponent : ENNReal := kappa * (U : ENNReal) ^ 2 + have hexponent : exponent ≠ ∞ := by + exact qOnlyEnvelope_ne_top kappa U hktop + have hbaseReal : + profileHighSkeletonAttachment row0 U demand ≤ + ENNReal.ofReal (Real.exp exponent.toReal) := by + apply ennreal_le_of_coe_le_ereal_exp_toReal _ _ hexponent + exact EReal.coe_ennreal_le_coe_ennreal_iff.mpr hbase + apply hbaseReal.trans + apply ENNReal.ofReal_le_ofReal + apply Real.exp_le_exp.mpr + have hlog : 0 < Real.log (n : ℝ) := Real.log_pos (by exact_mod_cast hn) + have hUreal : (U : ℝ) ≤ 4 * Real.log (n : ℝ) := + (Nat.cast_le.mpr hU).trans hphase.2 + have hU2 : (U : ℝ) ^ 2 ≤ (4 * Real.log (n : ℝ)) ^ 2 := + pow_le_pow_left₀ (Nat.cast_nonneg U) hUreal 2 + have hbound : kappa.toReal * (U : ℝ) ^ 2 ≤ + C * Real.log (n : ℝ) ^ 2 := by + calc + kappa.toReal * (U : ℝ) ^ 2 ≤ + kappa.toReal * (4 * Real.log (n : ℝ)) ^ 2 := + mul_le_mul_of_nonneg_left hU2 ENNReal.toReal_nonneg + _ = C * Real.log (n : ℝ) ^ 2 := by + simp [C] + ring + have hexponentReal : exponent.toReal = kappa.toReal * (U : ℝ) ^ 2 := by + simp [exponent, hktop] + rw [hexponentReal] + exact hbound + +#print axioms exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope +#print axioms qOnlyEnvelope_ne_top +#print axioms eventually_profileHighSkeletonAttachment_le_qOnly_logScale + +end + +end Erdos625 From d7911a510becbae4eea72332beb39f0bcd419738 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:06:50 +0300 Subject: [PATCH 30/47] Validate the attained-profile q-only endpoint --- .../workflows/erdos625-q-only-attachment-envelope.yml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml index cc4d9059..47c39a7a 100644 --- a/.github/workflows/erdos625-q-only-attachment-envelope.yml +++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml @@ -4,6 +4,7 @@ on: pull_request: paths: - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean" + - "625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean" - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md" - ".github/workflows/erdos625-q-only-attachment-envelope.yml" workflow_dispatch: @@ -21,7 +22,8 @@ jobs: run: | if grep -nE \ '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ - 625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean; then + 625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean \ + 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -32,15 +34,15 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build q-only endpoint and dependency closure warning-fatally + - name: Build attained-profile q-only endpoint warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section9MatchingRestrictionQOnly --wfail \ + lake build Erdos625.Section9ProfileAttachmentQOnly --wfail \ > /tmp/q-only-envelope-lean.log 2>&1 status=$? - tail -n 260 /tmp/q-only-envelope-lean.log + tail -n 300 /tmp/q-only-envelope-lean.log exit $status - name: Upload focused compiler log if: always() From 892c413daf44c14e8039b4454eff2b418874440e Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:20:05 +0300 Subject: [PATCH 31/47] Fix q-only profile positivity and warning-fatal lint --- .../Erdos625/Section9ProfileAttachmentQOnly.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean index e0a1bb0b..5d2f11a9 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean @@ -29,7 +29,7 @@ theorem exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope : ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧ ∀ {b n : ℕ} {k : ColoringProfile b} (row0 : OrderedProfilePartition n k) (U m : ℕ) - (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) + (_hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) (demand : ProfileCanonicalHighSkeleton k U), m = canonicalDemandResidualTotal (profileBlockMargin k) (profileBlockMargin k) U demand → @@ -97,8 +97,8 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale : have hmpos : 0 < m := by by_contra hm have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm - subst m - simp at hpow + have htwoPos : 0 < (2 : Nat) ^ U := pow_pos (by decide) U + exact (not_le_of_gt htwoPos) (by simpa [hm0] using hpow) have hbase := hfinite row0 U m hcap demand rfl hmpos hpow let exponent : ENNReal := kappa * (U : ENNReal) ^ 2 have hexponent : exponent ≠ ∞ := by @@ -126,7 +126,7 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale : simp [C] ring have hexponentReal : exponent.toReal = kappa.toReal * (U : ℝ) ^ 2 := by - simp [exponent, hktop] + simp [exponent] rw [hexponentReal] exact hbound From 6eb80a228aeae38b021d47ac406fa9e64d6bfeae Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:32:20 +0300 Subject: [PATCH 32/47] Add the intrinsic profile residual dichotomy --- ...ction9ProfileAttachmentIntrinsicSplit.lean | 84 +++++++++++++++++++ 1 file changed, 84 insertions(+) create mode 100644 625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean new file mode 100644 index 00000000..23b6a867 --- /dev/null +++ b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean @@ -0,0 +1,84 @@ +import Erdos625.Section9ProfileAttachmentQOnly +import Erdos625.Section9SmallResidualAttachmentBound +import Erdos625.Section8ProfileSkeletonWeight +import Mathlib.Tactic + +/-! +# Section IX: intrinsic finite residual dichotomy + +The q-only estimate requires exactly `2^U <= m^3`. Rather than introduce an +external cutoff in `m`, this module splits on that finite proposition itself. +Its negation forces `m < 2^(ceil(U/3))`, where the deterministic residual bound +applies directly. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- One absolute q-only constant gives an exact finite dichotomy for every +attained profile high skeleton. + +In the quadratic branch the attachment is bounded by `exp(kappa * U^2)`. In +the complementary branch the residual mass is below `2^(ceil(U/3))` and the +literal deterministic bound `2^(U*m/2)` is retained. -/ +theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split : + ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧ + ∀ {b n : ℕ} {k : ColoringProfile b} + (row0 : OrderedProfilePartition n k) (U : ℕ) + (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) + (demand : ProfileCanonicalHighSkeleton k U), + let m := canonicalDemandResidualTotal + (profileBlockMargin k) (profileBlockMargin k) U demand + (2 ^ U ≤ m ^ 3 ∧ + profileHighSkeletonAttachment row0 U demand ≤ + EReal.exp ((((kappa * (U : ENNReal) ^ 2 : ENNReal)) : EReal))) ∨ + (¬ 2 ^ U ≤ m ^ 3 ∧ + m < 2 ^ residualCeilThird U ∧ + profileHighSkeletonAttachment row0 U demand ≤ + (2 : ENNReal) ^ (U * m / 2)) := by + obtain ⟨kappa, hkpos, hktop, hlarge⟩ := + exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope + refine ⟨kappa, hkpos, hktop, ?_⟩ + intro b n k row0 U hcap demand + let m := canonicalDemandResidualTotal + (profileBlockMargin k) (profileBlockMargin k) U demand + by_cases hpow : 2 ^ U ≤ m ^ 3 + · left + have hmpos : 0 < m := by + by_contra hm + have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm + have htwoPos : 0 < (2 : Nat) ^ U := pow_pos (by decide) U + exact (not_le_of_gt htwoPos) (by simpa [hm0] using hpow) + exact ⟨hpow, hlarge row0 U m hcap demand rfl hmpos hpow⟩ + · right + have hmass := residualMass_lt_two_pow_ceilThird_of_not_cube U m hpow + let witness := canonicalDemandReferenceWitness + (profileBlockMargin k) (profileBlockMargin k) U demand + have hmatching : + IsBipartiteMatching (positiveDemandSupport demand.1) := + profileHighSkeleton_positiveSupport_isBipartiteMatching k U hcap demand + have htotal : + (∑ a, residualRowDegree witness a) = + ∑ a, residualColumnDegree witness a := + sum_residualRowDegree_eq_sum_residualColumnDegree + (profileBlockMargin_total_eq_self row0) witness + have hrowSum : (∑ a, residualRowDegree witness a) = m := by + simp only [m, canonicalDemandResidualTotal, witness] + have hsmall := residualActualAttachmentNumerator_le_two_pow_of_small_mass + (positiveDemandSupport demand.1) (U / 2) U m + (residualRowDegree witness) (residualColumnDegree witness) + htotal hmatching rfl hrowSum + refine ⟨hpow, hmass, ?_⟩ + unfold profileHighSkeletonAttachment + simpa only [m, witness] using hsmall + +#print axioms exists_absolute_profileHighSkeletonAttachment_intrinsic_split + +end + +end Erdos625 From 55b9eb080d4cd8c57e9efb3ace52dba8c3dcf6d4 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:32:50 +0300 Subject: [PATCH 33/47] Validate the intrinsic profile residual split --- .../workflows/erdos625-q-only-attachment-envelope.yml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml index 47c39a7a..46b6f359 100644 --- a/.github/workflows/erdos625-q-only-attachment-envelope.yml +++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml @@ -5,6 +5,7 @@ on: paths: - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean" - "625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean" + - "625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean" - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md" - ".github/workflows/erdos625-q-only-attachment-envelope.yml" workflow_dispatch: @@ -23,7 +24,8 @@ jobs: if grep -nE \ '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ 625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean \ - 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean; then + 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean \ + 625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -34,15 +36,15 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build attained-profile q-only endpoint warning-fatally + - name: Build intrinsic profile split warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section9ProfileAttachmentQOnly --wfail \ + lake build Erdos625.Section9ProfileAttachmentIntrinsicSplit --wfail \ > /tmp/q-only-envelope-lean.log 2>&1 status=$? - tail -n 300 /tmp/q-only-envelope-lean.log + tail -n 320 /tmp/q-only-envelope-lean.log exit $status - name: Upload focused compiler log if: always() From 997d61099d3c21664f07557cf832bfe58c44d08d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:35:57 +0300 Subject: [PATCH 34/47] Expose the residual-mass abbreviation in the positivity proof --- 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean index 5d2f11a9..03926b9e 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean @@ -94,6 +94,7 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale : intro b k row0 U hU hcap demand hpow let m := canonicalDemandResidualTotal (profileBlockMargin k) (profileBlockMargin k) U demand + change 2 ^ U ≤ m ^ 3 at hpow have hmpos : 0 < m := by by_contra hm have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm From ada3ea50c09e7b07cbdf511ff6e48eed34d577a0 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:38:12 +0300 Subject: [PATCH 35/47] Normalize the intrinsic-split target before case analysis --- .../Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean index 23b6a867..4de3fe50 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean @@ -45,6 +45,7 @@ theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split : exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope refine ⟨kappa, hkpos, hktop, ?_⟩ intro b n k row0 U hcap demand + dsimp only let m := canonicalDemandResidualTotal (profileBlockMargin k) (profileBlockMargin k) U demand by_cases hpow : 2 ^ U ≤ m ^ 3 From 146a7bfc80eda23e34f035033f9550b0f6f0424e Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 10:44:28 +0300 Subject: [PATCH 36/47] Cancel obsolete q-only validation runs --- .github/workflows/erdos625-q-only-attachment-envelope.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml index 46b6f359..68a49e1b 100644 --- a/.github/workflows/erdos625-q-only-attachment-envelope.yml +++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml @@ -10,6 +10,10 @@ on: - ".github/workflows/erdos625-q-only-attachment-envelope.yml" workflow_dispatch: +concurrency: + group: erdos625-q-only-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + permissions: contents: read From f48c6613a449344c5519079ca6198601b4ec4aa6 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 13:16:32 +0300 Subject: [PATCH 37/47] Fix warning-fatal q-only profile proof --- .../Erdos625/Section9ProfileAttachmentQOnly.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean index 03926b9e..47aadbe5 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean @@ -98,8 +98,8 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale : have hmpos : 0 < m := by by_contra hm have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm - have htwoPos : 0 < (2 : Nat) ^ U := pow_pos (by decide) U - exact (not_le_of_gt htwoPos) (by simpa [hm0] using hpow) + subst m + simp at hpow have hbase := hfinite row0 U m hcap demand rfl hmpos hpow let exponent : ENNReal := kappa * (U : ENNReal) ^ 2 have hexponent : exponent ≠ ∞ := by From 8c47f865e4441841e776d4d16760509a56c985bf Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 13:17:04 +0300 Subject: [PATCH 38/47] Fix warning-fatal intrinsic split proof --- .../Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean index 4de3fe50..81820bde 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean @@ -30,7 +30,7 @@ theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split : ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧ ∀ {b n : ℕ} {k : ColoringProfile b} (row0 : OrderedProfilePartition n k) (U : ℕ) - (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) + (_hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) (demand : ProfileCanonicalHighSkeleton k U), let m := canonicalDemandResidualTotal (profileBlockMargin k) (profileBlockMargin k) U demand @@ -53,8 +53,8 @@ theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split : have hmpos : 0 < m := by by_contra hm have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm - have htwoPos : 0 < (2 : Nat) ^ U := pow_pos (by decide) U - exact (not_le_of_gt htwoPos) (by simpa [hm0] using hpow) + subst m + simp at hpow exact ⟨hpow, hlarge row0 U m hcap demand rfl hmpos hpow⟩ · right have hmass := residualMass_lt_two_pow_ceilThird_of_not_cube U m hpow From 2971838d9e91859ef481239049fad4129f5f43c7 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 13:23:11 +0300 Subject: [PATCH 39/47] Assemble the q-only and small residual attachment regimes --- .../Section9QOnlyTwoRegimeAssembly.lean | 229 ++++++++++++++++++ 1 file changed, 229 insertions(+) create mode 100644 625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean new file mode 100644 index 00000000..5563b3f8 --- /dev/null +++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean @@ -0,0 +1,229 @@ +import Erdos625.Section9ProfileAttachmentQOnly +import Erdos625.Section9ProfileAttachmentSmallResidualLogScale +import Erdos625.Section9PhaseTwoPowerCorridor +import Erdos625.Section9ActualAttachmentAggregation +import Erdos625.Section10AmplificationScales +import Mathlib.Tactic + +/-! +# Section IX: q-only two-regime attachment assembly + +The direct matching-restriction route gives an `exp(O((log n)^2))` attachment +bound whenever its intrinsic finite hypothesis `2^U <= m^3` holds. The +existing phase corridor shows that this hypothesis holds throughout the old +large-residual range. Its complement is therefore covered by the literal +small-residual estimate. + +This file combines those two profile-level estimates with the exact bare-times- +attachment aggregation. It does not estimate the Section VIII bare skeleton +sum or prove the final random-graph statement. +-/ + +namespace Erdos625 + +open Filter +open scoped ENNReal Topology + +noncomputable section + +set_option autoImplicit false + +/-- A `log^2` large branch and an `n/log^5` small branch admit one deterministic +error sequence at the amplification scale `n/log^4`. The two branches may have +different nonnegative constants. -/ +theorem exists_uniform_qOnly_twoRegime_error + (S : ℕ → Type*) + (attachment : ∀ n, S n → ℝ) + (m₀ : ∀ n, S n → ℕ) + (Cq Cs : ℝ) (hCq : 0 ≤ Cq) (hCs : 0 ≤ Cs) + (hlarge : ∀ᶠ n : ℕ in atTop, + ∀ s : S n, + (n : ℝ) / Real.log (n : ℝ) ^ 6 ≤ (m₀ n s : ℝ) → + attachment n s ≤ Real.exp (Cq * Real.log (n : ℝ) ^ 2)) + (hsmall : ∀ᶠ n : ℕ in atTop, + ∀ s : S n, + (m₀ n s : ℝ) < (n : ℝ) / Real.log (n : ℝ) ^ 6 → + attachment n s ≤ + Real.exp (Cs * (n : ℝ) / Real.log (n : ℝ) ^ 5)) : + ∃ εAtt : ℕ → ℝ, + Tendsto εAtt atTop (nhds 0) ∧ + ∀ᶠ n : ℕ in atTop, + 0 ≤ εAtt n ∧ + ∀ s : S n, + attachment n s ≤ + Real.exp + (εAtt n * (n : ℝ) / Real.log (n : ℝ) ^ 4) := by + refine ⟨fun n => + Cq * (Real.log (n : ℝ) ^ 6 / (n : ℝ)) + + Cs / Real.log (n : ℝ), ?_, ?_⟩ + · have h_log_div_n : + Tendsto + (fun n : ℕ => Real.log (n : ℝ) ^ 6 / (n : ℝ)) + atTop (nhds 0) := by + suffices h_log : + Tendsto (fun y : ℝ => y ^ 6 / Real.exp y) atTop (nhds 0) by + have hcomp := h_log.comp + (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) + exact hcomp.congr' (by + filter_upwards [Filter.eventually_gt_atTop 0] with n hn + simp +decide [Real.exp_log (Nat.cast_pos.mpr hn)]) + simpa only [Real.exp_neg, div_eq_mul_inv] using + Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero 6 + have h_inv_log : + Tendsto (fun n : ℕ => 1 / Real.log (n : ℝ)) atTop (nhds 0) := + tendsto_inv_atTop_zero.comp + (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) + simpa only [div_eq_mul_inv] using + (tendsto_const_nhds.mul h_log_div_n).add + (tendsto_const_nhds.mul h_inv_log) + · obtain ⟨a₁, ha₁⟩ := hlarge + obtain ⟨a₂, ha₂⟩ := hsmall + use Nat.max (Nat.max a₁ a₂) 3 + intro n hn + have ha₁n : a₁ ≤ n := by omega + have ha₂n : a₂ ≤ n := by omega + have hn3 : 3 ≤ n := by omega + have hnpos : 0 < (n : ℝ) := by positivity + have hlog : 0 < Real.log (n : ℝ) := + Real.log_pos (by exact_mod_cast (lt_of_lt_of_le (by norm_num : 1 < 3) hn3)) + have hscale : + (Cq * (Real.log (n : ℝ) ^ 6 / (n : ℝ)) + + Cs / Real.log (n : ℝ)) * + (n : ℝ) / Real.log (n : ℝ) ^ 4 = + Cq * Real.log (n : ℝ) ^ 2 + + Cs * (n : ℝ) / Real.log (n : ℝ) ^ 5 := by + field_simp [ne_of_gt hnpos, ne_of_gt hlog] + ring + refine ⟨?_, ?_⟩ + · exact add_nonneg + (mul_nonneg hCq + (div_nonneg (pow_nonneg (Real.log_natCast_nonneg _) _) + (Nat.cast_nonneg _))) + (div_nonneg hCs (Real.log_natCast_nonneg _)) + · intro s + by_cases hmass : + (m₀ n s : ℝ) < (n : ℝ) / Real.log (n : ℝ) ^ 6 + · refine (ha₂ n ha₂n s hmass).trans (Real.exp_le_exp.mpr ?_) + rw [hscale] + exact le_add_of_nonneg_left + (mul_nonneg hCq (sq_nonneg (Real.log (n : ℝ)))) + · refine (ha₁ n ha₁n s (le_of_not_gt hmass)).trans + (Real.exp_le_exp.mpr ?_) + rw [hscale] + exact le_add_of_nonneg_right + (div_nonneg + (mul_nonneg hCs (Nat.cast_nonneg n)) + (pow_nonneg hlog.le 5)) + +/-- The q-only large branch and the literal small branch combine into the exact +midpoint canonical attachment sum with a vanishing amplification-scale error. -/ +theorem exists_midpointCanonicalAttachment_qOnly_twoRegime_error + (b U : Nat → Nat) + (k : (n : Nat) → ColoringProfile (b n)) + (row0 : (n : Nat) → OrderedProfilePartition n (k n)) + (hU : ∀ᶠ n : Nat in atTop, U n ≤ phaseNat n) + (hcap : ∀ᶠ n : Nat in atTop, + ∀ a : ProfileBlockIndex (k n), profileBlockMargin (k n) a ≤ U n) : + ∃ epsilon : Nat → Real, + Tendsto epsilon atTop (nhds 0) ∧ + (∀ᶠ n in atTop, 0 ≤ epsilon n) ∧ + ∀ᶠ n in atTop, + midpointCanonicalAttachmentSum (row0 n) (U n) ≤ + canonicalBareSkeletonSum (k n) (U n) * + ENNReal.ofReal + (Real.exp (epsilon n * amplificationBase n)) := by + obtain ⟨Cq, hCq, hq⟩ := + eventually_profileHighSkeletonAttachment_le_qOnly_logScale + obtain ⟨Cs, hCs, hs⟩ := + eventually_profileHighSkeletonAttachment_le_smallResidual_logScale + have hlarge : ∀ᶠ n : Nat in atTop, + ∀ demand : ProfileCanonicalHighSkeleton (k n) (U n), + (n : Real) / Real.log (n : Real) ^ 6 ≤ + (canonicalDemandResidualTotal + (profileBlockMargin (k n)) (profileBlockMargin (k n)) + (U n) demand : Real) → + (profileHighSkeletonAttachment (row0 n) (U n) demand).toReal ≤ + Real.exp (Cq * Real.log (n : Real) ^ 2) := by + filter_upwards + [hq, hU, hcap, eventually_phaseControlled_two_pow_le_cube, + eventually_gt_atTop (1 : Nat)] with n hqn hUn hcapn hcorr hn + intro demand hmass + let m := canonicalDemandResidualTotal + (profileBlockMargin (k n)) (profileBlockMargin (k n)) (U n) demand + have hlog : 0 < Real.log (n : Real) := + Real.log_pos (by exact_mod_cast hn) + have hmpos : 0 < m := by + have hmreal : 0 < (m : Real) := + lt_of_lt_of_le + (div_pos (by positivity) (pow_pos hlog 6)) hmass + exact_mod_cast hmreal + have hpow : 2 ^ U n ≤ m ^ 3 := hcorr (U n) m hUn hmpos hmass + have hbound := hqn (row0 n) (U n) hUn hcapn demand hpow + exact (ENNReal.toReal_mono ENNReal.ofReal_ne_top hbound).trans_eq (by + rw [ENNReal.toReal_ofReal (Real.exp_nonneg _)]) + have hsmall : ∀ᶠ n : Nat in atTop, + ∀ demand : ProfileCanonicalHighSkeleton (k n) (U n), + (canonicalDemandResidualTotal + (profileBlockMargin (k n)) (profileBlockMargin (k n)) + (U n) demand : Real) < + (n : Real) / Real.log (n : Real) ^ 6 → + (profileHighSkeletonAttachment (row0 n) (U n) demand).toReal ≤ + Real.exp (Cs * (n : Real) / Real.log (n : Real) ^ 5) := by + filter_upwards [hs, hU, hcap] with n hsn hUn hcapn + intro demand hmass + have hbound := hsn (row0 n) (U n) hUn hcapn demand hmass + exact (ENNReal.toReal_mono ENNReal.ofReal_ne_top hbound).trans_eq (by + rw [ENNReal.toReal_ofReal (Real.exp_nonneg _)]) + obtain ⟨epsilon, hepsilon, hevent⟩ := + exists_uniform_qOnly_twoRegime_error + (fun n => ProfileCanonicalHighSkeleton (k n) (U n)) + (fun n demand => + (profileHighSkeletonAttachment (row0 n) (U n) demand).toReal) + (fun n demand => + canonicalDemandResidualTotal + (profileBlockMargin (k n)) (profileBlockMargin (k n)) + (U n) demand) + Cq Cs hCq hCs hlarge hsmall + refine ⟨epsilon, hepsilon, hevent.mono fun _ hn => hn.1, ?_⟩ + filter_upwards + [hevent, hq, hs, hU, hcap, eventually_phaseControlled_two_pow_le_cube, + eventually_gt_atTop (1 : Nat)] with n hn hqn hsn hUn hcapn hcorr hnlarge + apply midpointCanonicalAttachmentSum_le_bare_mul + intro demand + have hfinite : + profileHighSkeletonAttachment (row0 n) (U n) demand ≠ ⊤ := by + by_cases hmass : + (canonicalDemandResidualTotal + (profileBlockMargin (k n)) (profileBlockMargin (k n)) + (U n) demand : Real) < + (n : Real) / Real.log (n : Real) ^ 6 + · have hbound := hsn (row0 n) (U n) hUn hcapn demand hmass + intro htop + rw [htop] at hbound + exact ENNReal.ofReal_ne_top (top_le_iff.mp hbound) + · let m := canonicalDemandResidualTotal + (profileBlockMargin (k n)) (profileBlockMargin (k n)) (U n) demand + have hlog : 0 < Real.log (n : Real) := + Real.log_pos (by exact_mod_cast hnlarge) + have hmpos : 0 < m := by + have hmreal : 0 < (m : Real) := + lt_of_lt_of_le + (div_pos (by positivity) (pow_pos hlog 6)) + (le_of_not_gt hmass) + exact_mod_cast hmreal + have hpow : 2 ^ U n ≤ m ^ 3 := + hcorr (U n) m hUn hmpos (le_of_not_gt hmass) + have hbound := hqn (row0 n) (U n) hUn hcapn demand hpow + intro htop + rw [htop] at hbound + exact ENNReal.ofReal_ne_top (top_le_iff.mp hbound) + rw [← ENNReal.ofReal_toReal hfinite] + apply ENNReal.ofReal_le_ofReal + simpa only [amplificationBase, mul_div_assoc] using hn.2 demand + +#print axioms exists_uniform_qOnly_twoRegime_error +#print axioms exists_midpointCanonicalAttachment_qOnly_twoRegime_error + +end + +end Erdos625 From 8333bc77433d3fbfdaaeb5fa4a7991c34da54657 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 13:23:57 +0300 Subject: [PATCH 40/47] Validate the q-only two-regime assembly --- .../workflows/erdos625-q-only-attachment-envelope.yml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml index 68a49e1b..967a991a 100644 --- a/.github/workflows/erdos625-q-only-attachment-envelope.yml +++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml @@ -6,6 +6,7 @@ on: - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean" - "625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean" - "625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean" + - "625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean" - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md" - ".github/workflows/erdos625-q-only-attachment-envelope.yml" workflow_dispatch: @@ -29,7 +30,8 @@ jobs: '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ 625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean \ 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean \ - 625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean; then + 625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean \ + 625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -40,15 +42,15 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build intrinsic profile split warning-fatally + - name: Build q-only two-regime assembly warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section9ProfileAttachmentIntrinsicSplit --wfail \ + lake build Erdos625.Section9QOnlyTwoRegimeAssembly --wfail \ > /tmp/q-only-envelope-lean.log 2>&1 status=$? - tail -n 320 /tmp/q-only-envelope-lean.log + tail -n 380 /tmp/q-only-envelope-lean.log exit $status - name: Upload focused compiler log if: always() From 2dd427978fd4199733b665e24c11a17da0237b2e Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 13:34:45 +0300 Subject: [PATCH 41/47] Avoid placeholder-word false positive in assembly documentation --- 625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean index 5563b3f8..f566d705 100644 --- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean +++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean @@ -28,7 +28,7 @@ noncomputable section set_option autoImplicit false -/-- A `log^2` large branch and an `n/log^5` small branch admit one deterministic +/-- A `log^2` large branch and an `n/log^5` small branch yield one deterministic error sequence at the amplification scale `n/log^4`. The two branches may have different nonnegative constants. -/ theorem exists_uniform_qOnly_twoRegime_error From 33866e2330689468acf71557ceabc0dc0c21c87a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 13:46:28 +0300 Subject: [PATCH 42/47] Use an explicit positivity contradiction in the q-only profile adapter --- .../Erdos625/Section9ProfileAttachmentQOnly.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean index 47aadbe5..f3fc1b71 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean @@ -98,8 +98,9 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale : have hmpos : 0 < m := by by_contra hm have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm - subst m - simp at hpow + have hm3 : m ^ 3 = 0 := by rw [hm0]; norm_num + rw [hm3] at hpow + exact (Nat.not_lt_of_ge hpow) (pow_pos (by decide) U) have hbase := hfinite row0 U m hcap demand rfl hmpos hpow let exponent : ENNReal := kappa * (U : ENNReal) ^ 2 have hexponent : exponent ≠ ∞ := by From 96f8e82ffbf3851002a7995f42872014d89425a2 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 13:47:10 +0300 Subject: [PATCH 43/47] Use an explicit positivity contradiction in the intrinsic split --- .../Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean index 81820bde..aff375fc 100644 --- a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean +++ b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean @@ -53,8 +53,9 @@ theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split : have hmpos : 0 < m := by by_contra hm have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm - subst m - simp at hpow + have hm3 : m ^ 3 = 0 := by rw [hm0]; norm_num + rw [hm3] at hpow + exact (Nat.not_lt_of_ge hpow) (pow_pos (by decide) U) exact ⟨hpow, hlarge row0 U m hcap demand rfl hmpos hpow⟩ · right have hmass := residualMass_lt_two_pow_ceilThird_of_not_cube U m hpow From 7836b7d446ec29e95eaf3cdd6b52e87d583a5b97 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 13:58:06 +0300 Subject: [PATCH 44/47] Repair the q-only two-regime filter and normalization bridges --- .../Section9QOnlyTwoRegimeAssembly.lean | 29 ++++++++++--------- 1 file changed, 16 insertions(+), 13 deletions(-) diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean index f566d705..ea8b191a 100644 --- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean +++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean @@ -9,13 +9,13 @@ import Mathlib.Tactic # Section IX: q-only two-regime attachment assembly The direct matching-restriction route gives an `exp(O((log n)^2))` attachment -bound whenever its intrinsic finite hypothesis `2^U <= m^3` holds. The +bound whenever its intrinsic finite hypothesis `2^U <= m^3` holds. The existing phase corridor shows that this hypothesis holds throughout the old -large-residual range. Its complement is therefore covered by the literal +large-residual range. Its complement is therefore covered by the literal small-residual estimate. This file combines those two profile-level estimates with the exact bare-times- -attachment aggregation. It does not estimate the Section VIII bare skeleton +attachment aggregation. It does not estimate the Section VIII bare skeleton sum or prove the final random-graph statement. -/ @@ -29,7 +29,7 @@ noncomputable section set_option autoImplicit false /-- A `log^2` large branch and an `n/log^5` small branch yield one deterministic -error sequence at the amplification scale `n/log^4`. The two branches may have +error sequence at the amplification scale `n/log^4`. The two branches may have different nonnegative constants. -/ theorem exists_uniform_qOnly_twoRegime_error (S : ℕ → Type*) @@ -69,15 +69,16 @@ theorem exists_uniform_qOnly_twoRegime_error simp +decide [Real.exp_log (Nat.cast_pos.mpr hn)]) simpa only [Real.exp_neg, div_eq_mul_inv] using Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero 6 + have h_inv_log_raw := tendsto_inv_atTop_zero.comp + (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) have h_inv_log : - Tendsto (fun n : ℕ => 1 / Real.log (n : ℝ)) atTop (nhds 0) := - tendsto_inv_atTop_zero.comp - (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) - simpa only [div_eq_mul_inv] using - (tendsto_const_nhds.mul h_log_div_n).add - (tendsto_const_nhds.mul h_inv_log) - · obtain ⟨a₁, ha₁⟩ := hlarge - obtain ⟨a₂, ha₂⟩ := hsmall + Tendsto (fun n : ℕ => 1 / Real.log (n : ℝ)) atTop (nhds 0) := by + simpa only [Function.comp_apply, one_div] using h_inv_log_raw + have hq := h_log_div_n.const_mul Cq + have hs := h_inv_log.const_mul Cs + simpa only [div_eq_mul_inv, one_div, mul_zero, add_zero] using hq.add hs + · rcases (eventually_atTop.1 hlarge) with ⟨a₁, ha₁⟩ + rcases (eventually_atTop.1 hsmall) with ⟨a₂, ha₂⟩ use Nat.max (Nat.max a₁ a₂) 3 intro n hn have ha₁n : a₁ ≤ n := by omega @@ -173,7 +174,9 @@ theorem exists_midpointCanonicalAttachment_qOnly_twoRegime_error intro demand hmass have hbound := hsn (row0 n) (U n) hUn hcapn demand hmass exact (ENNReal.toReal_mono ENNReal.ofReal_ne_top hbound).trans_eq (by - rw [ENNReal.toReal_ofReal (Real.exp_nonneg _)]) + rw [ENNReal.toReal_ofReal (Real.exp_nonneg _)] + congr 1 + ring) obtain ⟨epsilon, hepsilon, hevent⟩ := exists_uniform_qOnly_twoRegime_error (fun n => ProfileCanonicalHighSkeleton (k n) (U n)) From c7d21751f66727a9a0c6101e927278f5234a8b57 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 14:09:24 +0300 Subject: [PATCH 45/47] Construct the q-only two-regime eventual bound explicitly --- .../Erdos625/Section9QOnlyTwoRegimeAssembly.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean index ea8b191a..01dbedd0 100644 --- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean +++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean @@ -73,13 +73,15 @@ theorem exists_uniform_qOnly_twoRegime_error (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) have h_inv_log : Tendsto (fun n : ℕ => 1 / Real.log (n : ℝ)) atTop (nhds 0) := by - simpa only [Function.comp_apply, one_div] using h_inv_log_raw + simpa only [Function.comp_def, one_div] using h_inv_log_raw have hq := h_log_div_n.const_mul Cq have hs := h_inv_log.const_mul Cs - simpa only [div_eq_mul_inv, one_div, mul_zero, add_zero] using hq.add hs + simpa only [div_eq_mul_inv, one_div, one_mul, mul_zero, add_zero] using + hq.add hs · rcases (eventually_atTop.1 hlarge) with ⟨a₁, ha₁⟩ rcases (eventually_atTop.1 hsmall) with ⟨a₂, ha₂⟩ - use Nat.max (Nat.max a₁ a₂) 3 + apply eventually_atTop.2 + refine ⟨Nat.max (Nat.max a₁ a₂) 3, ?_⟩ intro n hn have ha₁n : a₁ ≤ n := by omega have ha₂n : a₂ ≤ n := by omega From d33b06d47aaba00914046fdbca4bdf625fa1bdce Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 20:44:36 +0300 Subject: [PATCH 46/47] Repair q-only two-regime focused Lean target --- .../Erdos625/Section9QOnlyTwoRegimeAssembly.lean | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean index 01dbedd0..9303ae20 100644 --- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean +++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean @@ -83,9 +83,14 @@ theorem exists_uniform_qOnly_twoRegime_error apply eventually_atTop.2 refine ⟨Nat.max (Nat.max a₁ a₂) 3, ?_⟩ intro n hn - have ha₁n : a₁ ≤ n := by omega - have ha₂n : a₂ ≤ n := by omega - have hn3 : 3 ≤ n := by omega + have ha₁n : a₁ ≤ n := + (Nat.le_max_left a₁ a₂).trans + ((Nat.le_max_left (Nat.max a₁ a₂) 3).trans hn) + have ha₂n : a₂ ≤ n := + (Nat.le_max_right a₁ a₂).trans + ((Nat.le_max_left (Nat.max a₁ a₂) 3).trans hn) + have hn3 : 3 ≤ n := + (Nat.le_max_right (Nat.max a₁ a₂) 3).trans hn have hnpos : 0 < (n : ℝ) := by positivity have hlog : 0 < Real.log (n : ℝ) := Real.log_pos (by exact_mod_cast (lt_of_lt_of_le (by norm_num : 1 < 3) hn3)) @@ -96,7 +101,6 @@ theorem exists_uniform_qOnly_twoRegime_error Cq * Real.log (n : ℝ) ^ 2 + Cs * (n : ℝ) / Real.log (n : ℝ) ^ 5 := by field_simp [ne_of_gt hnpos, ne_of_gt hlog] - ring refine ⟨?_, ?_⟩ · exact add_nonneg (mul_nonneg hCq @@ -223,7 +227,7 @@ theorem exists_midpointCanonicalAttachment_qOnly_twoRegime_error rw [htop] at hbound exact ENNReal.ofReal_ne_top (top_le_iff.mp hbound) rw [← ENNReal.ofReal_toReal hfinite] - apply ENNReal.ofReal_le_ofReal + apply ENNREAL.ofReal_le_ofReal simpa only [amplificationBase, mul_div_assoc] using hn.2 demand #print axioms exists_uniform_qOnly_twoRegime_error From 2ea82c988218dee89d3639f598090ce813501c40 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Sat, 25 Jul 2026 20:47:01 +0300 Subject: [PATCH 47/47] Correct ENNReal namespace in q-only assembly --- 625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean index 9303ae20..aab1ce4f 100644 --- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean +++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean @@ -227,7 +227,7 @@ theorem exists_midpointCanonicalAttachment_qOnly_twoRegime_error rw [htop] at hbound exact ENNReal.ofReal_ne_top (top_le_iff.mp hbound) rw [← ENNReal.ofReal_toReal hfinite] - apply ENNREAL.ofReal_le_ofReal + apply ENNReal.ofReal_le_ofReal simpa only [amplificationBase, mul_div_assoc] using hn.2 demand #print axioms exists_uniform_qOnly_twoRegime_error