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 1/4] 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 2/4] 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 3/4] 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 4/4] 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