From 21168cd9144a8ce457da7626cd9916d2b28c2906 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:19:39 +0300 Subject: [PATCH 01/59] Add direct half-deficit support-choice assembly --- .../Section8DirectHalfDeficitAssembly.lean | 339 ++++++++++++++++++ 1 file changed, 339 insertions(+) create mode 100644 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean diff --git a/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean new file mode 100644 index 00000000..c03b1fff --- /dev/null +++ b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean @@ -0,0 +1,339 @@ +import Erdos625.Section8AttainedAllDeficitReindexing +import Erdos625.Section8SharpDeficitProduct +import Erdos625.Section8EndpointAllHighDecoration +import Mathlib.Tactic + +/-! +# Section VIII: direct support/choice assembly over the half-deficit envelope + +The exact attained-demand encoding currently uses a dependent subtype carrying +one deficit in every selected endpoint cell. The analytic product theorem uses +`NearSkeletonChoice`, where zero deficit is represented by `none` and every +positive deficit is represented by `some h`. + +This module removes the later conversion burden. It enlarges the admissible +window to the simpler condition `2 h < m`, which every attained high cell +already satisfies, and maps attained demands directly into the same optional +choice type used by the product expansion. Since all weights are nonnegative, +the enlargement is harmless for an upper bound. + +The final theorem is a generic finite assembly principle: once one has a +pointwise comparison of an attained demand with a reference support weight times +its optional-deficit charge, the entire attained sum is bounded by one sum over +block supports of reference weight times a product of local partition +functions. + +No pointwise weight comparison, endpoint transportation estimate, or phase +asymptotic is asserted here. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- Every four-endpoint overlap size is at most `alpha`. This lets us use the +single ambient deficit type `Fin (alpha+1)` for all selected cells. -/ +theorem fourEndpointOverlapSize_le_alpha + (alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) : + fourEndpointOverlapSize alpha hAlpha i j ≤ alpha := by + fin_cases i <;> fin_cases j <;> + simp [fourEndpointOverlapSize, fourEndpointSize, + fourEndpointCoordinate, fourDeficitCoordinate, fourDeficit] <;> omega + +/-- Positive deficits in the enlarged half-deficit envelope. The original +strict global cutoff is not needed for the upper bound once `2 h < m` is known. -/ +def fourEndpointHalfDeficitAllowed + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) + (cell : ↥P.edges) : Finset (FourEndpointDeficit alpha) := + let m := fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1 + Finset.univ.filter fun deficit => 0 < deficit.1 ∧ 2 * deficit.1 < m + +/-- The already charged local ratio used for one positive deficit. -/ +def fourEndpointHalfDeficitWeight + (n alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) + (cell : ↥P.edges) (deficit : FourEndpointDeficit alpha) : ENNReal := + nearCellTerm n + (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1) + (Nat.dist cell.1.1.1.val cell.1.2.1.val) deficit.1 + +/-- One abstract block matching together with the optional positive deficit in +every selected cell. This is the same data structure used by the exact product +expansion. -/ +abbrev FourEndpointSupportChoiceData + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) := + Σ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + NearSkeletonChoice (↥P.edges) (FourEndpointDeficit alpha) + (fourEndpointHalfDeficitAllowed alpha hAlpha P) + +noncomputable instance instFintypeFourEndpointSupportChoiceData + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) : + Fintype (FourEndpointSupportChoiceData alpha hAlpha k) := + Fintype.ofFinite _ + +/-- Decode optional deficit choices to their multiplicity table. `none` means +full containment, while `some h` means multiplicity `m-h`. -/ +noncomputable def fourEndpointSupportChoiceTable + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (D : FourEndpointSupportChoiceData alpha hAlpha k) : + FourEndpointBlockAtom alpha hAlpha k → + FourEndpointBlockAtom alpha hAlpha k → Nat := fun a b => + if hab : (a, b) ∈ D.1.edges then + let cell : ↥D.1.edges := ⟨(a, b), hab⟩ + let m := fourEndpointOverlapSize alpha hAlpha a.1 b.1 + match D.2 cell with + | none => m + | some deficit => m - deficit.1.1 + else 0 + +/-- Convert the older dependent support/deficit data to the optional-choice +representation. Zero deficit becomes `none`; a positive deficit becomes the +corresponding `some` value. -/ +noncomputable def fourEndpointSupportDeficitToChoice + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (D : FourEndpointSupportDeficitData alpha hAlpha k) : + NearSkeletonChoice (↥D.1.edges) (FourEndpointDeficit alpha) + (fourEndpointHalfDeficitAllowed alpha hAlpha D.1) := fun cell => + let h := (D.2 cell).1.1 + if hz : h = 0 then none else + let deficit : FourEndpointDeficit alpha := + ⟨h, Nat.lt_succ_of_le + ((Nat.le_of_lt_succ (D.2 cell).1.2).trans + (fourEndpointOverlapSize_le_alpha + alpha hAlpha cell.1.1.1 cell.1.2.1))⟩ + some ⟨deficit, by + simp only [fourEndpointHalfDeficitAllowed, Finset.mem_filter, + Finset.mem_univ, true_and] + exact ⟨Nat.pos_of_ne_zero hz, (D.2 cell).2⟩⟩ + +/-- Support/deficit data regarded as support/optional-choice data. -/ +noncomputable def fourEndpointSupportDeficitToChoiceData + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (D : FourEndpointSupportDeficitData alpha hAlpha k) : + FourEndpointSupportChoiceData alpha hAlpha k := + ⟨D.1, fourEndpointSupportDeficitToChoice alpha hAlpha D⟩ + +/-- The optional-choice decoder agrees exactly with the older deficit-table +decoder. -/ +theorem fourEndpointSupportChoiceTable_toChoice_eq + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (D : FourEndpointSupportDeficitData alpha hAlpha k) : + fourEndpointSupportChoiceTable alpha hAlpha + (fourEndpointSupportDeficitToChoiceData alpha hAlpha D) = + fourEndpointSupportDeficitTable alpha hAlpha D := by + funext a b + by_cases hab : (a, b) ∈ D.1.edges + · let cell : ↥D.1.edges := ⟨(a, b), hab⟩ + by_cases hz : (D.2 cell).1.1 = 0 + · simp [fourEndpointSupportChoiceTable, + fourEndpointSupportDeficitToChoiceData, + fourEndpointSupportDeficitToChoice, + fourEndpointSupportDeficitTable, hab, cell, hz] + · simp [fourEndpointSupportChoiceTable, + fourEndpointSupportDeficitToChoiceData, + fourEndpointSupportDeficitToChoice, + fourEndpointSupportDeficitTable, hab, cell, hz] + · simp [fourEndpointSupportChoiceTable, + fourEndpointSupportDeficitToChoiceData, + fourEndpointSupportDeficitTable, hab] + +/-- Direct attained-demand encoding into the analytic optional-choice type. -/ +noncomputable def fourEndpointDemandSupportChoiceEncoding + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (demand : ProfileCanonicalHighSkeleton k + (fourEndpointLargestSize alpha hAlpha)) : + FourEndpointSupportChoiceData alpha hAlpha k := + fourEndpointSupportDeficitToChoiceData alpha hAlpha + (fourEndpointDemandSupportDeficitEncoding + alpha hAlpha k hcover slotIndex demand) + +/-- Decoding the direct optional-choice encoding recovers the attained demand's +abstract multiplicity table. -/ +theorem fourEndpointSupportChoiceTable_encoding_eq + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (demand : ProfileCanonicalHighSkeleton k + (fourEndpointLargestSize alpha hAlpha)) : + fourEndpointSupportChoiceTable alpha hAlpha + (fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex demand) = + fourEndpointAbstractDemandTable alpha hAlpha k slotIndex demand := by + rw [fourEndpointDemandSupportChoiceEncoding, + fourEndpointSupportChoiceTable_toChoice_eq, + fourEndpointSupportDeficitTable_encoding_eq] + +/-- The direct support/optional-choice encoding is injective on attained +canonical high demands. -/ +theorem fourEndpointDemandSupportChoiceEncoding_injective + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) : + Function.Injective + (fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex) := by + intro demand₁ demand₂ hdata + apply fourEndpointAbstractDemandTable_injective + alpha hAlpha k hcover slotIndex + have hdecoded := congrArg + (fourEndpointSupportChoiceTable alpha hAlpha) hdata + simpa only [fourEndpointSupportChoiceTable_encoding_eq] using hdecoded + +/-- A reference support weight times the exact product charge of one optional +deficit choice. -/ +noncomputable def fourEndpointSupportChoiceChargedWeight + (n alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (reference : FourEndpointAbstractBlockSkeleton alpha hAlpha k → ENNReal) + (D : FourEndpointSupportChoiceData alpha hAlpha k) : ENNReal := + reference D.1 * + nearSkeletonChoiceWeight + (fourEndpointHalfDeficitAllowed alpha hAlpha D.1) + (fourEndpointHalfDeficitWeight n alpha hAlpha D.1) D.2 + +/-- Summing all support/choice data is exactly a sum over supports of reference +weight times the product of local deficit partition functions. -/ +theorem sum_fourEndpointSupportChoiceChargedWeight_eq + (n alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (reference : FourEndpointAbstractBlockSkeleton alpha hAlpha k → ENNReal) : + (∑ D : FourEndpointSupportChoiceData alpha hAlpha k, + fourEndpointSupportChoiceChargedWeight + n alpha hAlpha reference D) = + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * + ∏ cell : ↥P.edges, + (1 + ∑ deficit ∈ + fourEndpointHalfDeficitAllowed alpha hAlpha P cell, + fourEndpointHalfDeficitWeight + n alpha hAlpha P cell deficit) := by + rw [Fintype.sum_sigma] + apply Finset.sum_congr rfl + intro P _ + unfold fourEndpointSupportChoiceChargedWeight + rw [← Finset.mul_sum] + rw [sum_nearSkeletonChoiceWeight_eq_product] + +/-- Generic global assembly theorem. Any pointwise bound on attained demands by +their encoded support reference and optional-deficit charge immediately sums to +the product-form support bound, with no extra multiplicity factor. -/ +theorem sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (weightDemand : ProfileCanonicalHighSkeleton k + (fourEndpointLargestSize alpha hAlpha) → ENNReal) + (reference : FourEndpointAbstractBlockSkeleton alpha hAlpha k → ENNReal) + (hweight : ∀ demand, + weightDemand demand ≤ + fourEndpointSupportChoiceChargedWeight n alpha hAlpha reference + (fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex demand)) : + (∑ demand, weightDemand demand) ≤ + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * + ∏ cell : ↥P.edges, + (1 + ∑ deficit ∈ + fourEndpointHalfDeficitAllowed alpha hAlpha P cell, + fourEndpointHalfDeficitWeight + n alpha hAlpha P cell deficit) := by + classical + let encode := fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex + have hencode : Function.Injective encode := + fourEndpointDemandSupportChoiceEncoding_injective + alpha hAlpha k hcover slotIndex + calc + (∑ demand, weightDemand demand) ≤ + ∑ demand, + fourEndpointSupportChoiceChargedWeight + n alpha hAlpha reference (encode demand) := by + exact Finset.sum_le_sum fun demand _ => hweight demand + _ = ∑ D ∈ Finset.image encode Finset.univ, + fourEndpointSupportChoiceChargedWeight + n alpha hAlpha reference D := by + symm + rw [Finset.sum_image] + intro demand₁ _ demand₂ _ h + exact hencode h + _ ≤ ∑ D : FourEndpointSupportChoiceData alpha hAlpha k, + fourEndpointSupportChoiceChargedWeight + n alpha hAlpha reference D := by + apply Finset.sum_le_sum_of_subset + exact Finset.image_subset_iff.mpr fun _ _ => Finset.mem_univ _ + _ = _ := + sum_fourEndpointSupportChoiceChargedWeight_eq + n alpha hAlpha reference + +/-- Cellwise-bounded form of the direct support assembly. -/ +theorem sum_profileCanonicalHighSkeleton_le_directSupportChoiceBound + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (weightDemand : ProfileCanonicalHighSkeleton k + (fourEndpointLargestSize alpha hAlpha) → ENNReal) + (reference : FourEndpointAbstractBlockSkeleton alpha hAlpha k → ENNReal) + (bound : FourEndpointAbstractBlockSkeleton alpha hAlpha k → + FourEndpointBlockAtom alpha hAlpha k × + FourEndpointBlockAtom alpha hAlpha k → ENNReal) + (hweight : ∀ demand, + weightDemand demand ≤ + fourEndpointSupportChoiceChargedWeight n alpha hAlpha reference + (fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex demand)) + (hlocal : ∀ P (cell : ↥P.edges), + (∑ deficit ∈ fourEndpointHalfDeficitAllowed alpha hAlpha P cell, + fourEndpointHalfDeficitWeight n alpha hAlpha P cell deficit) ≤ + bound P cell.1) : + (∑ demand, weightDemand demand) ≤ + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * ∏ cell : ↥P.edges, (1 + bound P cell.1) := by + calc + (∑ demand, weightDemand demand) ≤ + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * + ∏ cell : ↥P.edges, + (1 + ∑ deficit ∈ + fourEndpointHalfDeficitAllowed alpha hAlpha P cell, + fourEndpointHalfDeficitWeight + n alpha hAlpha P cell deficit) := + sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct + n alpha hAlpha k hcover slotIndex weightDemand reference hweight + _ ≤ ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * ∏ cell : ↥P.edges, (1 + bound P cell.1) := by + apply Finset.sum_le_sum + intro P _ + apply mul_le_mul_left' + apply Finset.prod_le_prod' + intro cell _ + exact add_le_add_left (hlocal P cell) 1 + +#print axioms fourEndpointSupportChoiceTable_toChoice_eq +#print axioms fourEndpointDemandSupportChoiceEncoding_injective +#print axioms sum_fourEndpointSupportChoiceChargedWeight_eq +#print axioms sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct +#print axioms sum_profileCanonicalHighSkeleton_le_directSupportChoiceBound + +end + +end Erdos625 From 1bb904048f0d9956b3cc2374221a85f4aa6dbf62 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:20:12 +0300 Subject: [PATCH 02/59] Add exact regression for the half-deficit assembly --- .../section8_direct_half_deficit_assembly.py | 140 ++++++++++++++++++ 1 file changed, 140 insertions(+) create mode 100644 625/experiments/section8_direct_half_deficit_assembly.py diff --git a/625/experiments/section8_direct_half_deficit_assembly.py b/625/experiments/section8_direct_half_deficit_assembly.py new file mode 100644 index 00000000..856b5665 --- /dev/null +++ b/625/experiments/section8_direct_half_deficit_assembly.py @@ -0,0 +1,140 @@ +#!/usr/bin/env python3 +"""Exact regression for the simplified Section VIII half-deficit assembly. + +The checker verifies finite set inclusions, decoding, injectivity on small +support/deficit data, the optional-choice product identity, and the stronger +three-quarter geometric charge. It is standard-library only and is not a +proof of the random-graph asymptotics. +""" + +from __future__ import annotations + +from fractions import Fraction +from itertools import product +from math import comb + + +def require(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def exact_high_cut(a: int, m: int) -> int: + return m - (a // 2 + 1) + + +def exact_high_deficits(a: int, m: int) -> list[int]: + cut = max(-1, exact_high_cut(a, m)) + return [h for h in range(0, m + 1) if h <= cut] + + +def half_envelope(m: int) -> list[int]: + return [h for h in range(0, m + 1) if 2 * h < m] + + +def local_ratio(m: int, d: int, h: int) -> Fraction: + denominator = 1 + for t in range(1, h + 1): + denominator *= d + t + exponent = h * m - h * (h + 1) // 2 + return Fraction(comb(m, h), denominator * 2**exponent) + + +def charged_term(n: int, m: int, d: int, h: int) -> Fraction: + return n**h * local_ratio(m, d, h) + + +def check_envelope_inclusion() -> int: + checked = 0 + for a in range(9, 81): + for m in range(a // 2 + 1, a + 1): + exact = set(exact_high_deficits(a, m)) + half = set(half_envelope(m)) + require(exact <= half, f"high window not contained: a={a}, m={m}") + checked += 1 + return checked + + +def check_decode_and_injectivity() -> int: + checked = 0 + for m in range(2, 20): + deficits = half_envelope(m) + decoded = {h: m - h for h in deficits} + require(len(set(decoded.values())) == len(decoded), f"decode not injective at m={m}") + require(decoded[0] == m, f"zero deficit is not full containment at m={m}") + checked += len(deficits) + return checked + + +def check_product_identity() -> int: + checked = 0 + for cell_data in ( + ((7, 0),), + ((7, 0), (8, 1)), + ((7, 0), (8, 1), (9, 2)), + ): + local_weights: list[dict[int, Fraction]] = [] + for m, d in cell_data: + weights = {h: local_ratio(m, d, h) for h in half_envelope(m) if h > 0} + local_weights.append(weights) + lhs = Fraction(0) + choices = [[None, *weights.keys()] for weights in local_weights] + for choice in product(*choices): + term = Fraction(1) + for index, h in enumerate(choice): + if h is not None: + term *= local_weights[index][h] + lhs += term + rhs = Fraction(1) + for weights in local_weights: + rhs *= 1 + sum(weights.values(), Fraction(0)) + require(lhs == rhs, f"optional product identity failed for {cell_data}") + checked += 1 + return checked + + +def check_three_quarter_charge() -> int: + checked = 0 + for n in (10, 100, 1000): + for m in range(3, 80): + base = Fraction(n * m, 2 ** ((3 * m - 1) // 4)) + for d in range(4): + for h in half_envelope(m): + if h == 0: + continue + require( + charged_term(n, m, d, h) <= base**h, + f"three-quarter charge failed: n={n}, m={m}, d={d}, h={h}", + ) + checked += 1 + return checked + + +def check_enlargement_is_strict() -> int: + strict = 0 + for a in range(9, 60): + for m in range(a // 2 + 1, a): + if set(exact_high_deficits(a, m)) < set(half_envelope(m)): + strict += 1 + require(strict > 0, "the half-deficit envelope never strictly enlarges the exact window") + return strict + + +def main() -> None: + inclusion = check_envelope_inclusion() + decoding = check_decode_and_injectivity() + products = check_product_identity() + charges = check_three_quarter_charge() + strict = check_enlargement_is_strict() + + print("ERDOS 625 DIRECT HALF-DEFICIT ASSEMBLY: PASS") + print(f" exact-window inclusions: {inclusion}") + print(f" decoded deficit values: {decoding}") + print(f" optional product instances: {products}") + print(f" three-quarter charged terms: {charges}") + print(f" strict harmless enlargements: {strict}") + print(" scope: exact finite regression; not the endpoint asymptotic theorem") + + +if __name__ == "__main__": + main() From af14c98f8880b68201549003f6b8717d1d5a9c53 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:20:49 +0300 Subject: [PATCH 03/59] Document the direct half-deficit simplification --- ...ION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md | 227 ++++++++++++++++++ 1 file changed, 227 insertions(+) create mode 100644 625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md diff --git a/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md b/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md new file mode 100644 index 00000000..7762956f --- /dev/null +++ b/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md @@ -0,0 +1,227 @@ +# Section VIII: direct half-deficit assembly + +## 1. What is being simplified + +After the exact physical-fibre and pointwise weight identity in PR #53, the +remaining proof should not pass through another bespoke hierarchy of + +```text +exact high deficit subtype +-> optional deficit choice +-> local product expansion. +``` + +The analytic theorem already uses an optional choice in every distinguishable +block cell. The clean route is therefore to encode attained demands directly +into that same type. + +The second simplification is a harmless enlargement. An attained high cell +has full endpoint multiplicity `m`, actual multiplicity `j`, and deficit + +```text +h = m-j. +``` + +The canonical high condition implies + +```text +2h < m. +``` + +For an upper bound there is no need to preserve the more complicated exact +window + +```text +h <= m - (U/2+1). +``` + +We may sum every positive deficit satisfying `2h= 1 : 2h < m_e}. +``` + +A support/choice datum is + +```text +(P, omega), +``` + +where `omega(e)` is either + +- `none`, representing `h_e=0` and full containment; or +- `some h`, with `h in allowed_P(e)`. + +This is precisely `NearSkeletonChoice`. Decoding gives + +```text +j_e = m_e if omega(e)=none, +j_e = m_e-h_e if omega(e)=some h_e. +``` + +The attained-demand encoding from PR #48 maps into this type by sending zero +deficit to `none`. The decoded table is unchanged, so injectivity follows from +the already checked injectivity of the abstract demand table. + +## 3. One generic global theorem + +Let `R(P)` be any nonnegative reference weight on block supports, and let + +```text +q(P,e,h) +``` + +be the charged local deficit ratio. The charged weight of `(P,omega)` is + +```text +R(P) * product_e q(P,e,omega(e)), +``` + +with the convention that `none` contributes one. + +The new finite assembly theorem gives exactly + +```text +sum_(P,omega) chargedWeight(P,omega) += +sum_P R(P) * product_e + (1 + sum_(h in allowed_P(e)) q(P,e,h)). +``` + +If each attained demand weight is bounded pointwise by its encoded charged +weight, injectivity gives the same right-hand side as an upper bound for the +entire attained family. There is no extra factor for: + +- the number of deficit vectors; +- identical endpoint types; +- a choice of physical full completion; +- conversion between two deficit representations. + +## 4. Why the enlargement helps formalization + +The old exact cutoff depends simultaneously on the global largest endpoint +`U` and the local endpoint `m_e`. The half-deficit envelope depends only on +`m_e`. This removes from the global analytic assembly: + +1. `allHighDeficitCut` arithmetic; +2. reconstruction of the strict global high inequality after every local + choice; +3. the theorem that all four endpoint sizes lie above `U/2`; +4. a conversion from a dependent `Fin (m_e+1)` subtype to + `NearSkeletonChoice`; +5. a separate proof that the analytic product sums exactly the same data as the + combinatorial encoding. + +All that remains is the local inequality + +```text +2h < m_e, +``` + +which is already proved for attained demands and is exactly the premise of the +three-quarter exponent budget. + +## 5. Resulting proof architecture + +The remaining Section VIII proof can now be organized as follows. + +### Finite pointwise step + +For one attained demand with encoded support `P` and choice `omega`, prove + +```text +profileHighSkeletonWeight(demand) + <= R(P) * nearSkeletonChoiceWeight(omega). +``` + +PR #53 supplies the exact left-hand aggregate formula. The only new algebra is +therefore: + +- compare the partial local factors with their full local factors; +- apply the single global falling-factorial loss once. + +### Exact finite summation + +Apply the direct support/choice theorem. This automatically produces + +```text +sum_P R(P) * product_e (1 + local positive-deficit mass). +``` + +### Local analytic bound + +For + +```text +rho_e = n*m_e / 2^floor((3m_e-1)/4), +``` + +PR #49 gives + +```text +q(P,e,h) <= rho_e^h. +``` + +When `rho_e<=1/2`, + +```text +sum_(h>=1, 2h Date: Wed, 29 Jul 2026 09:21:07 +0300 Subject: [PATCH 04/59] Add focused CI for the direct half-deficit assembly --- .../erdos625-direct-half-deficit-assembly.yml | 67 +++++++++++++++++++ 1 file changed, 67 insertions(+) create mode 100644 .github/workflows/erdos625-direct-half-deficit-assembly.yml diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml new file mode 100644 index 00000000..d19ab04e --- /dev/null +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -0,0 +1,67 @@ +name: Erdős 625 direct half-deficit assembly + +on: + pull_request: + paths: + - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" + - "625/experiments/section8_direct_half_deficit_assembly.py" + - "625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md" + - ".github/workflows/erdos625-direct-half-deficit-assembly.yml" + workflow_dispatch: + +concurrency: + group: erdos625-direct-half-deficit-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + exact-regression: + runs-on: ubuntu-24.04 + steps: + - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5 + - name: Compile exact checker + run: python -m py_compile 625/experiments/section8_direct_half_deficit_assembly.py + - name: Run exact checker + run: python 625/experiments/section8_direct_half_deficit_assembly.py + - name: Run exact checker with optimization + run: python -O 625/experiments/section8_direct_half_deficit_assembly.py + + 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/Section8DirectHalfDeficitAssembly.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 the direct half-deficit assembly warning-fatally + working-directory: 625/formalization + shell: bash + run: | + set +e + lake build Erdos625.Section8DirectHalfDeficitAssembly --wfail \ + > /tmp/erdos625-direct-half-deficit.log 2>&1 + status=$? + tail -n 700 /tmp/erdos625-direct-half-deficit.log + exit $status + - name: Upload focused Lean log + if: always() + uses: actions/upload-artifact@v4 + with: + name: erdos625-direct-half-deficit-log + path: /tmp/erdos625-direct-half-deficit.log + if-no-files-found: ignore From 35b63b402e365424dd6732383bea9f4c52a06064 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:28:06 +0300 Subject: [PATCH 05/59] Add a coarse uniform half-deficit charge --- .../Section8CoarseHalfDeficitCharge.lean | 217 ++++++++++++++++++ 1 file changed, 217 insertions(+) create mode 100644 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean diff --git a/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean b/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean new file mode 100644 index 00000000..f840d2f4 --- /dev/null +++ b/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean @@ -0,0 +1,217 @@ +import Erdos625.Section8DirectHalfDeficitAssembly +import Erdos625.Section8ThreeQuarterDeficitArithmetic +import Erdos625.Section8AllHighDeficitProductBound +import Mathlib.Tactic + +/-! +# Section VIII: coarse uniform charge for the half-deficit envelope + +The exact local ratio contains a binomial factor and an endpoint-distance +factor. Neither is needed in the final asymptotic argument. Under the sole +condition `2h deficit.1) (alpha + 1) rho hrho + · exact card_fourEndpointHalfDeficitAllowed_le alpha hAlpha P + · intro cell deficit hdeficit + simpa only [fourEndpointHalfDeficitAllowed, Finset.mem_filter, + Finset.mem_univ, true_and] using hdeficit |>.1 + · intro cell deficit hdeficit + exact (fourEndpointHalfDeficitWeight_le_threeQuarterBase_pow_of_mem + n alpha hAlpha P cell deficit hdeficit).trans + (ENNReal.pow_le_pow_left (hbase cell)) + +/-- Global attained-demand bound after replacing every support's exact local +partition function by the same coarse base. -/ +theorem sum_profileCanonicalHighSkeleton_le_uniformHalfDeficitSupportSum + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (weightDemand : ProfileCanonicalHighSkeleton k + (fourEndpointLargestSize alpha hAlpha) → ENNReal) + (reference : FourEndpointAbstractBlockSkeleton alpha hAlpha k → ENNReal) + (rho : ENNReal) (hrho : rho ≤ 1) + (hweight : ∀ demand, + weightDemand demand ≤ + fourEndpointSupportChoiceChargedWeight n alpha hAlpha reference + (fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex demand)) + (hbase : ∀ P (cell : ↥P.edges), + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1) ≤ rho) : + (∑ demand, weightDemand demand) ≤ + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * + (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ P.edges.card := by + calc + (∑ demand, weightDemand demand) ≤ + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * + ∏ cell : ↥P.edges, + (1 + ∑ deficit ∈ + fourEndpointHalfDeficitAllowed alpha hAlpha P cell, + fourEndpointHalfDeficitWeight + n alpha hAlpha P cell deficit) := + sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct + n alpha hAlpha k hcover slotIndex weightDemand reference hweight + _ ≤ ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * + (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ P.edges.card := by + apply Finset.sum_le_sum + intro P _ + exact mul_le_mul_left' + (sum_fourEndpointHalfDeficitChoiceWeight_le_uniform + n alpha hAlpha P rho hrho (hbase P)) _ + +#print axioms nearCellTerm_le_threeQuarterCellBase_pow +#print axioms sum_fourEndpointHalfDeficitChoiceWeight_le_uniform +#print axioms sum_profileCanonicalHighSkeleton_le_uniformHalfDeficitSupportSum + +end + +end Erdos625 From c55813b9915b308ec9f4bc9b13674a8aa763a16f Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:28:30 +0300 Subject: [PATCH 06/59] Extend focused CI through the coarse half-deficit charge --- .../workflows/erdos625-direct-half-deficit-assembly.yml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index d19ab04e..8f75017f 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -4,6 +4,7 @@ on: pull_request: paths: - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" + - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/experiments/section8_direct_half_deficit_assembly.py" - "625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md" - ".github/workflows/erdos625-direct-half-deficit-assembly.yml" @@ -37,7 +38,8 @@ jobs: run: | if grep -nE \ '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ - 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean; then + 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ + 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -48,12 +50,12 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the direct half-deficit assembly warning-fatally + - name: Build the coarse half-deficit endpoint warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section8DirectHalfDeficitAssembly --wfail \ + lake build Erdos625.Section8CoarseHalfDeficitCharge --wfail \ > /tmp/erdos625-direct-half-deficit.log 2>&1 status=$? tail -n 700 /tmp/erdos625-direct-half-deficit.log From 459031ba4640fdbaa7e1a36ab7a270e543482982 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:29:47 +0300 Subject: [PATCH 07/59] Group full support references directly by endpoint table --- .../Section8DirectReferenceGrouping.lean | 144 ++++++++++++++++++ 1 file changed, 144 insertions(+) create mode 100644 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean diff --git a/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean new file mode 100644 index 00000000..1f90daa6 --- /dev/null +++ b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean @@ -0,0 +1,144 @@ +import Erdos625.Section8DirectHalfDeficitAssembly +import Erdos625.Section8EndpointDecoratedReferenceIdentification +import Mathlib.Tactic + +/-! +# Section VIII: direct grouping of full-support references + +The zero-deficit reference of a block support should not be reconstructed by a +second cardinality argument. Define it literally as the sum of the common +full-cell atom over every independent full stub matching in the selected block +cells. The total space of such decorated supports is tautologically equivalent +to the dependent sum over endpoint tables of the already defined +`FourEndpointDecoratedBlockPairing` fibres. + +Consequently the total reference sum is exactly `sum_L fourEndpointW(L)`. This +module is finite and exact: no endpoint transport inequality or asymptotic +estimate is asserted. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- The endpoint table carried by one abstract block support. -/ +def fourEndpointSupportTable + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : + FourEndpointFullTable where + toFun := P.typeTable + +/-- Regard an abstract support as a block pairing over its own endpoint table. -/ +def fourEndpointBlockPairingOfSupport + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : + FourEndpointBlockPairing alpha hAlpha k + (fourEndpointSupportTable alpha hAlpha P) := + ⟨P, rfl⟩ + +/-- Independent full-cell physical stub matchings on one abstract support. -/ +abbrev FourEndpointFullDecorationOfSupport + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) := + ∀ e : ↥P.edges, + SingleCellStubMatching + (fourEndpointSize alpha hAlpha e.1.1.1) + (fourEndpointSize alpha hAlpha e.1.2.1) + (fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1) + +/-- All block supports, decorated by literal full-cell physical matchings. -/ +abbrev FourEndpointAllDecoratedSupport + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) := + Σ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + FourEndpointFullDecorationOfSupport alpha hAlpha P + +/-- The total decorated-support space is exactly the dependent sum of the +existing endpoint-table fibres. -/ +def fourEndpointAllDecoratedSupportEquivSigmaTable + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) : + FourEndpointAllDecoratedSupport alpha hAlpha k ≃ + Σ L : FourEndpointFullTable, + FourEndpointDecoratedBlockPairing alpha hAlpha k L where + toFun z := + ⟨fourEndpointSupportTable alpha hAlpha z.1, + ⟨fourEndpointBlockPairingOfSupport alpha hAlpha z.1, z.2⟩⟩ + invFun z := ⟨z.2.1.1, z.2.2⟩ + left_inv z := rfl + right_inv := by + rintro ⟨L, ⟨P, hP⟩, decoration⟩ + have hL : fourEndpointSupportTable alpha hAlpha P = L := by + apply FourEndpointFullTable.ext + exact hP + subst L + rfl + +/-- The common atom attached to every full physical decoration of one support. -/ +def fourEndpointFullSupportAtomWeight + (n alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : ENNReal := + fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha + (fourEndpointSupportTable alpha hAlpha P) + +/-- Aggregate zero-deficit reference weight of one block support. -/ +def fourEndpointFullSupportReferenceWeight + (n alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : ENNReal := + ∑ _ : FourEndpointFullDecorationOfSupport alpha hAlpha P, + fourEndpointFullSupportAtomWeight n alpha hAlpha P + +/-- Direct reference grouping: summing literal full-support reference weights +over all block supports gives exactly the existing endpoint-table sum. -/ +theorem sum_fourEndpointFullSupportReferenceWeight_eq_sum_W + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) : + (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + fourEndpointFullSupportReferenceWeight n alpha hAlpha P) = + ∑ L : FourEndpointFullTable, + fourEndpointW n alpha hAlpha k L := by + let equivalence := + fourEndpointAllDecoratedSupportEquivSigmaTable alpha hAlpha k + calc + (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + fourEndpointFullSupportReferenceWeight n alpha hAlpha P) = + ∑ z : FourEndpointAllDecoratedSupport alpha hAlpha k, + fourEndpointFullSupportAtomWeight n alpha hAlpha z.1 := by + rw [Fintype.sum_sigma] + rfl + _ = ∑ z : Σ L : FourEndpointFullTable, + FourEndpointDecoratedBlockPairing alpha hAlpha k L, + fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha z.1 := by + simpa [equivalence, fourEndpointFullSupportAtomWeight, + fourEndpointAllDecoratedSupportEquivSigmaTable] using + equivalence.sum_comp + (fun z : Σ L : FourEndpointFullTable, + FourEndpointDecoratedBlockPairing alpha hAlpha k L => + fourEndpointDecoratedReferenceAtomWeight + n alpha hAlpha z.1) + _ = ∑ L : FourEndpointFullTable, + ∑ _ : FourEndpointDecoratedBlockPairing alpha hAlpha k L, + fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L := by + rw [Fintype.sum_sigma] + _ = ∑ L : FourEndpointFullTable, + fourEndpointW n alpha hAlpha k L := by + apply Finset.sum_congr rfl + intro L _ + exact sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW + n alpha hAlpha k L + +#print axioms fourEndpointAllDecoratedSupportEquivSigmaTable +#print axioms sum_fourEndpointFullSupportReferenceWeight_eq_sum_W + +end + +end Erdos625 From 083eac7a70ab2b919a9b2fdf196ca9c2891539da Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:30:14 +0300 Subject: [PATCH 08/59] Extend focused CI through direct reference grouping --- .../workflows/erdos625-direct-half-deficit-assembly.yml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index 8f75017f..189d1125 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -5,6 +5,7 @@ on: paths: - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" + - "625/formalization/Erdos625/Section8DirectReferenceGrouping.lean" - "625/experiments/section8_direct_half_deficit_assembly.py" - "625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md" - ".github/workflows/erdos625-direct-half-deficit-assembly.yml" @@ -39,7 +40,8 @@ jobs: if grep -nE \ '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ - 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean; then + 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ + 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -50,12 +52,12 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the coarse half-deficit endpoint warning-fatally + - name: Build the direct reference grouping warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section8CoarseHalfDeficitCharge --wfail \ + lake build Erdos625.Section8DirectReferenceGrouping --wfail \ > /tmp/erdos625-direct-half-deficit.log 2>&1 status=$? tail -n 700 /tmp/erdos625-direct-half-deficit.log From 4676581e8df9922889949b5ef5bd832b697a9483 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:34:22 +0300 Subject: [PATCH 09/59] Reduce the finite bare-skeleton sum to one common factor times sum W --- .../Section8FiniteBareSkeletonReduction.lean | 127 ++++++++++++++++++ 1 file changed, 127 insertions(+) create mode 100644 625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean diff --git a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean new file mode 100644 index 00000000..320062ef --- /dev/null +++ b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean @@ -0,0 +1,127 @@ +import Erdos625.Section8CoarseHalfDeficitCharge +import Erdos625.Section8DirectReferenceGrouping +import Mathlib.Tactic + +/-! +# Section VIII: finite bare-skeleton reduction + +This module combines the simplified interfaces already available on the branch. +For an abstract endpoint block support, the number of selected block cells is at +most the total number of row blocks. Hence the coarse optional-deficit factor +may be replaced by one common power. The direct reference-grouping theorem +then replaces the remaining support sum by the endpoint-table sum +`sum_L fourEndpointW(L)`. + +The resulting theorem has only two nontrivial premises: + +* a pointwise charged comparison for one attained demand; +* a uniform bound on the sixteen local three-quarter bases. + +No asymptotic statement is made here. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- A physical typed partial matching has no more edges than available row +stubs. -/ +theorem UnlabelledTypedSkeleton.edges_card_le_rowTotal + {I J : Type*} + [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] + {row : I → Nat} {col : J → Nat} + (S : UnlabelledTypedSkeleton row col) : + S.edges.card ≤ Finset.univ.sum row := by + have hinj : Set.InjOn (fun e : RowStub row × ColumnStub col => e.1) + (↑S.edges : Set (RowStub row × ColumnStub col)) := by + intro e₁ he₁ e₂ he₂ hfirst + exact S.leftUnique e₁ (by simpa using he₁) e₂ (by simpa using he₂) hfirst + have hcard : (S.edges.image fun e => e.1).card = S.edges.card := by + rw [Finset.card_image_of_injOn] + exact hinj + calc + S.edges.card = (S.edges.image fun e => e.1).card := hcard.symm + _ ≤ (Finset.univ : Finset (RowStub row)).card := by + apply Finset.card_le_card + exact Finset.subset_univ _ + _ = Fintype.card (RowStub row) := Finset.card_univ + _ = Finset.univ.sum row := card_rowStub row + +/-- Total number of row block slots in the four endpoint types. -/ +def fourEndpointTotalBlockCount + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) : Nat := + ∑ i : Fin 4, fourEndpointMultiplicity alpha hAlpha k i + +/-- Every abstract block matching has at most the total number of block slots. -/ +theorem fourEndpointAbstractBlockSkeleton_edges_card_le + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : + P.edges.card ≤ fourEndpointTotalBlockCount alpha hAlpha k := by + simpa only [fourEndpointTotalBlockCount] using + P.edges_card_le_rowTotal + +/-- Finite endpoint of the simplified Section VIII argument. A pointwise +charged comparison and a common local base imply a single common deficit factor +multiplying the exact endpoint-table reference sum. -/ +theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (weightDemand : ProfileCanonicalHighSkeleton k + (fourEndpointLargestSize alpha hAlpha) → ENNReal) + (rho : ENNReal) (hrho : rho ≤ 1) + (hweight : ∀ demand, + weightDemand demand ≤ + fourEndpointSupportChoiceChargedWeight n alpha hAlpha + (fourEndpointFullSupportReferenceWeight n alpha hAlpha) + (fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex demand)) + (hbase : ∀ P (cell : ↥P.edges), + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1) ≤ rho) : + (∑ demand, weightDemand demand) ≤ + (∑ L : FourEndpointFullTable, + fourEndpointW n alpha hAlpha k L) * + (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ + fourEndpointTotalBlockCount alpha hAlpha k := by + let common : ENNReal := + (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ + fourEndpointTotalBlockCount alpha hAlpha k + calc + (∑ demand, weightDemand demand) ≤ + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + fourEndpointFullSupportReferenceWeight n alpha hAlpha P * + (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ P.edges.card := + sum_profileCanonicalHighSkeleton_le_uniformHalfDeficitSupportSum + n alpha hAlpha k hcover slotIndex weightDemand + (fourEndpointFullSupportReferenceWeight n alpha hAlpha) + rho hrho hweight hbase + _ ≤ ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + fourEndpointFullSupportReferenceWeight n alpha hAlpha P * common := by + apply Finset.sum_le_sum + intro P _ + apply mul_le_mul_left' + exact pow_le_pow_right₀ (by simp [common]) + (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P) + _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + fourEndpointFullSupportReferenceWeight n alpha hAlpha P) * common := by + rw [Finset.sum_mul] + _ = (∑ L : FourEndpointFullTable, + fourEndpointW n alpha hAlpha k L) * common := by + rw [sum_fourEndpointFullSupportReferenceWeight_eq_sum_W] + _ = _ := by rfl + +#print axioms UnlabelledTypedSkeleton.edges_card_le_rowTotal +#print axioms fourEndpointAbstractBlockSkeleton_edges_card_le +#print axioms sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W + +end + +end Erdos625 From ccc5e771e9800245708b25ded41de2c37fae4149 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:34:47 +0300 Subject: [PATCH 10/59] Build the complete finite bare-skeleton reduction --- .../workflows/erdos625-direct-half-deficit-assembly.yml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index 189d1125..e4af5807 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -6,6 +6,7 @@ on: - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/formalization/Erdos625/Section8DirectReferenceGrouping.lean" + - "625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean" - "625/experiments/section8_direct_half_deficit_assembly.py" - "625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md" - ".github/workflows/erdos625-direct-half-deficit-assembly.yml" @@ -41,7 +42,8 @@ jobs: '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ - 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean; then + 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean \ + 625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean; then exit 1 fi - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1 @@ -52,12 +54,12 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the direct reference grouping warning-fatally + - name: Build the finite bare-skeleton reduction warning-fatally working-directory: 625/formalization shell: bash run: | set +e - lake build Erdos625.Section8DirectReferenceGrouping --wfail \ + lake build Erdos625.Section8FiniteBareSkeletonReduction --wfail \ > /tmp/erdos625-direct-half-deficit.log 2>&1 status=$? tail -n 700 /tmp/erdos625-direct-half-deficit.log From f65858da5ec8e762a565c1a5a307fc8efdf97ab6 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:36:57 +0300 Subject: [PATCH 11/59] Update the simplified Section 8 proof frontier --- ...ION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md | 204 ++++++++++-------- 1 file changed, 118 insertions(+), 86 deletions(-) diff --git a/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md b/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md index 7762956f..daa073a8 100644 --- a/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md +++ b/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md @@ -12,11 +12,11 @@ exact high deficit subtype ``` The analytic theorem already uses an optional choice in every distinguishable -block cell. The clean route is therefore to encode attained demands directly +block cell. The clean route is therefore to encode attained demands directly into that same type. -The second simplification is a harmless enlargement. An attained high cell -has full endpoint multiplicity `m`, actual multiplicity `j`, and deficit +The second simplification is a harmless enlargement. An attained high cell has +full endpoint multiplicity `m`, actual multiplicity `j`, and deficit ```text h = m-j. @@ -35,10 +35,31 @@ window h <= m - (U/2+1). ``` -We may sum every positive deficit satisfying `2h=1, 2h Date: Wed, 29 Jul 2026 09:45:08 +0300 Subject: [PATCH 12/59] Derive endpoint coordinates from the standard deficit equality --- .../Section8FourDeficitProfileCover.lean | 58 ++++++++++--------- 1 file changed, 31 insertions(+), 27 deletions(-) diff --git a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean index 21733164..37877fad 100644 --- a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean +++ b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean @@ -18,6 +18,26 @@ noncomputable section set_option autoImplicit false +/-- Equality of deficit values determines the finite size coordinate. -/ +theorem profileDeficit_eq_fourDeficit_imp_coordinate_eq + (alpha : Nat) (hAlpha : 5 < alpha) + (coord : Fin (alpha + 1)) (i : Fin 4) + (hdeficit : profileDeficit alpha coord = (fourDeficit i : Real)) : + coord = fourDeficitCoordinate alpha hAlpha i := by + let target := fourDeficitCoordinate alpha hAlpha i + have htarget : profileDeficit alpha target = (fourDeficit i : Real) := + profileDeficit_fourDeficitCoordinate alpha hAlpha i + have hsumCoord := profileClassSize_add_profileDeficit alpha coord + have hsumTarget := profileClassSize_add_profileDeficit alpha target + have hclass : profileClassSize coord = profileClassSize target := by + rw [hdeficit] at hsumCoord + rw [htarget] at hsumTarget + linarith + apply Fin.ext + unfold profileClassSize at hclass + norm_num at hclass + omega + /-- A profile supported on the four distinguished deficit coordinates has every actual block in one of the four endpoint-size slot families. -/ theorem isFourEndpointProfileCover_of_isFourDeficitSupported @@ -32,33 +52,16 @@ theorem isFourEndpointProfileCover_of_isFourDeficitSupported obtain ⟨coord, _hcoord, hrep⟩ := haMem simp only [Multiset.mem_replicate] at hrep obtain ⟨hkpos, hsize⟩ := hrep - rcases hsupport coord (by omega) with h0 | hrest - · subst coord - refine ⟨0, ?_⟩ - simp only [fourEndpointBlockSlots, Finset.mem_filter, - Finset.mem_univ, true_and] - change (a.1 : Nat) = fourEndpointSize alpha hAlpha 0 - simpa [fourEndpointSize, fourEndpointCoordinate] using hsize - · rcases hrest with h1 | hrest - · subst coord - refine ⟨1, ?_⟩ - simp only [fourEndpointBlockSlots, Finset.mem_filter, - Finset.mem_univ, true_and] - change (a.1 : Nat) = fourEndpointSize alpha hAlpha 1 - simpa [fourEndpointSize, fourEndpointCoordinate] using hsize - · rcases hrest with h2 | h3 - · subst coord - refine ⟨2, ?_⟩ - simp only [fourEndpointBlockSlots, Finset.mem_filter, - Finset.mem_univ, true_and] - change (a.1 : Nat) = fourEndpointSize alpha hAlpha 2 - simpa [fourEndpointSize, fourEndpointCoordinate] using hsize - · subst coord - refine ⟨3, ?_⟩ - simp only [fourEndpointBlockSlots, Finset.mem_filter, - Finset.mem_univ, true_and] - change (a.1 : Nat) = fourEndpointSize alpha hAlpha 3 - simpa [fourEndpointSize, fourEndpointCoordinate] using hsize + obtain ⟨i, hdeficit⟩ := hsupport coord hkpos + have hcoord : coord = fourDeficitCoordinate alpha hAlpha i := + profileDeficit_eq_fourDeficit_imp_coordinate_eq + alpha hAlpha coord i hdeficit + subst coord + refine ⟨i, ?_⟩ + simp only [fourEndpointBlockSlots, Finset.mem_filter, + Finset.mem_univ, true_and] + change (a.1 : Nat) = fourEndpointSize alpha hAlpha i + simpa [fourEndpointSize, fourEndpointCoordinate] using hsize /-- The concrete four-deficit embedding used by the midpoint construction satisfies the endpoint-cover hypothesis needed by the Section VIII block @@ -70,6 +73,7 @@ theorem fourDeficitEmbedding_isFourEndpointProfileCover apply isFourEndpointProfileCover_of_isFourDeficitSupported exact (fourDeficitEmbedding_profile_invariants alpha hAlpha m).2.2 +#print axioms profileDeficit_eq_fourDeficit_imp_coordinate_eq #print axioms isFourEndpointProfileCover_of_isFourDeficitSupported #print axioms fourDeficitEmbedding_isFourEndpointProfileCover From eebf7a63ef3785d5588ba01188d7ed89a1a52e97 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:45:36 +0300 Subject: [PATCH 13/59] Track the repaired four-deficit cover adapter in focused CI --- .github/workflows/erdos625-direct-half-deficit-assembly.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index e4af5807..b656de33 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -3,6 +3,7 @@ name: Erdős 625 direct half-deficit assembly on: pull_request: paths: + - "625/formalization/Erdos625/Section8FourDeficitProfileCover.lean" - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/formalization/Erdos625/Section8DirectReferenceGrouping.lean" @@ -40,6 +41,7 @@ jobs: run: | if grep -nE \ '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ + 625/formalization/Erdos625/Section8FourDeficitProfileCover.lean \ 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean \ From 06ee5c864e3648cffdf8af64996c9dc4c303a696 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:46:18 +0300 Subject: [PATCH 14/59] Cast the recovered class-size equality back to Nat explicitly --- .../Erdos625/Section8FourDeficitProfileCover.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean index 37877fad..add238bf 100644 --- a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean +++ b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean @@ -33,9 +33,10 @@ theorem profileDeficit_eq_fourDeficit_imp_coordinate_eq rw [hdeficit] at hsumCoord rw [htarget] at hsumTarget linarith + have hnat : coord.val + 1 = target.val + 1 := by + unfold profileClassSize at hclass + exact_mod_cast hclass apply Fin.ext - unfold profileClassSize at hclass - norm_num at hclass omega /-- A profile supported on the four distinguished deficit coordinates has every From b0c42ad8646896f4e8cbb11bc2f47fb3eede7ec5 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 09:55:40 +0300 Subject: [PATCH 15/59] Remove proof-irrelevance friction from deficit-table decoding --- .../Erdos625/Section8AttainedAllDeficitReindexing.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean b/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean index 77bb47c1..0c4d7dbe 100644 --- a/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean +++ b/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean @@ -125,13 +125,15 @@ theorem fourEndpointSupportDeficitTable_encoding_eq alpha hAlpha k hcover slotIndex demand).edges · let e : ↥(fourEndpointDemandBlockPairing alpha hAlpha k hcover slotIndex demand).1.edges := ⟨(a, b), hab⟩ - have hrec := fourEndpointCellMultiplicity_demandDeficit_eq + have hle := fourEndpointDemandCell_le_fullMultiplicity alpha hAlpha k hcover slotIndex demand e - simpa [fourEndpointSupportDeficitTable, + simp [fourEndpointSupportDeficitTable, fourEndpointDemandSupportDeficitEncoding, fourEndpointAbstractDemandTable, + fourEndpointDemandDeficit, fourEndpointCellMultiplicityOfDeficit, - fourEndpointCellFullMultiplicity, e, hab] using hrec + fourEndpointCellFullMultiplicity, e, hab] at hle ⊢ + omega · have hz : demand.1 (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a) (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b) = 0 := by From 747afab4205e6dd6c79ec57696cdfa8ce07b4117 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 10:04:08 +0300 Subject: [PATCH 16/59] Remove the unused simplifier argument in deficit decoding --- .../Erdos625/Section8AttainedAllDeficitReindexing.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean b/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean index 0c4d7dbe..1aba689d 100644 --- a/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean +++ b/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean @@ -131,7 +131,6 @@ theorem fourEndpointSupportDeficitTable_encoding_eq fourEndpointDemandSupportDeficitEncoding, fourEndpointAbstractDemandTable, fourEndpointDemandDeficit, - fourEndpointCellMultiplicityOfDeficit, fourEndpointCellFullMultiplicity, e, hab] at hle ⊢ omega · have hz : demand.1 From f6a81c112736b2b180b4aaea02fb5123dd6d983d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 10:06:25 +0300 Subject: [PATCH 17/59] Make the support-choice sum explicit and type the local bound --- .../Section8DirectHalfDeficitAssembly.lean | 29 +++++++++++++++---- 1 file changed, 23 insertions(+), 6 deletions(-) diff --git a/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean index c03b1fff..0633c148 100644 --- a/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean +++ b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean @@ -225,10 +225,18 @@ theorem sum_fourEndpointSupportChoiceChargedWeight_eq fourEndpointHalfDeficitAllowed alpha hAlpha P cell, fourEndpointHalfDeficitWeight n alpha hAlpha P cell deficit) := by + classical + change + (∑ D : Σ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + NearSkeletonChoice (↥P.edges) (FourEndpointDeficit alpha) + (fourEndpointHalfDeficitAllowed alpha hAlpha P), + reference D.1 * + nearSkeletonChoiceWeight + (fourEndpointHalfDeficitAllowed alpha hAlpha D.1) + (fourEndpointHalfDeficitWeight n alpha hAlpha D.1) D.2) = _ rw [Fintype.sum_sigma] apply Finset.sum_congr rfl intro P _ - unfold fourEndpointSupportChoiceChargedWeight rw [← Finset.mul_sum] rw [sum_nearSkeletonChoiceWeight_eq_product] @@ -301,7 +309,8 @@ theorem sum_profileCanonicalHighSkeleton_le_directSupportChoiceBound fourEndpointSupportChoiceChargedWeight n alpha hAlpha reference (fourEndpointDemandSupportChoiceEncoding alpha hAlpha k hcover slotIndex demand)) - (hlocal : ∀ P (cell : ↥P.edges), + (hlocal : ∀ (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) + (cell : ↥P.edges), (∑ deficit ∈ fourEndpointHalfDeficitAllowed alpha hAlpha P cell, fourEndpointHalfDeficitWeight n alpha hAlpha P cell deficit) ≤ bound P cell.1) : @@ -323,10 +332,18 @@ theorem sum_profileCanonicalHighSkeleton_le_directSupportChoiceBound reference P * ∏ cell : ↥P.edges, (1 + bound P cell.1) := by apply Finset.sum_le_sum intro P _ - apply mul_le_mul_left' - apply Finset.prod_le_prod' - intro cell _ - exact add_le_add_left (hlocal P cell) 1 + have hprod : + (∏ cell : ↥P.edges, + (1 + ∑ deficit ∈ + fourEndpointHalfDeficitAllowed alpha hAlpha P cell, + fourEndpointHalfDeficitWeight + n alpha hAlpha P cell deficit)) ≤ + ∏ cell : ↥P.edges, (1 + bound P cell.1) := by + apply Finset.prod_le_prod' + intro cell _ + exact add_le_add_left (hlocal P cell) 1 + simpa [mul_comm] using + (mul_le_mul_right hprod (reference P)) #print axioms fourEndpointSupportChoiceTable_toChoice_eq #print axioms fourEndpointDemandSupportChoiceEncoding_injective From c1e78a7cfc0279c88d3fb136d787fd30383e765d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 10:15:26 +0300 Subject: [PATCH 18/59] Use the canonical Sigma Fintype and keep one direct assembly endpoint --- .../Section8DirectHalfDeficitAssembly.lean | 69 +------------------ 1 file changed, 1 insertion(+), 68 deletions(-) diff --git a/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean index 0633c148..823bb1a6 100644 --- a/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean +++ b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean @@ -74,12 +74,6 @@ abbrev FourEndpointSupportChoiceData NearSkeletonChoice (↥P.edges) (FourEndpointDeficit alpha) (fourEndpointHalfDeficitAllowed alpha hAlpha P) -noncomputable instance instFintypeFourEndpointSupportChoiceData - (alpha : Nat) (hAlpha : 5 < alpha) - (k : ColoringProfile (alpha + 1)) : - Fintype (FourEndpointSupportChoiceData alpha hAlpha k) := - Fintype.ofFinite _ - /-- Decode optional deficit choices to their multiplicity table. `none` means full containment, while `some h` means multiplicity `m-h`. -/ noncomputable def fourEndpointSupportChoiceTable @@ -226,17 +220,10 @@ theorem sum_fourEndpointSupportChoiceChargedWeight_eq fourEndpointHalfDeficitWeight n alpha hAlpha P cell deficit) := by classical - change - (∑ D : Σ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, - NearSkeletonChoice (↥P.edges) (FourEndpointDeficit alpha) - (fourEndpointHalfDeficitAllowed alpha hAlpha P), - reference D.1 * - nearSkeletonChoiceWeight - (fourEndpointHalfDeficitAllowed alpha hAlpha D.1) - (fourEndpointHalfDeficitWeight n alpha hAlpha D.1) D.2) = _ rw [Fintype.sum_sigma] apply Finset.sum_congr rfl intro P _ + unfold fourEndpointSupportChoiceChargedWeight rw [← Finset.mul_sum] rw [sum_nearSkeletonChoiceWeight_eq_product] @@ -292,64 +279,10 @@ theorem sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct sum_fourEndpointSupportChoiceChargedWeight_eq n alpha hAlpha reference -/-- Cellwise-bounded form of the direct support assembly. -/ -theorem sum_profileCanonicalHighSkeleton_le_directSupportChoiceBound - (n alpha : Nat) (hAlpha : 5 < alpha) - (k : ColoringProfile (alpha + 1)) - (hcover : IsFourEndpointProfileCover alpha hAlpha k) - (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) - (weightDemand : ProfileCanonicalHighSkeleton k - (fourEndpointLargestSize alpha hAlpha) → ENNReal) - (reference : FourEndpointAbstractBlockSkeleton alpha hAlpha k → ENNReal) - (bound : FourEndpointAbstractBlockSkeleton alpha hAlpha k → - FourEndpointBlockAtom alpha hAlpha k × - FourEndpointBlockAtom alpha hAlpha k → ENNReal) - (hweight : ∀ demand, - weightDemand demand ≤ - fourEndpointSupportChoiceChargedWeight n alpha hAlpha reference - (fourEndpointDemandSupportChoiceEncoding - alpha hAlpha k hcover slotIndex demand)) - (hlocal : ∀ (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) - (cell : ↥P.edges), - (∑ deficit ∈ fourEndpointHalfDeficitAllowed alpha hAlpha P cell, - fourEndpointHalfDeficitWeight n alpha hAlpha P cell deficit) ≤ - bound P cell.1) : - (∑ demand, weightDemand demand) ≤ - ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, - reference P * ∏ cell : ↥P.edges, (1 + bound P cell.1) := by - calc - (∑ demand, weightDemand demand) ≤ - ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, - reference P * - ∏ cell : ↥P.edges, - (1 + ∑ deficit ∈ - fourEndpointHalfDeficitAllowed alpha hAlpha P cell, - fourEndpointHalfDeficitWeight - n alpha hAlpha P cell deficit) := - sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct - n alpha hAlpha k hcover slotIndex weightDemand reference hweight - _ ≤ ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, - reference P * ∏ cell : ↥P.edges, (1 + bound P cell.1) := by - apply Finset.sum_le_sum - intro P _ - have hprod : - (∏ cell : ↥P.edges, - (1 + ∑ deficit ∈ - fourEndpointHalfDeficitAllowed alpha hAlpha P cell, - fourEndpointHalfDeficitWeight - n alpha hAlpha P cell deficit)) ≤ - ∏ cell : ↥P.edges, (1 + bound P cell.1) := by - apply Finset.prod_le_prod' - intro cell _ - exact add_le_add_left (hlocal P cell) 1 - simpa [mul_comm] using - (mul_le_mul_right hprod (reference P)) - #print axioms fourEndpointSupportChoiceTable_toChoice_eq #print axioms fourEndpointDemandSupportChoiceEncoding_injective #print axioms sum_fourEndpointSupportChoiceChargedWeight_eq #print axioms sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct -#print axioms sum_profileCanonicalHighSkeleton_le_directSupportChoiceBound end From 0729b909fbfc203d060dd1650cb4b2ca03e622fe Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 10:27:37 +0300 Subject: [PATCH 19/59] Normalize the dependent support-choice sum before factorization --- .../Section8DirectHalfDeficitAssembly.lean | 84 ++++++++----------- 1 file changed, 37 insertions(+), 47 deletions(-) diff --git a/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean index 823bb1a6..687d557f 100644 --- a/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean +++ b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean @@ -6,25 +6,17 @@ import Mathlib.Tactic /-! # Section VIII: direct support/choice assembly over the half-deficit envelope -The exact attained-demand encoding currently uses a dependent subtype carrying -one deficit in every selected endpoint cell. The analytic product theorem uses -`NearSkeletonChoice`, where zero deficit is represented by `none` and every -positive deficit is represented by `some h`. +An attained high demand is encoded directly by its abstract block matching and +one optional positive deficit in each selected cell. The admissible window is +enlarged to the local condition `2 h < m`, which every attained high cell +satisfies. Because all weights are nonnegative, this enlargement is harmless +for an upper bound and matches the hypothesis of the three-quarter exponent +estimate. -This module removes the later conversion burden. It enlarges the admissible -window to the simpler condition `2 h < m`, which every attained high cell -already satisfies, and maps attained demands directly into the same optional -choice type used by the product expansion. Since all weights are nonnegative, -the enlargement is harmless for an upper bound. - -The final theorem is a generic finite assembly principle: once one has a -pointwise comparison of an attained demand with a reference support weight times -its optional-deficit charge, the entire attained sum is bounded by one sum over -block supports of reference weight times a product of local partition -functions. - -No pointwise weight comparison, endpoint transportation estimate, or phase -asymptotic is asserted here. +The exported assembly theorem has one premise: a pointwise comparison of each +attained demand with a support reference times its encoded deficit charge. It +then sums the full attained family into a product of local partition functions, +with no additional fibre multiplicity. -/ namespace Erdos625 @@ -35,8 +27,7 @@ noncomputable section set_option autoImplicit false -/-- Every four-endpoint overlap size is at most `alpha`. This lets us use the -single ambient deficit type `Fin (alpha+1)` for all selected cells. -/ +/-- Every four-endpoint overlap size is at most `alpha`. -/ theorem fourEndpointOverlapSize_le_alpha (alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) : fourEndpointOverlapSize alpha hAlpha i j ≤ alpha := by @@ -44,8 +35,7 @@ theorem fourEndpointOverlapSize_le_alpha simp [fourEndpointOverlapSize, fourEndpointSize, fourEndpointCoordinate, fourDeficitCoordinate, fourDeficit] <;> omega -/-- Positive deficits in the enlarged half-deficit envelope. The original -strict global cutoff is not needed for the upper bound once `2 h < m` is known. -/ +/-- Positive deficits in the enlarged half-deficit envelope. -/ def fourEndpointHalfDeficitAllowed (alpha : Nat) (hAlpha : 5 < alpha) {k : ColoringProfile (alpha + 1)} @@ -54,7 +44,7 @@ def fourEndpointHalfDeficitAllowed let m := fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1 Finset.univ.filter fun deficit => 0 < deficit.1 ∧ 2 * deficit.1 < m -/-- The already charged local ratio used for one positive deficit. -/ +/-- Charged local ratio for one positive deficit. -/ def fourEndpointHalfDeficitWeight (n alpha : Nat) (hAlpha : 5 < alpha) {k : ColoringProfile (alpha + 1)} @@ -64,9 +54,8 @@ def fourEndpointHalfDeficitWeight (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1) (Nat.dist cell.1.1.1.val cell.1.2.1.val) deficit.1 -/-- One abstract block matching together with the optional positive deficit in -every selected cell. This is the same data structure used by the exact product -expansion. -/ +/-- One block matching together with one optional positive deficit in each +selected cell. -/ abbrev FourEndpointSupportChoiceData (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) := @@ -74,8 +63,7 @@ abbrev FourEndpointSupportChoiceData NearSkeletonChoice (↥P.edges) (FourEndpointDeficit alpha) (fourEndpointHalfDeficitAllowed alpha hAlpha P) -/-- Decode optional deficit choices to their multiplicity table. `none` means -full containment, while `some h` means multiplicity `m-h`. -/ +/-- Decode optional choices to the corresponding multiplicity table. -/ noncomputable def fourEndpointSupportChoiceTable (alpha : Nat) (hAlpha : 5 < alpha) {k : ColoringProfile (alpha + 1)} @@ -90,9 +78,7 @@ noncomputable def fourEndpointSupportChoiceTable | some deficit => m - deficit.1.1 else 0 -/-- Convert the older dependent support/deficit data to the optional-choice -representation. Zero deficit becomes `none`; a positive deficit becomes the -corresponding `some` value. -/ +/-- Convert dependent deficit data to the optional-choice representation. -/ noncomputable def fourEndpointSupportDeficitToChoice (alpha : Nat) (hAlpha : 5 < alpha) {k : ColoringProfile (alpha + 1)} @@ -111,7 +97,7 @@ noncomputable def fourEndpointSupportDeficitToChoice Finset.mem_univ, true_and] exact ⟨Nat.pos_of_ne_zero hz, (D.2 cell).2⟩⟩ -/-- Support/deficit data regarded as support/optional-choice data. -/ +/-- Support/deficit data viewed as support/optional-choice data. -/ noncomputable def fourEndpointSupportDeficitToChoiceData (alpha : Nat) (hAlpha : 5 < alpha) {k : ColoringProfile (alpha + 1)} @@ -119,8 +105,7 @@ noncomputable def fourEndpointSupportDeficitToChoiceData FourEndpointSupportChoiceData alpha hAlpha k := ⟨D.1, fourEndpointSupportDeficitToChoice alpha hAlpha D⟩ -/-- The optional-choice decoder agrees exactly with the older deficit-table -decoder. -/ +/-- The optional-choice and dependent-deficit decoders agree. -/ theorem fourEndpointSupportChoiceTable_toChoice_eq (alpha : Nat) (hAlpha : 5 < alpha) {k : ColoringProfile (alpha + 1)} @@ -144,7 +129,7 @@ theorem fourEndpointSupportChoiceTable_toChoice_eq fourEndpointSupportDeficitToChoiceData, fourEndpointSupportDeficitTable, hab] -/-- Direct attained-demand encoding into the analytic optional-choice type. -/ +/-- Direct attained-demand encoding into the optional-choice type. -/ noncomputable def fourEndpointDemandSupportChoiceEncoding (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) @@ -157,8 +142,7 @@ noncomputable def fourEndpointDemandSupportChoiceEncoding (fourEndpointDemandSupportDeficitEncoding alpha hAlpha k hcover slotIndex demand) -/-- Decoding the direct optional-choice encoding recovers the attained demand's -abstract multiplicity table. -/ +/-- Decoding the direct encoding recovers the attained abstract demand table. -/ theorem fourEndpointSupportChoiceTable_encoding_eq (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) @@ -174,8 +158,7 @@ theorem fourEndpointSupportChoiceTable_encoding_eq fourEndpointSupportChoiceTable_toChoice_eq, fourEndpointSupportDeficitTable_encoding_eq] -/-- The direct support/optional-choice encoding is injective on attained -canonical high demands. -/ +/-- The direct support/choice encoding is injective. -/ theorem fourEndpointDemandSupportChoiceEncoding_injective (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) @@ -191,8 +174,7 @@ theorem fourEndpointDemandSupportChoiceEncoding_injective (fourEndpointSupportChoiceTable alpha hAlpha) hdata simpa only [fourEndpointSupportChoiceTable_encoding_eq] using hdecoded -/-- A reference support weight times the exact product charge of one optional -deficit choice. -/ +/-- Reference support weight times the exact optional-deficit charge. -/ noncomputable def fourEndpointSupportChoiceChargedWeight (n alpha : Nat) (hAlpha : 5 < alpha) {k : ColoringProfile (alpha + 1)} @@ -203,8 +185,7 @@ noncomputable def fourEndpointSupportChoiceChargedWeight (fourEndpointHalfDeficitAllowed alpha hAlpha D.1) (fourEndpointHalfDeficitWeight n alpha hAlpha D.1) D.2 -/-- Summing all support/choice data is exactly a sum over supports of reference -weight times the product of local deficit partition functions. -/ +/-- The support/choice sum factors exactly into local partition functions. -/ theorem sum_fourEndpointSupportChoiceChargedWeight_eq (n alpha : Nat) (hAlpha : 5 < alpha) {k : ColoringProfile (alpha + 1)} @@ -223,13 +204,22 @@ theorem sum_fourEndpointSupportChoiceChargedWeight_eq rw [Fintype.sum_sigma] apply Finset.sum_congr rfl intro P _ - unfold fourEndpointSupportChoiceChargedWeight + change + (∑ choice : NearSkeletonChoice (↥P.edges) (FourEndpointDeficit alpha) + (fourEndpointHalfDeficitAllowed alpha hAlpha P), + reference P * + nearSkeletonChoiceWeight + (fourEndpointHalfDeficitAllowed alpha hAlpha P) + (fourEndpointHalfDeficitWeight n alpha hAlpha P) choice) = + reference P * + ∏ cell : ↥P.edges, + (1 + ∑ deficit ∈ + fourEndpointHalfDeficitAllowed alpha hAlpha P cell, + fourEndpointHalfDeficitWeight n alpha hAlpha P cell deficit) rw [← Finset.mul_sum] rw [sum_nearSkeletonChoiceWeight_eq_product] -/-- Generic global assembly theorem. Any pointwise bound on attained demands by -their encoded support reference and optional-deficit charge immediately sums to -the product-form support bound, with no extra multiplicity factor. -/ +/-- A pointwise charged comparison sums with no extra multiplicity factor. -/ theorem sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct (n alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) From b9d36a93ae20101988a206466a8805696667e569 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 11:50:21 +0300 Subject: [PATCH 20/59] Fix finite-cardinality coercions in half-deficit charge --- .../Section8CoarseHalfDeficitCharge.lean | 38 +++++++++++-------- 1 file changed, 22 insertions(+), 16 deletions(-) diff --git a/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean b/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean index f840d2f4..af9b36c4 100644 --- a/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean +++ b/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean @@ -152,18 +152,22 @@ theorem sum_fourEndpointHalfDeficitChoiceWeight_le_uniform (fourEndpointHalfDeficitAllowed alpha hAlpha P) (fourEndpointHalfDeficitWeight n alpha hAlpha P) choice) ≤ (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ P.edges.card := by - apply sum_nearSkeletonChoiceWeight_le_uniform_pow - (fourEndpointHalfDeficitAllowed alpha hAlpha P) - (fourEndpointHalfDeficitWeight n alpha hAlpha P) - (fun deficit => deficit.1) (alpha + 1) rho hrho - · exact card_fourEndpointHalfDeficitAllowed_le alpha hAlpha P - · intro cell deficit hdeficit - simpa only [fourEndpointHalfDeficitAllowed, Finset.mem_filter, - Finset.mem_univ, true_and] using hdeficit |>.1 - · intro cell deficit hdeficit - exact (fourEndpointHalfDeficitWeight_le_threeQuarterBase_pow_of_mem - n alpha hAlpha P cell deficit hdeficit).trans - (ENNReal.pow_le_pow_left (hbase cell)) + have hbound := + sum_nearSkeletonChoiceWeight_le_uniform_pow + (fourEndpointHalfDeficitAllowed alpha hAlpha P) + (fourEndpointHalfDeficitWeight n alpha hAlpha P) + (fun deficit => deficit.1) (alpha + 1) rho hrho + (card_fourEndpointHalfDeficitAllowed_le alpha hAlpha P) + (by + intro cell deficit hdeficit + simpa only [fourEndpointHalfDeficitAllowed, Finset.mem_filter, + Finset.mem_univ, true_and] using hdeficit |>.1) + (by + intro cell deficit hdeficit + exact (fourEndpointHalfDeficitWeight_le_threeQuarterBase_pow_of_mem + n alpha hAlpha P cell deficit hdeficit).trans + (ENNReal.pow_le_pow_left (hbase cell))) + simpa only [Fintype.card_coe] using hbound /-- Global attained-demand bound after replacing every support's exact local partition function by the same coarse base. -/ @@ -181,7 +185,8 @@ theorem sum_profileCanonicalHighSkeleton_le_uniformHalfDeficitSupportSum fourEndpointSupportChoiceChargedWeight n alpha hAlpha reference (fourEndpointDemandSupportChoiceEncoding alpha hAlpha k hcover slotIndex demand)) - (hbase : ∀ P (cell : ↥P.edges), + (hbase : ∀ (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) + (cell : ↥P.edges), threeQuarterCellBase n (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1) ≤ rho) : (∑ demand, weightDemand demand) ≤ @@ -204,9 +209,10 @@ theorem sum_profileCanonicalHighSkeleton_le_uniformHalfDeficitSupportSum (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ P.edges.card := by apply Finset.sum_le_sum intro P _ - exact mul_le_mul_left' - (sum_fourEndpointHalfDeficitChoiceWeight_le_uniform - n alpha hAlpha P rho hrho (hbase P)) _ + simpa [mul_comm] using + (mul_le_mul_right + (sum_fourEndpointHalfDeficitChoiceWeight_le_uniform + n alpha hAlpha P rho hrho (hbase P)) (reference P)) #print axioms nearCellTerm_le_threeQuarterCellBase_pow #print axioms sum_fourEndpointHalfDeficitChoiceWeight_le_uniform From b99be0fe60cfaffe6e8f3a695171e9db88984397 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 11:51:32 +0300 Subject: [PATCH 21/59] Restrict endpoint reference grouping to attained finite tables --- .../Section8DirectReferenceGrouping.lean | 80 ++++++++++++------- 1 file changed, 51 insertions(+), 29 deletions(-) diff --git a/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean index 1f90daa6..3239dc17 100644 --- a/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean +++ b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean @@ -8,13 +8,17 @@ import Mathlib.Tactic The zero-deficit reference of a block support should not be reconstructed by a second cardinality argument. Define it literally as the sum of the common full-cell atom over every independent full stub matching in the selected block -cells. The total space of such decorated supports is tautologically equivalent -to the dependent sum over endpoint tables of the already defined +cells. + +The ambient type of all `Nat`-valued four-by-four tables is infinite. The +correct finite index is therefore the image of the finite block-support space. +The total space of decorated supports is tautologically equivalent to the +dependent sum over these attained endpoint tables of the already defined `FourEndpointDecoratedBlockPairing` fibres. -Consequently the total reference sum is exactly `sum_L fourEndpointW(L)`. This -module is finite and exact: no endpoint transport inequality or asymptotic -estimate is asserted. +Consequently the total reference sum is exactly the finite attained-table sum +of `fourEndpointW`. No endpoint transport inequality or asymptotic estimate is +asserted here. -/ namespace Erdos625 @@ -60,22 +64,40 @@ abbrev FourEndpointAllDecoratedSupport Σ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, FourEndpointFullDecorationOfSupport alpha hAlpha P +/-- The finite image of the block-support space in the endpoint-table space. -/ +noncomputable def fourEndpointAttainedFullTables + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) : Finset FourEndpointFullTable := by + classical + exact Finset.univ.image + (fun P : FourEndpointAbstractBlockSkeleton alpha hAlpha k => + fourEndpointSupportTable alpha hAlpha P) + +/-- An endpoint table that is actually carried by at least one abstract block +support. This is the finite table type relevant to the reference sum. -/ +abbrev FourEndpointAttainedFullTable + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) := + ↥(fourEndpointAttainedFullTables alpha hAlpha k) + /-- The total decorated-support space is exactly the dependent sum of the -existing endpoint-table fibres. -/ +attained endpoint-table fibres. -/ def fourEndpointAllDecoratedSupportEquivSigmaTable (alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) : FourEndpointAllDecoratedSupport alpha hAlpha k ≃ - Σ L : FourEndpointFullTable, - FourEndpointDecoratedBlockPairing alpha hAlpha k L where + Σ L : FourEndpointAttainedFullTable alpha hAlpha k, + FourEndpointDecoratedBlockPairing alpha hAlpha k L.1 where toFun z := - ⟨fourEndpointSupportTable alpha hAlpha z.1, - ⟨fourEndpointBlockPairingOfSupport alpha hAlpha z.1, z.2⟩⟩ + let L : FourEndpointAttainedFullTable alpha hAlpha k := + ⟨fourEndpointSupportTable alpha hAlpha z.1, + Finset.mem_image.mpr ⟨z.1, Finset.mem_univ z.1, rfl⟩⟩ + ⟨L, ⟨fourEndpointBlockPairingOfSupport alpha hAlpha z.1, z.2⟩⟩ invFun z := ⟨z.2.1.1, z.2.2⟩ left_inv z := rfl right_inv := by - rintro ⟨L, ⟨P, hP⟩, decoration⟩ - have hL : fourEndpointSupportTable alpha hAlpha P = L := by + rintro ⟨⟨L, hL⟩, ⟨P, hP⟩, decoration⟩ + have htable : fourEndpointSupportTable alpha hAlpha P = L := by apply FourEndpointFullTable.ext exact hP subst L @@ -98,14 +120,14 @@ def fourEndpointFullSupportReferenceWeight fourEndpointFullSupportAtomWeight n alpha hAlpha P /-- Direct reference grouping: summing literal full-support reference weights -over all block supports gives exactly the existing endpoint-table sum. -/ -theorem sum_fourEndpointFullSupportReferenceWeight_eq_sum_W +over all block supports gives exactly the finite attained endpoint-table sum. -/ +theorem sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W (n alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) : (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, fourEndpointFullSupportReferenceWeight n alpha hAlpha P) = - ∑ L : FourEndpointFullTable, - fourEndpointW n alpha hAlpha k L := by + ∑ L : FourEndpointAttainedFullTable alpha hAlpha k, + fourEndpointW n alpha hAlpha k L.1 := by let equivalence := fourEndpointAllDecoratedSupportEquivSigmaTable alpha hAlpha k calc @@ -115,29 +137,29 @@ theorem sum_fourEndpointFullSupportReferenceWeight_eq_sum_W fourEndpointFullSupportAtomWeight n alpha hAlpha z.1 := by rw [Fintype.sum_sigma] rfl - _ = ∑ z : Σ L : FourEndpointFullTable, - FourEndpointDecoratedBlockPairing alpha hAlpha k L, - fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha z.1 := by + _ = ∑ z : Σ L : FourEndpointAttainedFullTable alpha hAlpha k, + FourEndpointDecoratedBlockPairing alpha hAlpha k L.1, + fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha z.1.1 := by simpa [equivalence, fourEndpointFullSupportAtomWeight, fourEndpointAllDecoratedSupportEquivSigmaTable] using equivalence.sum_comp - (fun z : Σ L : FourEndpointFullTable, - FourEndpointDecoratedBlockPairing alpha hAlpha k L => + (fun z : Σ L : FourEndpointAttainedFullTable alpha hAlpha k, + FourEndpointDecoratedBlockPairing alpha hAlpha k L.1 => fourEndpointDecoratedReferenceAtomWeight - n alpha hAlpha z.1) - _ = ∑ L : FourEndpointFullTable, - ∑ _ : FourEndpointDecoratedBlockPairing alpha hAlpha k L, - fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L := by + n alpha hAlpha z.1.1) + _ = ∑ L : FourEndpointAttainedFullTable alpha hAlpha k, + ∑ _ : FourEndpointDecoratedBlockPairing alpha hAlpha k L.1, + fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L.1 := by rw [Fintype.sum_sigma] - _ = ∑ L : FourEndpointFullTable, - fourEndpointW n alpha hAlpha k L := by + _ = ∑ L : FourEndpointAttainedFullTable alpha hAlpha k, + fourEndpointW n alpha hAlpha k L.1 := by apply Finset.sum_congr rfl intro L _ exact sum_fourEndpointDecoratedReferenceAtomWeight_eq_fourEndpointW - n alpha hAlpha k L + n alpha hAlpha k L.1 #print axioms fourEndpointAllDecoratedSupportEquivSigmaTable -#print axioms sum_fourEndpointFullSupportReferenceWeight_eq_sum_W +#print axioms sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W end From f07d1516449f3b1c48c080f3f5d2da939d87225c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 11:52:23 +0300 Subject: [PATCH 22/59] Use attained endpoint tables in finite bare-skeleton reduction --- .../Section8FiniteBareSkeletonReduction.lean | 38 +++++++++++-------- 1 file changed, 22 insertions(+), 16 deletions(-) diff --git a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean index 320062ef..d2ae2000 100644 --- a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean +++ b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean @@ -5,12 +5,15 @@ import Mathlib.Tactic /-! # Section VIII: finite bare-skeleton reduction -This module combines the simplified interfaces already available on the branch. -For an abstract endpoint block support, the number of selected block cells is at -most the total number of row blocks. Hence the coarse optional-deficit factor -may be replaced by one common power. The direct reference-grouping theorem -then replaces the remaining support sum by the endpoint-table sum -`sum_L fourEndpointW(L)`. +This module combines the simplified finite interfaces. For an abstract +endpoint block support, the number of selected block cells is at most the total +number of row blocks. Hence the coarse optional-deficit factor may be replaced +by one common power. + +The endpoint-table index is the finite attained image of the support space, +not the infinite type of all `Nat`-valued four-by-four tables. Direct reference +grouping then replaces the remaining support sum by the attained-table sum of +`fourEndpointW`. The resulting theorem has only two nontrivial premises: @@ -68,7 +71,7 @@ theorem fourEndpointAbstractBlockSkeleton_edges_card_le /-- Finite endpoint of the simplified Section VIII argument. A pointwise charged comparison and a common local base imply a single common deficit factor -multiplying the exact endpoint-table reference sum. -/ +multiplying the exact attained endpoint-table reference sum. -/ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W (n alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) @@ -83,12 +86,13 @@ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W (fourEndpointFullSupportReferenceWeight n alpha hAlpha) (fourEndpointDemandSupportChoiceEncoding alpha hAlpha k hcover slotIndex demand)) - (hbase : ∀ P (cell : ↥P.edges), + (hbase : ∀ (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) + (cell : ↥P.edges), threeQuarterCellBase n (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1) ≤ rho) : (∑ demand, weightDemand demand) ≤ - (∑ L : FourEndpointFullTable, - fourEndpointW n alpha hAlpha k L) * + (∑ L : FourEndpointAttainedFullTable alpha hAlpha k, + fourEndpointW n alpha hAlpha k L.1) * (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ fourEndpointTotalBlockCount alpha hAlpha k := by let common : ENNReal := @@ -107,15 +111,17 @@ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W fourEndpointFullSupportReferenceWeight n alpha hAlpha P * common := by apply Finset.sum_le_sum intro P _ - apply mul_le_mul_left' - exact pow_le_pow_right₀ (by simp [common]) - (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P) + simpa [mul_comm] using + (mul_le_mul_right + (pow_le_pow_right₀ (by simp [common]) + (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) + (fourEndpointFullSupportReferenceWeight n alpha hAlpha P)) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, fourEndpointFullSupportReferenceWeight n alpha hAlpha P) * common := by rw [Finset.sum_mul] - _ = (∑ L : FourEndpointFullTable, - fourEndpointW n alpha hAlpha k L) * common := by - rw [sum_fourEndpointFullSupportReferenceWeight_eq_sum_W] + _ = (∑ L : FourEndpointAttainedFullTable alpha hAlpha k, + fourEndpointW n alpha hAlpha k L.1) * common := by + rw [sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W] _ = _ := by rfl #print axioms UnlabelledTypedSkeleton.edges_card_le_rowTotal From 570be3fe6f3aa7795dbb7a7c312a4b0b82bc00c9 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 11:56:48 +0300 Subject: [PATCH 23/59] Verify exact local and aggregate charged-weight ratios --- .../section8_direct_half_deficit_assembly.py | 108 +++++++++++++++++- 1 file changed, 103 insertions(+), 5 deletions(-) diff --git a/625/experiments/section8_direct_half_deficit_assembly.py b/625/experiments/section8_direct_half_deficit_assembly.py index 856b5665..c018f689 100644 --- a/625/experiments/section8_direct_half_deficit_assembly.py +++ b/625/experiments/section8_direct_half_deficit_assembly.py @@ -1,17 +1,17 @@ #!/usr/bin/env python3 """Exact regression for the simplified Section VIII half-deficit assembly. -The checker verifies finite set inclusions, decoding, injectivity on small -support/deficit data, the optional-choice product identity, and the stronger -three-quarter geometric charge. It is standard-library only and is not a -proof of the random-graph asymptotics. +The checker verifies finite set inclusions, decoding, injectivity, the optional +choice-product identity, the exact one-cell partial/full ratio, the single +global falling-factorial loss, and the stronger three-quarter geometric charge. +It is standard-library only and is not a proof of the random-graph asymptotics. """ from __future__ import annotations from fractions import Fraction from itertools import product -from math import comb +from math import comb, factorial def require(condition: bool, message: str) -> None: @@ -19,6 +19,14 @@ def require(condition: bool, message: str) -> None: raise RuntimeError(message) +def falling(n: int, r: int) -> int: + require(0 <= r <= n, f"invalid falling factorial ({n})_{r}") + value = 1 + for t in range(r): + value *= n - t + return value + + def exact_high_cut(a: int, m: int) -> int: return m - (a // 2 + 1) @@ -32,6 +40,24 @@ def half_envelope(m: int) -> list[int]: return [h for h in range(0, m + 1) if 2 * h < m] +def sign_reward(x: int) -> int: + return 2 ** (comb(x, 2) - 1) if x >= 3 else 1 + + +def local_matching_count(m: int, d: int, multiplicity: int) -> int: + """Number of partial matchings in an m by (m+d) endpoint cell.""" + require(0 <= multiplicity <= m, "infeasible local multiplicity") + return ( + falling(m, multiplicity) + * falling(m + d, multiplicity) + // factorial(multiplicity) + ) + + +def local_aggregate_factor(m: int, d: int, multiplicity: int) -> int: + return local_matching_count(m, d, multiplicity) * sign_reward(multiplicity) + + def local_ratio(m: int, d: int, h: int) -> Fraction: denominator = 1 for t in range(1, h + 1): @@ -93,6 +119,74 @@ def check_product_identity() -> int: return checked +def check_exact_local_ratio() -> int: + """Check the exact local identity underlying manuscript equation (8.21).""" + checked = 0 + for m in range(4, 41): + for d in range(4): + full = local_aggregate_factor(m, d, m) + for h in half_envelope(m): + partial = local_aggregate_factor(m, d, m - h) + require( + Fraction(partial, full) == local_ratio(m, d, h), + f"local ratio failed: m={m}, d={d}, h={h}", + ) + checked += 1 + return checked + + +def check_global_charged_comparison() -> int: + """Verify the complete pointwise comparison on small finite supports. + + The exact ratio is the product of the one-cell ratios times the single + ambient falling-factorial ratio. Replacing that global ratio by n^H gives + precisely the product of the charged local terms. + """ + checked = 0 + support_families = ( + ((7, 0),), + ((7, 0), (8, 1)), + ((7, 0), (8, 1), (9, 2)), + ((7, 3), (8, 2), (9, 1), (10, 0)), + ) + for cells in support_families: + full_total = sum(m for m, _d in cells) + n = max(80, full_total + 10) + full_numerator = 1 + for m, d in cells: + full_numerator *= local_aggregate_factor(m, d, m) + full_weight = Fraction(full_numerator, falling(n, full_total)) + + deficit_choices = [half_envelope(m) for m, _d in cells] + for deficits in product(*deficit_choices): + partial_total = sum(m - h for (m, _d), h in zip(cells, deficits)) + total_deficit = sum(deficits) + partial_numerator = 1 + exact_local_product = Fraction(1) + charged_product = Fraction(1) + for (m, d), h in zip(cells, deficits): + partial_numerator *= local_aggregate_factor(m, d, m - h) + exact_local_product *= local_ratio(m, d, h) + charged_product *= charged_term(n, m, d, h) + + partial_weight = Fraction(partial_numerator, falling(n, partial_total)) + ambient_ratio = Fraction(falling(n, full_total), falling(n, partial_total)) + require( + partial_weight == full_weight * exact_local_product * ambient_ratio, + f"exact aggregate ratio failed: cells={cells}, deficits={deficits}", + ) + require( + ambient_ratio <= n**total_deficit, + f"global denominator loss failed: cells={cells}, deficits={deficits}", + ) + require( + partial_weight <= full_weight * charged_product, + f"charged pointwise comparison failed: cells={cells}, deficits={deficits}", + ) + checked += 1 + return checked + + def check_three_quarter_charge() -> int: checked = 0 for n in (10, 100, 1000): @@ -124,6 +218,8 @@ def main() -> None: inclusion = check_envelope_inclusion() decoding = check_decode_and_injectivity() products = check_product_identity() + local_ratios = check_exact_local_ratio() + global_ratios = check_global_charged_comparison() charges = check_three_quarter_charge() strict = check_enlargement_is_strict() @@ -131,6 +227,8 @@ def main() -> None: print(f" exact-window inclusions: {inclusion}") print(f" decoded deficit values: {decoding}") print(f" optional product instances: {products}") + print(f" exact one-cell ratios: {local_ratios}") + print(f" exact aggregate charged comparisons: {global_ratios}") print(f" three-quarter charged terms: {charges}") print(f" strict harmless enlargements: {strict}") print(" scope: exact finite regression; not the endpoint asymptotic theorem") From c28c320d16cd02ee0de59505e569405cb3f6212c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 11:58:12 +0300 Subject: [PATCH 24/59] Isolate the local-product and single-global-loss comparison --- .../Section8PointwiseChargeProduct.lean | 79 +++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 625/formalization/Erdos625/Section8PointwiseChargeProduct.lean diff --git a/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean b/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean new file mode 100644 index 00000000..437775c5 --- /dev/null +++ b/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean @@ -0,0 +1,79 @@ +import Mathlib.Data.ENNReal.BigOperators +import Mathlib.Tactic + +/-! +# Section VIII: pointwise product reduction + +The remaining charged comparison has two logically independent inputs: + +* one local partial/full ratio in every selected cell; +* one global falling-factorial loss, paid only once. + +This module packages their finite multiplication. It deliberately contains no +endpoint-specific factorial algebra and no asymptotic estimate. Its purpose is +to prevent the final proof from redistributing the global denominator loss +cell-by-cell before the exact aggregate identity has been established. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- Multiply pointwise local comparisons and one independent global comparison. +The conclusion keeps the local and global charges visibly separate. -/ +theorem finiteProduct_mul_global_le + {Cell : Type*} [Fintype Cell] + (partial full localCharge : Cell → ENNReal) + (partialGlobal fullGlobal globalCharge : ENNReal) + (hlocal : ∀ c, partial c ≤ full c * localCharge c) + (hglobal : partialGlobal ≤ fullGlobal * globalCharge) : + (∏ c, partial c) * partialGlobal ≤ + ((∏ c, full c) * fullGlobal) * + (globalCharge * ∏ c, localCharge c) := by + have hprod : (∏ c, partial c) ≤ ∏ c, full c * localCharge c := by + apply Finset.prod_le_prod' + intro c _ + exact hlocal c + calc + (∏ c, partial c) * partialGlobal ≤ + (∏ c, full c * localCharge c) * + (fullGlobal * globalCharge) := + mul_le_mul' hprod hglobal + _ = ((∏ c, full c) * fullGlobal) * + (globalCharge * ∏ c, localCharge c) := by + rw [Finset.prod_mul_distrib] + ac_rfl + +/-- Specialization in which the single global loss is `base` raised to the +sum of the cell deficits. The global power is then absorbed into the local +charged factors `base^(deficit c) * localRatio c` exactly once. -/ +theorem finiteProduct_mul_globalPower_le_chargedProduct + {Cell : Type*} [Fintype Cell] + (partial full localRatio : Cell → ENNReal) + (deficit : Cell → Nat) + (partialGlobal fullGlobal base : ENNReal) + (hlocal : ∀ c, partial c ≤ full c * localRatio c) + (hglobal : partialGlobal ≤ + fullGlobal * base ^ (∑ c, deficit c)) : + (∏ c, partial c) * partialGlobal ≤ + ((∏ c, full c) * fullGlobal) * + ∏ c, (base ^ deficit c * localRatio c) := by + have h := finiteProduct_mul_global_le + partial full localRatio partialGlobal fullGlobal + (base ^ (∑ c, deficit c)) hlocal hglobal + have hcharge : + base ^ (∑ c, deficit c) * (∏ c, localRatio c) = + ∏ c, (base ^ deficit c * localRatio c) := by + rw [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum] + simpa only [hcharge] using h + +#print axioms finiteProduct_mul_global_le +#print axioms finiteProduct_mul_globalPower_le_chargedProduct + +end + +end Erdos625 From 8c0d039c451fef9299cdd0f962339aa214ac4202 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 11:58:58 +0300 Subject: [PATCH 25/59] Build the pointwise charge product with the finite reduction --- .../erdos625-direct-half-deficit-assembly.yml | 24 ++++++++++++++----- 1 file changed, 18 insertions(+), 6 deletions(-) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index b656de33..6040b691 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -5,6 +5,7 @@ on: paths: - "625/formalization/Erdos625/Section8FourDeficitProfileCover.lean" - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" + - "625/formalization/Erdos625/Section8PointwiseChargeProduct.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/formalization/Erdos625/Section8DirectReferenceGrouping.lean" - "625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean" @@ -43,6 +44,7 @@ jobs: '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \ 625/formalization/Erdos625/Section8FourDeficitProfileCover.lean \ 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ + 625/formalization/Erdos625/Section8PointwiseChargeProduct.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean \ 625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean; then @@ -56,16 +58,26 @@ jobs: use-mathlib-cache: true use-github-cache: false nanoda: false - - name: Build the finite bare-skeleton reduction warning-fatally + - name: Build the simplified Section VIII interfaces warning-fatally working-directory: 625/formalization shell: bash run: | - set +e - lake build Erdos625.Section8FiniteBareSkeletonReduction --wfail \ - > /tmp/erdos625-direct-half-deficit.log 2>&1 - status=$? + : > /tmp/erdos625-direct-half-deficit.log + for target in \ + Erdos625.Section8PointwiseChargeProduct \ + Erdos625.Section8FiniteBareSkeletonReduction; do + echo "=== $target ===" | tee -a /tmp/erdos625-direct-half-deficit.log + set +e + lake build "$target" --wfail \ + >> /tmp/erdos625-direct-half-deficit.log 2>&1 + status=$? + set -e + if [[ $status -ne 0 ]]; then + tail -n 700 /tmp/erdos625-direct-half-deficit.log + exit $status + fi + done tail -n 700 /tmp/erdos625-direct-half-deficit.log - exit $status - name: Upload focused Lean log if: always() uses: actions/upload-artifact@v4 From 16548108a3cbd0b8a7843cf65ae3faf2fad7a95c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:03:49 +0300 Subject: [PATCH 26/59] Absorb the single falling-factorial loss into local charges --- .../Section8PointwiseChargeProduct.lean | 65 ++++++++++++++++++- 1 file changed, 64 insertions(+), 1 deletion(-) diff --git a/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean b/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean index 437775c5..49962f12 100644 --- a/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean +++ b/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean @@ -1,3 +1,4 @@ +import Erdos625.Section8NearArithmeticFoundation import Mathlib.Data.ENNReal.BigOperators import Mathlib.Tactic @@ -69,10 +70,72 @@ theorem finiteProduct_mul_globalPower_le_chargedProduct base ^ (∑ c, deficit c) * (∏ c, localRatio c) = ∏ c, (base ^ deficit c * localRatio c) := by rw [Finset.prod_mul_distrib, Finset.prod_pow_eq_pow_sum] - simpa only [hcharge] using h + rw [hcharge] at h + exact h + +/-- The reciprocal of the smaller falling factorial is at most the reciprocal +of the full falling factorial times the single global loss `n^H`. This is the +reciprocal form of `denominatorLoss_eq_falling_and_le_pow` used by aggregate +weights. -/ +theorem inv_descFactorial_sub_le_inv_mul_pow + (n J H : Nat) (hH : H ≤ J) (hJ : J ≤ n) : + (((n.descFactorial (J - H) : Nat) : ENNReal)⁻¹) ≤ + (((n.descFactorial J : Nat) : ENNReal)⁻¹) * + (n : ENNReal) ^ H := by + let full : ENNReal := ((n.descFactorial J : Nat) : ENNReal) + let small : ENNReal := ((n.descFactorial (J - H) : Nat) : ENNReal) + have hfull0 : full ≠ 0 := by + dsimp [full] + exact_mod_cast + (Nat.ne_of_gt (Nat.descFactorial_pos.mpr hJ : 0 < n.descFactorial J)) + have hfullTop : full ≠ ∞ := by + dsimp [full] + exact ENNReal.natCast_ne_top _ + have hloss : denominatorLoss n J H ≤ (n : ENNReal) ^ H := + (denominatorLoss_eq_falling_and_le_pow n J H hH hJ).2 + have hinv : small⁻¹ = full⁻¹ * denominatorLoss n J H := by + unfold denominatorLoss + change small⁻¹ = full⁻¹ * (full / small) + rw [ENNReal.div_eq_inv_mul] + calc + small⁻¹ = small⁻¹ * (full⁻¹ * full) := by + rw [ENNReal.inv_mul_cancel hfull0 hfullTop, mul_one] + _ = full⁻¹ * (small⁻¹ * full) := by ac_rfl + rw [hinv] + simpa [mul_comm] using (mul_le_mul_right hloss full⁻¹) + +/-- Exact aggregate endpoint for the denominator bookkeeping. If each local +partial factor is bounded by its full factor times a literal local ratio, then +the aggregate partial weight with denominator `(n)_(J-H)` is bounded by the +full aggregate weight with denominator `(n)_J`, multiplied by the charged local +factors `n^(h_e) * localRatio_e`. + +The global falling-factorial comparison is invoked only once. -/ +theorem finiteProduct_mul_inv_descFactorial_sub_le_chargedProduct + {Cell : Type*} [Fintype Cell] + (partial full localRatio : Cell → ENNReal) + (deficit : Cell → Nat) + (n J : Nat) + (hdeficit : (∑ c, deficit c) ≤ J) + (hJ : J ≤ n) + (hlocal : ∀ c, partial c ≤ full c * localRatio c) : + (∏ c, partial c) * + (((n.descFactorial (J - ∑ c, deficit c) : Nat) : ENNReal)⁻¹) ≤ + ((∏ c, full c) * + (((n.descFactorial J : Nat) : ENNReal)⁻¹)) * + ∏ c, ((n : ENNReal) ^ deficit c * localRatio c) := by + apply finiteProduct_mul_globalPower_le_chargedProduct + partial full localRatio deficit + (((n.descFactorial (J - ∑ c, deficit c) : Nat) : ENNReal)⁻¹) + (((n.descFactorial J : Nat) : ENNReal)⁻¹) + (n : ENNReal) hlocal + exact inv_descFactorial_sub_le_inv_mul_pow + n J (∑ c, deficit c) hdeficit hJ #print axioms finiteProduct_mul_global_le #print axioms finiteProduct_mul_globalPower_le_chargedProduct +#print axioms inv_descFactorial_sub_le_inv_mul_pow +#print axioms finiteProduct_mul_inv_descFactorial_sub_le_chargedProduct end From 2debf1670849c213229df1c3d92e80f287d38f93 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:06:47 +0300 Subject: [PATCH 27/59] Canonicalize the common sixteen-type deficit base --- .../Section8CanonicalThreeQuarterRho.lean | 98 +++++++++++++++++++ 1 file changed, 98 insertions(+) create mode 100644 625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean diff --git a/625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean b/625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean new file mode 100644 index 00000000..4d383f4a --- /dev/null +++ b/625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean @@ -0,0 +1,98 @@ +import Erdos625.Section8CoarseHalfDeficitCharge +import Mathlib.Tactic + +/-! +# Section VIII: canonical common three-quarter base + +There are only sixteen endpoint types. Instead of carrying a support-dependent +hypothesis saying that one common `rho` dominates every selected cell, define +`rho` canonically as the sum of the sixteen endpoint-type bases. Every local +base is then bounded by `rho` by positivity. + +This removes the final cellwise domination premise from the finite +bare-skeleton reduction. The only analytic premise left is eventual smallness +of this explicit sixteen-term quantity. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- Explicit common charge obtained by summing the sixteen endpoint-type bases. -/ +def fourEndpointThreeQuarterRho + (n alpha : Nat) (hAlpha : 5 < alpha) : ENNReal := + ∑ i : Fin 4, ∑ j : Fin 4, + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha i j) + +/-- Each endpoint-type base is one nonnegative summand of the common charge. -/ +theorem threeQuarterCellBase_le_fourEndpointThreeQuarterRho + (n alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) : + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha i j) ≤ + fourEndpointThreeQuarterRho n alpha hAlpha := by + have hrow : + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha i j) ≤ + ∑ j' : Fin 4, + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha i j') := + Finset.single_le_sum + (s := Finset.univ) + (f := fun j' : Fin 4 => + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha i j')) + (fun _ _ => bot_le) (Finset.mem_univ j) + have houter : + (∑ j' : Fin 4, + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha i j')) ≤ + ∑ i' : Fin 4, ∑ j' : Fin 4, + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha i' j') := + Finset.single_le_sum + (s := Finset.univ) + (f := fun i' : Fin 4 => ∑ j' : Fin 4, + threeQuarterCellBase n + (fourEndpointOverlapSize alpha hAlpha i' j')) + (fun _ _ => bot_le) (Finset.mem_univ i) + exact hrow.trans houter + +/-- The global support sum with the canonical common base. No pairing-dependent +analytic premise remains. -/ +theorem sum_profileCanonicalHighSkeleton_le_canonicalThreeQuarterRhoSupportSum + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (weightDemand : ProfileCanonicalHighSkeleton k + (fourEndpointLargestSize alpha hAlpha) → ENNReal) + (reference : FourEndpointAbstractBlockSkeleton alpha hAlpha k → ENNReal) + (hrho : fourEndpointThreeQuarterRho n alpha hAlpha ≤ 1) + (hweight : ∀ demand, + weightDemand demand ≤ + fourEndpointSupportChoiceChargedWeight n alpha hAlpha reference + (fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex demand)) : + (∑ demand, weightDemand demand) ≤ + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + reference P * + (1 + ((alpha + 1 : Nat) : ENNReal) * + fourEndpointThreeQuarterRho n alpha hAlpha) ^ P.edges.card := by + apply sum_profileCanonicalHighSkeleton_le_uniformHalfDeficitSupportSum + n alpha hAlpha k hcover slotIndex weightDemand reference + (fourEndpointThreeQuarterRho n alpha hAlpha) hrho hweight + intro P cell + exact threeQuarterCellBase_le_fourEndpointThreeQuarterRho + n alpha hAlpha cell.1.1.1 cell.1.2.1 + +#print axioms threeQuarterCellBase_le_fourEndpointThreeQuarterRho +#print axioms sum_profileCanonicalHighSkeleton_le_canonicalThreeQuarterRhoSupportSum + +end + +end Erdos625 From b633a94f766837000561a6a15efc111485b65685 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:08:07 +0300 Subject: [PATCH 28/59] Remove the support-dependent base premise from the finite reduction --- .../Section8FiniteBareSkeletonReduction.lean | 65 +++++++++++++++++-- 1 file changed, 59 insertions(+), 6 deletions(-) diff --git a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean index d2ae2000..d8bc097d 100644 --- a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean +++ b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean @@ -1,4 +1,4 @@ -import Erdos625.Section8CoarseHalfDeficitCharge +import Erdos625.Section8CanonicalThreeQuarterRho import Erdos625.Section8DirectReferenceGrouping import Mathlib.Tactic @@ -15,10 +15,11 @@ not the infinite type of all `Nat`-valued four-by-four tables. Direct reference grouping then replaces the remaining support sum by the attained-table sum of `fourEndpointW`. -The resulting theorem has only two nontrivial premises: +The canonical common local base is the sum of the sixteen endpoint-type bases. +Thus the final canonical theorem has only two nontrivial premises: * a pointwise charged comparison for one attained demand; -* a uniform bound on the sixteen local three-quarter bases. +* smallness of one explicit sixteen-term quantity. No asymptotic statement is made here. -/ @@ -69,9 +70,7 @@ theorem fourEndpointAbstractBlockSkeleton_edges_card_le simpa only [fourEndpointTotalBlockCount] using P.edges_card_le_rowTotal -/-- Finite endpoint of the simplified Section VIII argument. A pointwise -charged comparison and a common local base imply a single common deficit factor -multiplying the exact attained endpoint-table reference sum. -/ +/-- Generic finite endpoint with an arbitrary common local base. -/ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W (n alpha : Nat) (hAlpha : 5 < alpha) (k : ColoringProfile (alpha + 1)) @@ -124,9 +123,63 @@ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W rw [sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W] _ = _ := by rfl +/-- Canonical finite endpoint. The support-dependent local-base premise has +been discharged by the explicit sum of the sixteen endpoint-type bases. -/ +theorem sum_profileCanonicalHighSkeleton_le_canonicalDeficitFactor_mul_sum_W + (n alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) + (hcover : IsFourEndpointProfileCover alpha hAlpha k) + (slotIndex : FourEndpointSlotIndexing alpha hAlpha k) + (weightDemand : ProfileCanonicalHighSkeleton k + (fourEndpointLargestSize alpha hAlpha) → ENNReal) + (hrho : fourEndpointThreeQuarterRho n alpha hAlpha ≤ 1) + (hweight : ∀ demand, + weightDemand demand ≤ + fourEndpointSupportChoiceChargedWeight n alpha hAlpha + (fourEndpointFullSupportReferenceWeight n alpha hAlpha) + (fourEndpointDemandSupportChoiceEncoding + alpha hAlpha k hcover slotIndex demand)) : + (∑ demand, weightDemand demand) ≤ + (∑ L : FourEndpointAttainedFullTable alpha hAlpha k, + fourEndpointW n alpha hAlpha k L.1) * + (1 + ((alpha + 1 : Nat) : ENNReal) * + fourEndpointThreeQuarterRho n alpha hAlpha) ^ + fourEndpointTotalBlockCount alpha hAlpha k := by + let common : ENNReal := + (1 + ((alpha + 1 : Nat) : ENNReal) * + fourEndpointThreeQuarterRho n alpha hAlpha) ^ + fourEndpointTotalBlockCount alpha hAlpha k + calc + (∑ demand, weightDemand demand) ≤ + ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + fourEndpointFullSupportReferenceWeight n alpha hAlpha P * + (1 + ((alpha + 1 : Nat) : ENNReal) * + fourEndpointThreeQuarterRho n alpha hAlpha) ^ P.edges.card := + sum_profileCanonicalHighSkeleton_le_canonicalThreeQuarterRhoSupportSum + n alpha hAlpha k hcover slotIndex weightDemand + (fourEndpointFullSupportReferenceWeight n alpha hAlpha) + hrho hweight + _ ≤ ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + fourEndpointFullSupportReferenceWeight n alpha hAlpha P * common := by + apply Finset.sum_le_sum + intro P _ + simpa [mul_comm] using + (mul_le_mul_right + (pow_le_pow_right₀ (by simp [common]) + (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) + (fourEndpointFullSupportReferenceWeight n alpha hAlpha P)) + _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, + fourEndpointFullSupportReferenceWeight n alpha hAlpha P) * common := by + rw [Finset.sum_mul] + _ = (∑ L : FourEndpointAttainedFullTable alpha hAlpha k, + fourEndpointW n alpha hAlpha k L.1) * common := by + rw [sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W] + _ = _ := by rfl + #print axioms UnlabelledTypedSkeleton.edges_card_le_rowTotal #print axioms fourEndpointAbstractBlockSkeleton_edges_card_le #print axioms sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W +#print axioms sum_profileCanonicalHighSkeleton_le_canonicalDeficitFactor_mul_sum_W end From 2f8ac78b2bc94657dd6f951c6504c6ae21c9be67 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:09:01 +0300 Subject: [PATCH 29/59] Validate the canonical sixteen-type deficit base --- .github/workflows/erdos625-direct-half-deficit-assembly.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index 6040b691..b6aadcfc 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -7,6 +7,7 @@ on: - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" - "625/formalization/Erdos625/Section8PointwiseChargeProduct.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" + - "625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean" - "625/formalization/Erdos625/Section8DirectReferenceGrouping.lean" - "625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean" - "625/experiments/section8_direct_half_deficit_assembly.py" @@ -46,6 +47,7 @@ jobs: 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ 625/formalization/Erdos625/Section8PointwiseChargeProduct.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ + 625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean \ 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean \ 625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean; then exit 1 @@ -65,6 +67,7 @@ jobs: : > /tmp/erdos625-direct-half-deficit.log for target in \ Erdos625.Section8PointwiseChargeProduct \ + Erdos625.Section8CanonicalThreeQuarterRho \ Erdos625.Section8FiniteBareSkeletonReduction; do echo "=== $target ===" | tee -a /tmp/erdos625-direct-half-deficit.log set +e From b923ed8fd79732ec45cb9f99e00d6451b3b9aad7 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:13:37 +0300 Subject: [PATCH 30/59] Avoid Lean's reserved partial keyword in charge products --- .../Section8PointwiseChargeProduct.lean | 62 +++++++++---------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean b/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean index 49962f12..4232001f 100644 --- a/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean +++ b/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean @@ -7,7 +7,7 @@ import Mathlib.Tactic The remaining charged comparison has two logically independent inputs: -* one local partial/full ratio in every selected cell; +* one local actual/full ratio in every selected cell; * one global falling-factorial loss, paid only once. This module packages their finite multiplication. It deliberately contains no @@ -28,19 +28,19 @@ set_option autoImplicit false The conclusion keeps the local and global charges visibly separate. -/ theorem finiteProduct_mul_global_le {Cell : Type*} [Fintype Cell] - (partial full localCharge : Cell → ENNReal) - (partialGlobal fullGlobal globalCharge : ENNReal) - (hlocal : ∀ c, partial c ≤ full c * localCharge c) - (hglobal : partialGlobal ≤ fullGlobal * globalCharge) : - (∏ c, partial c) * partialGlobal ≤ + (actual full localCharge : Cell → ENNReal) + (actualGlobal fullGlobal globalCharge : ENNReal) + (hlocal : ∀ c, actual c ≤ full c * localCharge c) + (hglobal : actualGlobal ≤ fullGlobal * globalCharge) : + (∏ c, actual c) * actualGlobal ≤ ((∏ c, full c) * fullGlobal) * (globalCharge * ∏ c, localCharge c) := by - have hprod : (∏ c, partial c) ≤ ∏ c, full c * localCharge c := by + have hprod : (∏ c, actual c) ≤ ∏ c, full c * localCharge c := by apply Finset.prod_le_prod' intro c _ exact hlocal c calc - (∏ c, partial c) * partialGlobal ≤ + (∏ c, actual c) * actualGlobal ≤ (∏ c, full c * localCharge c) * (fullGlobal * globalCharge) := mul_le_mul' hprod hglobal @@ -54,17 +54,17 @@ sum of the cell deficits. The global power is then absorbed into the local charged factors `base^(deficit c) * localRatio c` exactly once. -/ theorem finiteProduct_mul_globalPower_le_chargedProduct {Cell : Type*} [Fintype Cell] - (partial full localRatio : Cell → ENNReal) + (actual full localRatio : Cell → ENNReal) (deficit : Cell → Nat) - (partialGlobal fullGlobal base : ENNReal) - (hlocal : ∀ c, partial c ≤ full c * localRatio c) - (hglobal : partialGlobal ≤ + (actualGlobal fullGlobal base : ENNReal) + (hlocal : ∀ c, actual c ≤ full c * localRatio c) + (hglobal : actualGlobal ≤ fullGlobal * base ^ (∑ c, deficit c)) : - (∏ c, partial c) * partialGlobal ≤ + (∏ c, actual c) * actualGlobal ≤ ((∏ c, full c) * fullGlobal) * ∏ c, (base ^ deficit c * localRatio c) := by have h := finiteProduct_mul_global_le - partial full localRatio partialGlobal fullGlobal + actual full localRatio actualGlobal fullGlobal (base ^ (∑ c, deficit c)) hlocal hglobal have hcharge : base ^ (∑ c, deficit c) * (∏ c, localRatio c) = @@ -82,50 +82,50 @@ theorem inv_descFactorial_sub_le_inv_mul_pow (((n.descFactorial (J - H) : Nat) : ENNReal)⁻¹) ≤ (((n.descFactorial J : Nat) : ENNReal)⁻¹) * (n : ENNReal) ^ H := by - let full : ENNReal := ((n.descFactorial J : Nat) : ENNReal) - let small : ENNReal := ((n.descFactorial (J - H) : Nat) : ENNReal) - have hfull0 : full ≠ 0 := by - dsimp [full] + let fullDenom : ENNReal := ((n.descFactorial J : Nat) : ENNReal) + let smallDenom : ENNReal := ((n.descFactorial (J - H) : Nat) : ENNReal) + have hfull0 : fullDenom ≠ 0 := by + dsimp [fullDenom] exact_mod_cast (Nat.ne_of_gt (Nat.descFactorial_pos.mpr hJ : 0 < n.descFactorial J)) - have hfullTop : full ≠ ∞ := by - dsimp [full] + have hfullTop : fullDenom ≠ ∞ := by + dsimp [fullDenom] exact ENNReal.natCast_ne_top _ have hloss : denominatorLoss n J H ≤ (n : ENNReal) ^ H := (denominatorLoss_eq_falling_and_le_pow n J H hH hJ).2 - have hinv : small⁻¹ = full⁻¹ * denominatorLoss n J H := by + have hinv : smallDenom⁻¹ = fullDenom⁻¹ * denominatorLoss n J H := by unfold denominatorLoss - change small⁻¹ = full⁻¹ * (full / small) + change smallDenom⁻¹ = fullDenom⁻¹ * (fullDenom / smallDenom) rw [ENNReal.div_eq_inv_mul] calc - small⁻¹ = small⁻¹ * (full⁻¹ * full) := by + smallDenom⁻¹ = smallDenom⁻¹ * (fullDenom⁻¹ * fullDenom) := by rw [ENNReal.inv_mul_cancel hfull0 hfullTop, mul_one] - _ = full⁻¹ * (small⁻¹ * full) := by ac_rfl + _ = fullDenom⁻¹ * (smallDenom⁻¹ * fullDenom) := by ac_rfl rw [hinv] - simpa [mul_comm] using (mul_le_mul_right hloss full⁻¹) + simpa [mul_comm] using (mul_le_mul_right hloss fullDenom⁻¹) /-- Exact aggregate endpoint for the denominator bookkeeping. If each local -partial factor is bounded by its full factor times a literal local ratio, then -the aggregate partial weight with denominator `(n)_(J-H)` is bounded by the +actual factor is bounded by its full factor times a literal local ratio, then +the aggregate actual weight with denominator `(n)_(J-H)` is bounded by the full aggregate weight with denominator `(n)_J`, multiplied by the charged local factors `n^(h_e) * localRatio_e`. The global falling-factorial comparison is invoked only once. -/ theorem finiteProduct_mul_inv_descFactorial_sub_le_chargedProduct {Cell : Type*} [Fintype Cell] - (partial full localRatio : Cell → ENNReal) + (actual full localRatio : Cell → ENNReal) (deficit : Cell → Nat) (n J : Nat) (hdeficit : (∑ c, deficit c) ≤ J) (hJ : J ≤ n) - (hlocal : ∀ c, partial c ≤ full c * localRatio c) : - (∏ c, partial c) * + (hlocal : ∀ c, actual c ≤ full c * localRatio c) : + (∏ c, actual c) * (((n.descFactorial (J - ∑ c, deficit c) : Nat) : ENNReal)⁻¹) ≤ ((∏ c, full c) * (((n.descFactorial J : Nat) : ENNReal)⁻¹)) * ∏ c, ((n : ENNReal) ^ deficit c * localRatio c) := by apply finiteProduct_mul_globalPower_le_chargedProduct - partial full localRatio deficit + actual full localRatio deficit (((n.descFactorial (J - ∑ c, deficit c) : Nat) : ENNReal)⁻¹) (((n.descFactorial J : Nat) : ENNReal)⁻¹) (n : ENNReal) hlocal From c972f6ce61dc121fb64049952e7eaa23d5206f80 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:26:08 +0300 Subject: [PATCH 31/59] Rewrite optional choices to the exact local product before charging --- .../Section8CoarseHalfDeficitCharge.lean | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean b/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean index af9b36c4..7244757f 100644 --- a/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean +++ b/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean @@ -160,8 +160,12 @@ theorem sum_fourEndpointHalfDeficitChoiceWeight_le_uniform (card_fourEndpointHalfDeficitAllowed_le alpha hAlpha P) (by intro cell deficit hdeficit - simpa only [fourEndpointHalfDeficitAllowed, Finset.mem_filter, - Finset.mem_univ, true_and] using hdeficit |>.1) + have hmem : 0 < deficit.1 ∧ + 2 * deficit.1 < + fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1 := by + simpa only [fourEndpointHalfDeficitAllowed, Finset.mem_filter, + Finset.mem_univ, true_and] using hdeficit + exact hmem.1) (by intro cell deficit hdeficit exact (fourEndpointHalfDeficitWeight_le_threeQuarterBase_pow_of_mem @@ -209,10 +213,12 @@ theorem sum_profileCanonicalHighSkeleton_le_uniformHalfDeficitSupportSum (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ P.edges.card := by apply Finset.sum_le_sum intro P _ + have hchoice := + sum_fourEndpointHalfDeficitChoiceWeight_le_uniform + n alpha hAlpha P rho hrho (hbase P) + rw [sum_nearSkeletonChoiceWeight_eq_product] at hchoice simpa [mul_comm] using - (mul_le_mul_right - (sum_fourEndpointHalfDeficitChoiceWeight_le_uniform - n alpha hAlpha P rho hrho (hbase P)) (reference P)) + (mul_le_mul_right hchoice (reference P)) #print axioms nearCellTerm_le_threeQuarterCellBase_pow #print axioms sum_fourEndpointHalfDeficitChoiceWeight_le_uniform From b5cba465f37b250637a8b9b06263a8b4f222ab00 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:40:07 +0300 Subject: [PATCH 32/59] Make attained table grouping finite and lightweight --- .../Section8DirectReferenceGrouping.lean | 27 +++++++++++-------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean index 3239dc17..9547f4e4 100644 --- a/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean +++ b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean @@ -29,6 +29,8 @@ noncomputable section set_option autoImplicit false +local instance : DecidableEq FourEndpointFullTable := Classical.decEq _ + /-- The endpoint table carried by one abstract block support. -/ def fourEndpointSupportTable (alpha : Nat) (hAlpha : 5 < alpha) @@ -67,9 +69,8 @@ abbrev FourEndpointAllDecoratedSupport /-- The finite image of the block-support space in the endpoint-table space. -/ noncomputable def fourEndpointAttainedFullTables (alpha : Nat) (hAlpha : 5 < alpha) - (k : ColoringProfile (alpha + 1)) : Finset FourEndpointFullTable := by - classical - exact Finset.univ.image + (k : ColoringProfile (alpha + 1)) : Finset FourEndpointFullTable := + Finset.univ.image (fun P : FourEndpointAbstractBlockSkeleton alpha hAlpha k => fourEndpointSupportTable alpha hAlpha P) @@ -130,6 +131,10 @@ theorem sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W fourEndpointW n alpha hAlpha k L.1 := by let equivalence := fourEndpointAllDecoratedSupportEquivSigmaTable alpha hAlpha k + let targetWeight : + (Σ L : FourEndpointAttainedFullTable alpha hAlpha k, + FourEndpointDecoratedBlockPairing alpha hAlpha k L.1) → ENNReal := + fun z => fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha z.1.1 calc (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, fourEndpointFullSupportReferenceWeight n alpha hAlpha P) = @@ -137,20 +142,20 @@ theorem sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W fourEndpointFullSupportAtomWeight n alpha hAlpha z.1 := by rw [Fintype.sum_sigma] rfl + _ = ∑ z : FourEndpointAllDecoratedSupport alpha hAlpha k, + targetWeight (equivalence z) := by + apply Finset.sum_congr rfl + intro z _ + rfl _ = ∑ z : Σ L : FourEndpointAttainedFullTable alpha hAlpha k, FourEndpointDecoratedBlockPairing alpha hAlpha k L.1, - fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha z.1.1 := by - simpa [equivalence, fourEndpointFullSupportAtomWeight, - fourEndpointAllDecoratedSupportEquivSigmaTable] using - equivalence.sum_comp - (fun z : Σ L : FourEndpointAttainedFullTable alpha hAlpha k, - FourEndpointDecoratedBlockPairing alpha hAlpha k L.1 => - fourEndpointDecoratedReferenceAtomWeight - n alpha hAlpha z.1.1) + targetWeight z := + equivalence.sum_comp targetWeight _ = ∑ L : FourEndpointAttainedFullTable alpha hAlpha k, ∑ _ : FourEndpointDecoratedBlockPairing alpha hAlpha k L.1, fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L.1 := by rw [Fintype.sum_sigma] + rfl _ = ∑ L : FourEndpointAttainedFullTable alpha hAlpha k, fourEndpointW n alpha hAlpha k L.1 := by apply Finset.sum_congr rfl From 2f798108ee003722a501a1d1a01042b0b42bde0c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:51:48 +0300 Subject: [PATCH 33/59] Remove redundant closure after finite sigma expansion --- 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean index 9547f4e4..617f7d38 100644 --- a/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean +++ b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean @@ -155,7 +155,6 @@ theorem sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W ∑ _ : FourEndpointDecoratedBlockPairing alpha hAlpha k L.1, fourEndpointDecoratedReferenceAtomWeight n alpha hAlpha L.1 := by rw [Fintype.sum_sigma] - rfl _ = ∑ L : FourEndpointAttainedFullTable alpha hAlpha k, fourEndpointW n alpha hAlpha k L.1 := by apply Finset.sum_congr rfl From 34aabc0f0308ca2f76762ca418bb1f7ffedebf1a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:57:28 +0300 Subject: [PATCH 34/59] Reduce the phase estimate to a coarse five-halves corridor --- .../Erdos625/Section8CoarsePhaseCorridor.lean | 170 ++++++++++++++++++ 1 file changed, 170 insertions(+) create mode 100644 625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean diff --git a/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean b/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean new file mode 100644 index 00000000..257d69ed --- /dev/null +++ b/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean @@ -0,0 +1,170 @@ +import Erdos625.PhaseEstimates +import Erdos625.Section8CanonicalThreeQuarterRho +import Mathlib.Tactic + +/-! +# Section VIII: coarse phase corridor for the three-quarter deficit charge + +The sharp local estimate in the manuscript is stronger than the second moment +needs. The phase satisfies + +`phaseNat n ~ (2 / log 2) * log n`, + +and `2 / log 2 > 5/2`. Thus it is eventually enough to use the coarse corridor + +`(5/2) log n <= phaseNat n`. + +Every four-endpoint overlap size is at least `alpha-5`. Combined with the +three-quarter integer budget and the elementary lower bound `log 2 > 2/3`, this +gives + +`(5/4) log n - 19/6 <= log 2 * floor((3m-1)/4)`. + +Hence the denominator in the local charge already gains a factor of order +`n^(5/4)`, so the local base has the much coarser but still sufficient scale +`O(log n / n^(1/4))`. This module proves the corridor and the finite logarithmic +budget; it deliberately leaves the final exponential conversion separate. +-/ + +namespace Erdos625 + +open Filter Asymptotics Set +open scoped Topology BigOperators + +noncomputable section + +set_option autoImplicit false + +/-- A coarse lower phase corridor. The constant `5/2` is chosen below the +limit `2/log 2` and is more than sufficient for the deficit product. -/ +theorem eventually_five_halves_logOrder_le_phaseNat : + ∀ᶠ n : Nat in atTop, + (5 / 2 : Real) * logOrder n ≤ (phaseNat n : Real) := by + have hDenom : ∀ᶠ n : Nat in atTop, + (2 / q) * logOrder n ≠ 0 := by + filter_upwards [eventually_gt_atTop (1 : Nat)] with n hn + have hlog : 0 < logOrder n := Real.log_pos (by exact_mod_cast hn) + exact mul_ne_zero (div_ne_zero (by norm_num) q_ne_zero) hlog.ne' + have hRatioOne : Tendsto + ((fun n : Nat => (phaseNat n : Real)) / + (fun n : Nat => (2 / q) * logOrder n)) atTop (nhds 1) := + (isEquivalent_iff_tendsto_one hDenom).mp + phaseNat_isEquivalent_scaled_logOrder + have hRatio : Tendsto + (fun n : Nat => (phaseNat n : Real) / logOrder n) + atTop (nhds (2 / q)) := by + have hScaled := hRatioOne.const_mul (2 / q) + convert hScaled using 1 + · funext n + by_cases hlog : logOrder n = 0 + · simp [hlog] + · change (phaseNat n : Real) / logOrder n = + (2 / q) * ((phaseNat n : Real) / ((2 / q) * logOrder n)) + field_simp [q_ne_zero] + · simp + have hqUpper : q < (4 / 5 : Real) := by + exact Real.log_two_lt_d9.trans (by norm_num) + have hqLower : (1 / 2 : Real) < q := by + exact (by norm_num : (1 / 2 : Real) < 0.6931471803).trans + Real.log_two_gt_d9 + have hLimitLower : (5 / 2 : Real) < 2 / q := by + rw [lt_div_iff₀ q_pos] + nlinarith + have hLimitUpper : 2 / q < (4 : Real) := by + rw [div_lt_iff₀ q_pos] + nlinarith + have hEventuallyRatio : ∀ᶠ n : Nat in atTop, + (phaseNat n : Real) / logOrder n ∈ Set.Icc (5 / 2 : Real) 4 := + hRatio.eventually (Icc_mem_nhds hLimitLower hLimitUpper) + have hLogPos : ∀ᶠ n : Nat in atTop, 0 < logOrder n := by + filter_upwards [eventually_gt_atTop (1 : Nat)] with n hn + exact Real.log_pos (by exact_mod_cast hn) + filter_upwards [hEventuallyRatio, hLogPos] with n hnRatio hnLog + exact (le_div_iff₀ hnLog).mp hnRatio.1 + +/-- The phase eventually exceeds the finite threshold needed to cast all +truncated natural-number subtractions as ordinary real subtractions. -/ +theorem eventually_eight_lt_phaseNat : + ∀ᶠ n : Nat in atTop, 8 < phaseNat n := by + have hLog : ∀ᶠ n : Nat in atTop, (8 : Real) < logOrder n := + tendsto_logOrder_atTop.eventually (eventually_gt_atTop 8) + filter_upwards + [hLog, eventually_logOrder_le_phaseNat_and_phaseNat_le_four_logOrder] + with n hnLog hnPhase + exact_mod_cast (hnLog.trans_le hnPhase.1) + +/-- Every four-endpoint overlap size is at least the smallest endpoint size +`alpha-5`. -/ +theorem alpha_sub_five_le_fourEndpointOverlapSize + (alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) : + alpha - 5 ≤ fourEndpointOverlapSize alpha hAlpha i j := by + fin_cases i <;> fin_cases j <;> + simp [fourEndpointOverlapSize, fourEndpointSize, + fourEndpointCoordinate, fourDeficitCoordinate, fourDeficit] <;> omega + +/-- Division-free floor estimate for the three-quarter exponent. -/ +theorem three_mul_alpha_sub_nineteen_le_four_mul_threeQuarterBudget + (alpha m : Nat) (hm : alpha - 5 ≤ m) : + 3 * alpha - 19 ≤ 4 * ((3 * m - 1) / 4) := by + omega + +/-- Four-endpoint specialization of the preceding floor estimate. -/ +theorem three_mul_alpha_sub_nineteen_le_four_mul_endpointBudget + (alpha : Nat) (hAlpha : 5 < alpha) (i j : Fin 4) : + 3 * alpha - 19 ≤ + 4 * ((3 * fourEndpointOverlapSize alpha hAlpha i j - 1) / 4) := by + exact three_mul_alpha_sub_nineteen_le_four_mul_threeQuarterBudget + alpha (fourEndpointOverlapSize alpha hAlpha i j) + (alpha_sub_five_le_fourEndpointOverlapSize alpha hAlpha i j) + +/-- Coarse real logarithmic budget. It uses only `log 2 > 2/3`, the +five-halves phase corridor, and the finite endpoint floor estimate. -/ +theorem five_fourths_log_sub_le_q_mul_endpointBudget + (n alpha : Nat) (hAlpha : 5 < alpha) (hHigh : 8 < alpha) + (hphase : (5 / 2 : Real) * logOrder n ≤ (alpha : Real)) + (i j : Fin 4) : + (5 / 4 : Real) * logOrder n - 19 / 6 ≤ + q * (((3 * fourEndpointOverlapSize alpha hAlpha i j - 1) / 4 : Nat) : Real) := by + let budget : Nat := + (3 * fourEndpointOverlapSize alpha hAlpha i j - 1) / 4 + have hnat : 3 * alpha - 19 ≤ 4 * budget := by + exact three_mul_alpha_sub_nineteen_le_four_mul_endpointBudget + alpha hAlpha i j + have h19 : 19 ≤ 3 * alpha := by omega + have hcast : 3 * (alpha : Real) - 19 ≤ 4 * (budget : Real) := by + have hcastNat := congrArg (fun x : Nat => (x : Real)) hnat + rw [Nat.cast_sub h19] at hcastNat + norm_num at hcastNat ⊢ + exact hcastNat + have hq : (2 / 3 : Real) ≤ q := by + exact ((by norm_num : (2 / 3 : Real) < 0.6931471803).trans + Real.log_two_gt_d9).le + have hbudgetNonneg : 0 ≤ (budget : Real) := by positivity + have hqmul : (2 / 3 : Real) * (budget : Real) ≤ q * (budget : Real) := + mul_le_mul_of_nonneg_right hq hbudgetNonneg + dsimp only [budget] + nlinarith + +/-- Eventual form simultaneously valid for all sixteen endpoint types. -/ +theorem eventually_five_fourths_log_sub_le_q_mul_endpointBudget : + ∀ᶠ n : Nat in atTop, + ∀ i j : Fin 4, + (5 / 4 : Real) * logOrder n - 19 / 6 ≤ + q * (((3 * fourEndpointOverlapSize (phaseNat n) + (by omega : 5 < phaseNat n) i j - 1) / 4 : Nat) : Real) := by + filter_upwards + [eventually_five_halves_logOrder_le_phaseNat, + eventually_eight_lt_phaseNat] + with n hphase hHigh + intro i j + exact five_fourths_log_sub_le_q_mul_endpointBudget + n (phaseNat n) (by omega) hHigh hphase i j + +#print axioms eventually_five_halves_logOrder_le_phaseNat +#print axioms alpha_sub_five_le_fourEndpointOverlapSize +#print axioms three_mul_alpha_sub_nineteen_le_four_mul_endpointBudget +#print axioms five_fourths_log_sub_le_q_mul_endpointBudget + +end + +end Erdos625 From 7fb99bcbf1e5c290dd1a49618ee5f61af1faae1c Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 12:58:28 +0300 Subject: [PATCH 35/59] Build the coarse phase corridor with Section VIII reductions --- .github/workflows/erdos625-direct-half-deficit-assembly.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index b6aadcfc..0a6e9dfb 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -8,6 +8,7 @@ on: - "625/formalization/Erdos625/Section8PointwiseChargeProduct.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean" + - "625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean" - "625/formalization/Erdos625/Section8DirectReferenceGrouping.lean" - "625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean" - "625/experiments/section8_direct_half_deficit_assembly.py" @@ -48,6 +49,7 @@ jobs: 625/formalization/Erdos625/Section8PointwiseChargeProduct.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ 625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean \ + 625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean \ 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean \ 625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean; then exit 1 @@ -68,6 +70,7 @@ jobs: for target in \ Erdos625.Section8PointwiseChargeProduct \ Erdos625.Section8CanonicalThreeQuarterRho \ + Erdos625.Section8CoarsePhaseCorridor \ Erdos625.Section8FiniteBareSkeletonReduction; do echo "=== $target ===" | tee -a /tmp/erdos625-direct-half-deficit.log set +e From f84197999ad5a226fba20b693414aff395997a8d Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 13:01:37 +0300 Subject: [PATCH 36/59] Make the eventual endpoint budget proof argument explicit --- .../Erdos625/Section8CoarsePhaseCorridor.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean b/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean index 257d69ed..ae7b7210 100644 --- a/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean +++ b/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean @@ -145,20 +145,22 @@ theorem five_fourths_log_sub_le_q_mul_endpointBudget dsimp only [budget] nlinarith -/-- Eventual form simultaneously valid for all sixteen endpoint types. -/ +/-- Eventual form simultaneously valid for all sixteen endpoint types. The +finite proof argument `hAlpha` is explicit so no theorem statement depends on a +hidden tactic-generated proof. -/ theorem eventually_five_fourths_log_sub_le_q_mul_endpointBudget : ∀ᶠ n : Nat in atTop, - ∀ i j : Fin 4, + ∀ (hAlpha : 5 < phaseNat n) (i j : Fin 4), (5 / 4 : Real) * logOrder n - 19 / 6 ≤ q * (((3 * fourEndpointOverlapSize (phaseNat n) - (by omega : 5 < phaseNat n) i j - 1) / 4 : Nat) : Real) := by + hAlpha i j - 1) / 4 : Nat) : Real) := by filter_upwards [eventually_five_halves_logOrder_le_phaseNat, eventually_eight_lt_phaseNat] with n hphase hHigh - intro i j + intro hAlpha i j exact five_fourths_log_sub_le_q_mul_endpointBudget - n (phaseNat n) (by omega) hHigh hphase i j + n (phaseNat n) hAlpha hHigh hphase i j #print axioms eventually_five_halves_logOrder_le_phaseNat #print axioms alpha_sub_five_le_fourEndpointOverlapSize From 2b3b112f290ef9372852a10fbdd706d12edba5f2 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 13:04:00 +0300 Subject: [PATCH 37/59] Document the one-global-loss and coarse phase reductions --- ...ION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md | 199 ++++++++++++++---- 1 file changed, 156 insertions(+), 43 deletions(-) diff --git a/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md b/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md index daa073a8..75cc8b0d 100644 --- a/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md +++ b/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md @@ -50,12 +50,12 @@ still gives a subcritical exponent. Thus the finite proof can use the existing cardinality interface instead of proving an exact finite geometric sum. Finally, the zero-deficit reference is defined literally as the sum over full -stub decorations of one block support. The total decorated-support space is -then tautologically equivalent to the dependent sum over endpoint tables of -the existing `FourEndpointDecoratedBlockPairing` fibres. This makes +stub decorations of one block support. The ambient type of all natural-valued +four-by-four tables is infinite, so the correct table index is the finite image +of the block-support space. Grouping over that attained table type makes ```text -sum_P reference(P) = sum_L W(L) +sum_P reference(P) = sum_(attained L) W(L) ``` a finite reindexing theorem rather than another factorial calculation. @@ -86,9 +86,9 @@ j_e = m_e if omega(e)=none, j_e = m_e-h_e if omega(e)=some h_e. ``` -The attained-demand encoding from PR #48 maps into this type by sending zero -deficit to `none`. The decoded table is unchanged, so injectivity follows from -the already checked injectivity of the abstract demand table. +The attained-demand encoding maps into this type by sending zero deficit to +`none`. The decoded table is unchanged, so injectivity follows from the already +checked injectivity of the abstract demand table. ## 3. Exact finite summation @@ -124,7 +124,39 @@ entire attained family. There is no extra factor for: - a choice of physical full completion; - conversion between two deficit representations. -## 4. Coarse local charge +## 4. Pay the global denominator only once + +The ambient falling-factorial normalization is global. It must not be split +among the cells before the exact aggregate identity is established. + +If the full support carries total multiplicity `J` and the total deficit is +`H`, the exact denominator comparison is + +```text +1/(n)_(J-H) <= n^H/(n)_J. +``` + +The generic product module now proves the following interface. If every local +actual factor satisfies + +```text +actual_e <= full_e * localRatio_e, +``` + +then + +```text +[product_e actual_e] / (n)_(J-H) +<= +[product_e full_e] / (n)_J + * product_e [n^(h_e) * localRatio_e]. +``` + +Thus the single global loss `n^H` is absorbed into the local charged terms only +after it has been paid once. This is the exact logical order needed in the +pointwise charged comparison. + +## 5. Coarse local charge Define @@ -142,43 +174,57 @@ nearCellTerm(n,m,d,h) <= rho(n,m)^h. The bound is independent of the endpoint distance `d`. -If a common `rho` dominates the sixteen endpoint-type bases and `rho<=1`, then -one support contributes at most +There are only sixteen endpoint types. Define the canonical common base ```text -(1 + (alpha+1)*rho)^|P|. +rho_16(n,alpha) + = sum_(i,j in Fin 4) rho(n,m_ij). +``` + +Every selected cell base is automatically at most `rho_16`, so no +support-dependent domination premise remains. If `rho_16<=1`, one support +contributes at most + +```text +(1 + (alpha+1)*rho_16)^|P|. ``` This is intentionally weaker than the sharp geometric estimate -`(1+2rho)^|P|`, but it is easier to formalize and is still far below the target +`(1+2rho)^|P|`, but it is easier to formalize and remains far below the target scale. -## 5. Direct reference grouping +## 6. Direct reference grouping For one abstract support `P`, let `R(P)` be the literal sum of the common full-containment atom over every independent full stub matching in each -selected cell. Then +selected cell. + +The finite endpoint-table type is ```text -Sigma P, full decorations on P +image( + FourEndpointAbstractBlockSkeleton, + P |-> supportTable(P)). ``` -is equivalent to +The total decorated-support space is equivalent to ```text -Sigma L, FourEndpointDecoratedBlockPairing(alpha,hAlpha,k,L). +Sigma L : attained endpoint table, + FourEndpointDecoratedBlockPairing(alpha,hAlpha,k,L). ``` The existing exact normalization theorem on each endpoint table therefore gives ```text -sum_P R(P) = sum_L W(L). +sum_P R(P) = sum_(attained L) W(L). ``` -No new cell factorial or block-pairing cardinality formula is required. +No new cell factorial or block-pairing cardinality formula is required, and no +sum over the infinite type `Nat^(4x4)` is introduced. -## 6. Common support-card bound +## 7. Common support-card bound A block support is itself a partial matching of row block slots to column block slots. Projection to the row slot is injective, hence @@ -188,20 +234,85 @@ slots. Projection to the row slot is injective, hence ``` Thus every support may be charged by the same power. Combining direct deficit -summation, the coarse local charge, the support-card bound, and direct reference -grouping gives the finite reduction +summation, the canonical common base, the support-card bound, and direct +reference grouping gives the finite reduction ```text sum_(attained demands) weight(demand) <= -(sum_L W(L)) - * (1 + (alpha+1)*rho)^(total block count), +(sum_(attained L) W(L)) + * (1 + (alpha+1)*rho_16)^(total block count), ``` provided only that each individual attained weight satisfies the pointwise charged comparison. -## 7. Why this route is easier to formalize +## 8. A coarser phase estimate is enough + +The sharp estimate + +```text +rho_16 = O((log n)^(5/2)/sqrt n) +``` + +is not needed to close the second moment. + +The phase satisfies + +```text +phaseNat(n) ~ (2/log 2) log n, +``` + +and `2/log 2 > 5/2`. Hence eventually + +```text +(5/2) log n <= phaseNat(n). +``` + +Every endpoint overlap size obeys + +```text +m_ij >= alpha-5, +``` + +and the finite floor arithmetic gives + +```text +3*alpha-19 <= 4*floor((3*m_ij-1)/4). +``` + +Using only `log 2 > 2/3`, the resulting logarithmic denominator budget is + +```text +(5/4) log n - 19/6 + <= +(log 2) * floor((3*m_ij-1)/4). +``` + +After exponentiation this yields the much coarser bound + +```text +rho(n,m_ij) = O(log n / n^(1/4)). +``` + +Even after paying `alpha+1=O(log n)` and a support size of order `n/log n`, the +logarithm of the global deficit factor is only + +```text +O(n^(3/4) log n), +``` + +which is still + +```text +o(n/(log n)^4). +``` + +Thus the phase formalization no longer needs the sharp square-root-scale local +asymptotic. It only needs an elementary exponential conversion from the checked +five-fourths logarithmic budget. + +## 9. Why this route is easier to formalize Compared with the old near/middle proof and the first all-deficit plan, the new route removes: @@ -209,10 +320,12 @@ route removes: 1. the middle regime entirely; 2. `allHighDeficitCut` from the global analytic assembly; 3. repeated reconstruction of the global cutoff `U/2`; -4. a conversion between two dependent deficit structures after summation; +4. conversion between two dependent deficit structures after summation; 5. a finite geometric-series theorem; 6. a second endpoint-table cardinality proof; -7. support-dependent exponents in the final table sum. +7. support-dependent exponents in the final table sum; +8. support-dependent local-base hypotheses; +9. the sharp phase estimate as a necessary prerequisite. The analytic assembly now uses only: @@ -220,12 +333,14 @@ The analytic assembly now uses only: - one coarse local base; - one trivial cardinality bound on deficits; - one trivial cardinality bound on support size; -- the already checked endpoint-table reference sum. +- the finite attained endpoint-table reference sum; +- the coarse corridor `(5/2)log n <= phaseNat(n)`. -## 8. Minimal remaining theorem +## 10. Minimal remaining theorem Once the finite modules on this branch are green, the only genuinely new -Section VIII algebraic theorem is the pointwise charged comparison +Section VIII algebraic theorem is the endpoint-specific pointwise charged +comparison ```text profileHighSkeletonWeight(demand) @@ -237,23 +352,21 @@ fullSupportReference(P) PR #53 supplies the exact aggregate formula on the left. The remaining proof has only two ingredients: -1. compare every partial local factor with its full local factor; -2. apply the single global falling-factorial loss once. +1. identify the exact partial/full local factorial-and-reward ratio; +2. invoke the now-checked single global falling-factorial loss once. After that theorem, the branch's finite reduction gives the complete -bare-skeleton sum in one line. The remaining work is then purely asymptotic: -prove the common cell base is at most - -```text -O((log n)^(5/2)/sqrt n) -``` +bare-skeleton sum in one line. The remaining asymptotic work is reduced to: -and apply endpoint transportation. +1. exponentiate the coarse endpoint budget; +2. bound the explicit sixteen-term `rho_16`; +3. apply the already checked endpoint transportation estimate. -## 9. Audit boundary +## 11. Audit boundary This simplification does not itself prove the bare-skeleton estimate. It removes data conversion, geometric-series bookkeeping, endpoint regrouping, -and support-card bookkeeping from the remaining proof. The theorem remains -conditional until the pointwise charged comparison and the phase -specialization are integrated and built on one branch. +support-card bookkeeping, and the sharp phase estimate from the necessary +proof path. The theorem remains conditional until the endpoint-specific +pointwise charged comparison and the coarse exponential conversion are +integrated and built on one branch. From 170d262cf8cc99a78ca792c8461492b75d2e42d4 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 22:32:09 +0300 Subject: [PATCH 38/59] Repair the coarse phase inequality cast and final arithmetic --- 625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean b/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean index ae7b7210..50f2b4c9 100644 --- a/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean +++ b/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean @@ -132,7 +132,9 @@ theorem five_fourths_log_sub_le_q_mul_endpointBudget alpha hAlpha i j have h19 : 19 ≤ 3 * alpha := by omega have hcast : 3 * (alpha : Real) - 19 ≤ 4 * (budget : Real) := by - have hcastNat := congrArg (fun x : Nat => (x : Real)) hnat + have hcastNat : + ((3 * alpha - 19 : Nat) : Real) ≤ ((4 * budget : Nat) : Real) := by + exact_mod_cast hnat rw [Nat.cast_sub h19] at hcastNat norm_num at hcastNat ⊢ exact hcastNat @@ -142,7 +144,7 @@ theorem five_fourths_log_sub_le_q_mul_endpointBudget have hbudgetNonneg : 0 ≤ (budget : Real) := by positivity have hqmul : (2 / 3 : Real) * (budget : Real) ≤ q * (budget : Real) := mul_le_mul_of_nonneg_right hq hbudgetNonneg - dsimp only [budget] + change (5 / 4 : Real) * logOrder n - 19 / 6 ≤ q * (budget : Real) nlinarith /-- Eventual form simultaneously valid for all sixteen endpoint types. The From 82cd96fce184e4a62ec603f239f49298ad8a2d15 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 22:45:29 +0300 Subject: [PATCH 39/59] Remove no-op simplification from the common support-card bound --- .../Section8FiniteBareSkeletonReduction.lean | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean index d8bc097d..f114d2e1 100644 --- a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean +++ b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean @@ -110,11 +110,10 @@ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W fourEndpointFullSupportReferenceWeight n alpha hAlpha P * common := by apply Finset.sum_le_sum intro P _ - simpa [mul_comm] using - (mul_le_mul_right - (pow_le_pow_right₀ (by simp [common]) - (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) - (fourEndpointFullSupportReferenceWeight n alpha hAlpha P)) + exact mul_le_mul_left + (pow_le_pow_right₀ (by simp [common]) + (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) + (fourEndpointFullSupportReferenceWeight n alpha hAlpha P) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, fourEndpointFullSupportReferenceWeight n alpha hAlpha P) * common := by rw [Finset.sum_mul] @@ -163,11 +162,10 @@ theorem sum_profileCanonicalHighSkeleton_le_canonicalDeficitFactor_mul_sum_W fourEndpointFullSupportReferenceWeight n alpha hAlpha P * common := by apply Finset.sum_le_sum intro P _ - simpa [mul_comm] using - (mul_le_mul_right - (pow_le_pow_right₀ (by simp [common]) - (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) - (fourEndpointFullSupportReferenceWeight n alpha hAlpha P)) + exact mul_le_mul_left + (pow_le_pow_right₀ (by simp [common]) + (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) + (fourEndpointFullSupportReferenceWeight n alpha hAlpha P) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, fourEndpointFullSupportReferenceWeight n alpha hAlpha P) * common := by rw [Finset.sum_mul] From 8ae5ffbe5f48b817d327b60bdb57b45adf00dfd8 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 22:55:08 +0300 Subject: [PATCH 40/59] Use the exact ENNReal bottom proof in the support power bound --- .../Erdos625/Section8FiniteBareSkeletonReduction.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean index f114d2e1..48e34b37 100644 --- a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean +++ b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean @@ -111,7 +111,7 @@ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W apply Finset.sum_le_sum intro P _ exact mul_le_mul_left - (pow_le_pow_right₀ (by simp [common]) + (pow_le_pow_right₀ bot_le (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) (fourEndpointFullSupportReferenceWeight n alpha hAlpha P) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, @@ -163,7 +163,7 @@ theorem sum_profileCanonicalHighSkeleton_le_canonicalDeficitFactor_mul_sum_W apply Finset.sum_le_sum intro P _ exact mul_le_mul_left - (pow_le_pow_right₀ (by simp [common]) + (pow_le_pow_right₀ bot_le (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) (fourEndpointFullSupportReferenceWeight n alpha hAlpha P) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, From 965082dee37921ac7da7294d8e3e6703a8ef1ed2 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 22:59:16 +0300 Subject: [PATCH 41/59] Add the exact one-cell partial/full deficit identity --- .../Section8ExactLocalDeficitRatio.lean | 216 ++++++++++++++++++ 1 file changed, 216 insertions(+) create mode 100644 625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean new file mode 100644 index 00000000..a04b1c2d --- /dev/null +++ b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean @@ -0,0 +1,216 @@ +import Erdos625.Section8EndpointSingleCellStubs +import Erdos625.Section8NearCellChoiceLink +import Erdos625.LocalSignReward +import Mathlib.Tactic + +/-! +# Section VIII: exact one-cell partial/full deficit identity + +For endpoint sizes `m` and `m+d`, compare a partial cell of multiplicity +`m-h` with the full-containment cell of multiplicity `m`. + +The physical matching-count ratio is + +`choose(m,h) / ((d+1) ... (d+h))`, + +and the signed local-reward ratio is + +`2^(-h*m + h*(h+1)/2)`. + +This file proves the corresponding division-free identity over natural +numbers. It is the exact local algebra needed before the single global +falling-factorial loss is applied. No phase estimate or summation over cells +is used here. +-/ + +namespace Erdos625 + +open scoped BigOperators + +noncomputable section + +set_option autoImplicit false + +/-- Number of literal partial stub matchings in a cell with endpoint sizes +`m` and `m+d` and prescribed multiplicity `j`. -/ +def lowerUpperCellMatchingCount (m d j : Nat) : Nat := + Fintype.card (SingleCellStubMatching m (m + d) j) + +/-- Physical matching count multiplied by the local signed reward. -/ +def lowerUpperCellWeightedCount (m d j : Nat) : Nat := + lowerUpperCellMatchingCount m d j * localSignRewardNat j + +/-- The consecutive product `(d+1) ... (d+h)` used by the deficit ratio. -/ +def endpointDeficitDenominator (d h : Nat) : Nat := + ∏ t ∈ Finset.Icc 1 h, d + t + +/-- Multiplying the consecutive endpoint-distance factors by `d!` gives the +factorial at the upper endpoint. -/ +theorem factorial_mul_endpointDeficitDenominator + (d h : Nat) : + d.factorial * endpointDeficitDenominator d h = (d + h).factorial := by + induction h with + | zero => simp [endpointDeficitDenominator] + | succ h ih => + rw [endpointDeficitDenominator, + Finset.prod_Icc_succ_top (by omega : 1 ≤ h + 1)] + rw [← endpointDeficitDenominator, Nat.factorial_succ] + calc + d.factorial * + (endpointDeficitDenominator d h * (d + (h + 1))) = + (d.factorial * endpointDeficitDenominator d h) * (d + h + 1) := by + ring + _ = (d + h).factorial * (d + h + 1) := by rw [ih] + _ = (d + h + 1).factorial := by + rw [Nat.factorial_succ] + +/-- The consecutive endpoint-distance product is a descending factorial. -/ +theorem endpointDeficitDenominator_eq_descFactorial + (d h : Nat) : + endpointDeficitDenominator d h = (d + h).descFactorial h := by + have hleft := factorial_mul_endpointDeficitDenominator d h + have hright : + d.factorial * (d + h).descFactorial h = (d + h).factorial := by + simpa using + (Nat.factorial_mul_descFactorial (show h ≤ d + h by omega)) + exact Nat.mul_left_cancel (hleft.trans hright.symm) + +/-- Closed form for a one-cell matching count when the smaller endpoint is +`m`. -/ +theorem lowerUpperCellMatchingCount_eq_choose_mul_descFactorial + (m d j : Nat) (hj : j ≤ m) : + lowerUpperCellMatchingCount m d j = + m.choose j * (m + d).descFactorial j := by + have hcard := card_singleCellStubMatching_mul_factorial m (m + d) j + have hlower : m.descFactorial j = j.factorial * m.choose j := + Nat.descFactorial_eq_factorial_mul_choose + rw [hlower] at hcard + have hmul : + lowerUpperCellMatchingCount m d j * j.factorial = + (m.choose j * (m + d).descFactorial j) * j.factorial := by + calc + lowerUpperCellMatchingCount m d j * j.factorial = + (j.factorial * m.choose j) * (m + d).descFactorial j := hcard + _ = (m.choose j * (m + d).descFactorial j) * j.factorial := by + ring + exact Nat.mul_right_cancel hmul + +/-- Splitting the upper-endpoint descending factorial at deficit `h`. -/ +theorem upperEndpoint_descFactorial_full_split + (m d h : Nat) (hh : h ≤ m) : + (m + d).descFactorial m = + (m + d).descFactorial (m - h) * (d + h).descFactorial h := by + have hgap : m + d - (m - h) = d + h := by omega + have hsum : (m - h) + h = m := Nat.sub_add_cancel hh + calc + (m + d).descFactorial m = + (m + d).descFactorial ((m - h) + h) := by rw [hsum] + _ = (m + d).descFactorial (m - h) * + (m + d - (m - h)).descFactorial h := by + rw [Nat.descFactorial_mul_descFactorial] + _ = (m + d).descFactorial (m - h) * + (d + h).descFactorial h := by rw [hgap] + +/-- Exact physical matching-count ratio in cross-multiplied form. -/ +theorem lowerUpperCellMatchingCount_deficit_cross_mul + (m d h : Nat) (hh : h ≤ m) : + lowerUpperCellMatchingCount m d (m - h) * + endpointDeficitDenominator d h = + lowerUpperCellMatchingCount m d m * m.choose h := by + rw [lowerUpperCellMatchingCount_eq_choose_mul_descFactorial + m d (m - h) (Nat.sub_le _ _), + lowerUpperCellMatchingCount_eq_choose_mul_descFactorial m d m le_rfl, + Nat.choose_self, one_mul, Nat.choose_symm hh, + endpointDeficitDenominator_eq_descFactorial] + rw [← upperEndpoint_descFactorial_full_split m d h hh] + ring + +/-- One-step identity for the quadratic binary exponent. -/ +theorem deficitBinaryExponent_succ + (m h : Nat) (hh : h + 1 ≤ m) : + (h + 1) * m - (h + 1) * (h + 1 + 1) / 2 = + h * m - h * (h + 1) / 2 + (m - (h + 1)) := by + rw [tsub_eq_of_eq_add] + zify [hh] + rw [Nat.cast_sub] <;> push_cast <;> + repeat nlinarith [Nat.div_mul_le_self (h * (h + 1)) 2] + grind + +/-- Removing one vertex from a high local reward costs exactly one binary +power. -/ +theorem localSignRewardNat_pred_mul_pow + (x : Nat) (hx : 4 ≤ x) : + localSignRewardNat (x - 1) * 2 ^ (x - 1) = + localSignRewardNat x := by + have hx3 : 3 ≤ x := by omega + have hpred3 : 3 ≤ x - 1 := by omega + have hchooseRec : + x.choose 2 = (x - 1).choose 2 + (x - 1) := by + have hxrec : x - 1 + 1 = x := by omega + conv_lhs => rw [← hxrec] + rw [Nat.choose_succ_succ] + simp only [Nat.choose_one_right] + omega + have hchoosePred : 1 ≤ (x - 1).choose 2 := by + have hmono := Nat.choose_le_choose 2 hpred3 + norm_num at hmono + omega + have hexponent : + ((x - 1).choose 2 - 1) + (x - 1) = x.choose 2 - 1 := by + omega + simp only [localSignRewardNat, if_pos hx3, if_pos hpred3] + rw [← pow_add, hexponent] + +/-- Exact local reward ratio across an arbitrary admissible deficit. -/ +theorem localSignRewardNat_deficit_mul_pow + (m h : Nat) (hh : h ≤ m) (hhigh : 3 ≤ m - h) : + localSignRewardNat (m - h) * + 2 ^ (h * m - h * (h + 1) / 2) = + localSignRewardNat m := by + induction h with + | zero => simp + | succ h ih => + have hhPrev : h ≤ m := by omega + have hhighPrev : 3 ≤ m - h := by omega + have hstepHigh : 4 ≤ m - h := by omega + have hstep := localSignRewardNat_pred_mul_pow (m - h) hstepHigh + have hpred : m - h - 1 = m - (h + 1) := by omega + rw [hpred] at hstep + have hexponent := deficitBinaryExponent_succ m h (by omega) + calc + localSignRewardNat (m - (h + 1)) * + 2 ^ ((h + 1) * m - (h + 1) * (h + 1 + 1) / 2) = + (localSignRewardNat (m - (h + 1)) * + 2 ^ (m - (h + 1))) * + 2 ^ (h * m - h * (h + 1) / 2) := by + rw [hexponent, pow_add] + ring + _ = localSignRewardNat (m - h) * + 2 ^ (h * m - h * (h + 1) / 2) := by rw [hstep] + _ = localSignRewardNat m := ih hhPrev hhighPrev + +/-- Exact one-cell partial/full comparison, with every denominator kept in +cross-multiplied form. -/ +theorem lowerUpperCellWeightedCount_deficit_cross_mul + (m d h : Nat) (hh : h ≤ m) (hhigh : 3 ≤ m - h) : + lowerUpperCellWeightedCount m d (m - h) * + endpointDeficitDenominator d h * + 2 ^ (h * m - h * (h + 1) / 2) = + lowerUpperCellWeightedCount m d m * m.choose h := by + unfold lowerUpperCellWeightedCount + rw [mul_assoc, + show lowerUpperCellMatchingCount m d (m - h) * + endpointDeficitDenominator d h = + lowerUpperCellMatchingCount m d m * m.choose h from + lowerUpperCellMatchingCount_deficit_cross_mul m d h hh, + localSignRewardNat_deficit_mul_pow m h hh hhigh] + ring + +#print axioms endpointDeficitDenominator_eq_descFactorial +#print axioms lowerUpperCellMatchingCount_deficit_cross_mul +#print axioms localSignRewardNat_deficit_mul_pow +#print axioms lowerUpperCellWeightedCount_deficit_cross_mul + +end + +end Erdos625 From 9341682d710fedba89ddb7abaab194117d8042a1 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:00:32 +0300 Subject: [PATCH 42/59] Build the exact one-cell deficit identity in focused CI --- .github/workflows/erdos625-direct-half-deficit-assembly.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index 0a6e9dfb..29170e69 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -6,6 +6,7 @@ on: - "625/formalization/Erdos625/Section8FourDeficitProfileCover.lean" - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" - "625/formalization/Erdos625/Section8PointwiseChargeProduct.lean" + - "625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean" - "625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean" @@ -47,6 +48,7 @@ jobs: 625/formalization/Erdos625/Section8FourDeficitProfileCover.lean \ 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ 625/formalization/Erdos625/Section8PointwiseChargeProduct.lean \ + 625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ 625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean \ 625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean \ @@ -69,6 +71,7 @@ jobs: : > /tmp/erdos625-direct-half-deficit.log for target in \ Erdos625.Section8PointwiseChargeProduct \ + Erdos625.Section8ExactLocalDeficitRatio \ Erdos625.Section8CanonicalThreeQuarterRho \ Erdos625.Section8CoarsePhaseCorridor \ Erdos625.Section8FiniteBareSkeletonReduction; do From 5aa49daeefb1f282e61538da5860fea6a268c3d6 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:07:59 +0300 Subject: [PATCH 43/59] Repair the exact one-cell deficit algebra --- .../Section8ExactLocalDeficitRatio.lean | 63 ++++++++++++------- 1 file changed, 39 insertions(+), 24 deletions(-) diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean index a04b1c2d..c29246de 100644 --- a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean +++ b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean @@ -42,7 +42,7 @@ def lowerUpperCellWeightedCount (m d j : Nat) : Nat := /-- The consecutive product `(d+1) ... (d+h)` used by the deficit ratio. -/ def endpointDeficitDenominator (d h : Nat) : Nat := - ∏ t ∈ Finset.Icc 1 h, d + t + Finset.prod (Finset.Icc 1 h) (fun t => d + t) /-- Multiplying the consecutive endpoint-distance factors by `d!` gives the factorial at the upper endpoint. -/ @@ -54,7 +54,9 @@ theorem factorial_mul_endpointDeficitDenominator | succ h ih => rw [endpointDeficitDenominator, Finset.prod_Icc_succ_top (by omega : 1 ≤ h + 1)] - rw [← endpointDeficitDenominator, Nat.factorial_succ] + change d.factorial * + (endpointDeficitDenominator d h * (d + (h + 1))) = + (d + (h + 1)).factorial calc d.factorial * (endpointDeficitDenominator d h * (d + (h + 1))) = @@ -73,7 +75,7 @@ theorem endpointDeficitDenominator_eq_descFactorial d.factorial * (d + h).descFactorial h = (d + h).factorial := by simpa using (Nat.factorial_mul_descFactorial (show h ≤ d + h by omega)) - exact Nat.mul_left_cancel (hleft.trans hright.symm) + exact Nat.mul_left_cancel (Nat.factorial_pos d) (hleft.trans hright.symm) /-- Closed form for a one-cell matching count when the smaller endpoint is `m`. -/ @@ -83,7 +85,7 @@ theorem lowerUpperCellMatchingCount_eq_choose_mul_descFactorial m.choose j * (m + d).descFactorial j := by have hcard := card_singleCellStubMatching_mul_factorial m (m + d) j have hlower : m.descFactorial j = j.factorial * m.choose j := - Nat.descFactorial_eq_factorial_mul_choose + Nat.descFactorial_eq_factorial_mul_choose m j rw [hlower] at hcard have hmul : lowerUpperCellMatchingCount m d j * j.factorial = @@ -93,7 +95,7 @@ theorem lowerUpperCellMatchingCount_eq_choose_mul_descFactorial (j.factorial * m.choose j) * (m + d).descFactorial j := hcard _ = (m.choose j * (m + d).descFactorial j) * j.factorial := by ring - exact Nat.mul_right_cancel hmul + exact Nat.mul_right_cancel (Nat.factorial_pos j) hmul /-- Splitting the upper-endpoint descending factorial at deficit `h`. -/ theorem upperEndpoint_descFactorial_full_split @@ -101,15 +103,16 @@ theorem upperEndpoint_descFactorial_full_split (m + d).descFactorial m = (m + d).descFactorial (m - h) * (d + h).descFactorial h := by have hgap : m + d - (m - h) = d + h := by omega - have hsum : (m - h) + h = m := Nat.sub_add_cancel hh + have hremain : m - (m - h) = h := by omega calc (m + d).descFactorial m = - (m + d).descFactorial ((m - h) + h) := by rw [hsum] - _ = (m + d).descFactorial (m - h) * - (m + d - (m - h)).descFactorial h := by + (m + d - (m - h)).descFactorial (m - (m - h)) * + (m + d).descFactorial (m - h) := by rw [Nat.descFactorial_mul_descFactorial] + _ = (d + h).descFactorial h * + (m + d).descFactorial (m - h) := by rw [hgap, hremain] _ = (m + d).descFactorial (m - h) * - (d + h).descFactorial h := by rw [hgap] + (d + h).descFactorial h := by rw [mul_comm] /-- Exact physical matching-count ratio in cross-multiplied form. -/ theorem lowerUpperCellMatchingCount_deficit_cross_mul @@ -121,8 +124,8 @@ theorem lowerUpperCellMatchingCount_deficit_cross_mul m d (m - h) (Nat.sub_le _ _), lowerUpperCellMatchingCount_eq_choose_mul_descFactorial m d m le_rfl, Nat.choose_self, one_mul, Nat.choose_symm hh, - endpointDeficitDenominator_eq_descFactorial] - rw [← upperEndpoint_descFactorial_full_split m d h hh] + endpointDeficitDenominator_eq_descFactorial, + upperEndpoint_descFactorial_full_split m d h hh] ring /-- One-step identity for the quadratic binary exponent. -/ @@ -146,11 +149,13 @@ theorem localSignRewardNat_pred_mul_pow have hpred3 : 3 ≤ x - 1 := by omega have hchooseRec : x.choose 2 = (x - 1).choose 2 + (x - 1) := by - have hxrec : x - 1 + 1 = x := by omega - conv_lhs => rw [← hxrec] - rw [Nat.choose_succ_succ] - simp only [Nat.choose_one_right] - omega + calc + x.choose 2 = (x - 1 + 1).choose (1 + 1) := by congr <;> omega + _ = (x - 1).choose 1 + (x - 1).choose 2 := by + rw [Nat.choose_succ_succ] + _ = (x - 1).choose 2 + (x - 1) := by + simp only [Nat.choose_one_right] + omega have hchoosePred : 1 ≤ (x - 1).choose 2 := by have hmono := Nat.choose_le_choose 2 hpred3 norm_num at hmono @@ -198,13 +203,23 @@ theorem lowerUpperCellWeightedCount_deficit_cross_mul 2 ^ (h * m - h * (h + 1) / 2) = lowerUpperCellWeightedCount m d m * m.choose h := by unfold lowerUpperCellWeightedCount - rw [mul_assoc, - show lowerUpperCellMatchingCount m d (m - h) * - endpointDeficitDenominator d h = - lowerUpperCellMatchingCount m d m * m.choose h from - lowerUpperCellMatchingCount_deficit_cross_mul m d h hh, - localSignRewardNat_deficit_mul_pow m h hh hhigh] - ring + calc + lowerUpperCellMatchingCount m d (m - h) * + localSignRewardNat (m - h) * + endpointDeficitDenominator d h * + 2 ^ (h * m - h * (h + 1) / 2) = + (lowerUpperCellMatchingCount m d (m - h) * + endpointDeficitDenominator d h) * + (localSignRewardNat (m - h) * + 2 ^ (h * m - h * (h + 1) / 2)) := by + ring + _ = (lowerUpperCellMatchingCount m d m * m.choose h) * + localSignRewardNat m := by + rw [lowerUpperCellMatchingCount_deficit_cross_mul m d h hh, + localSignRewardNat_deficit_mul_pow m h hh hhigh] + _ = lowerUpperCellMatchingCount m d m * + localSignRewardNat m * m.choose h := by + ring #print axioms endpointDeficitDenominator_eq_descFactorial #print axioms lowerUpperCellMatchingCount_deficit_cross_mul From 7283cb74ee856a13e07ecc76e52a7201d9a46636 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:14:20 +0300 Subject: [PATCH 44/59] Close the final exact local deficit side conditions --- .../Erdos625/Section8ExactLocalDeficitRatio.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean index c29246de..ae320ca3 100644 --- a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean +++ b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean @@ -64,7 +64,7 @@ theorem factorial_mul_endpointDeficitDenominator ring _ = (d + h).factorial * (d + h + 1) := by rw [ih] _ = (d + h + 1).factorial := by - rw [Nat.factorial_succ] + rw [Nat.factorial_succ, mul_comm] /-- The consecutive endpoint-distance product is a descending factorial. -/ theorem endpointDeficitDenominator_eq_descFactorial @@ -80,7 +80,7 @@ theorem endpointDeficitDenominator_eq_descFactorial /-- Closed form for a one-cell matching count when the smaller endpoint is `m`. -/ theorem lowerUpperCellMatchingCount_eq_choose_mul_descFactorial - (m d j : Nat) (hj : j ≤ m) : + (m d j : Nat) (_hj : j ≤ m) : lowerUpperCellMatchingCount m d j = m.choose j * (m + d).descFactorial j := by have hcard := card_singleCellStubMatching_mul_factorial m (m + d) j @@ -109,6 +109,7 @@ theorem upperEndpoint_descFactorial_full_split (m + d - (m - h)).descFactorial (m - (m - h)) * (m + d).descFactorial (m - h) := by rw [Nat.descFactorial_mul_descFactorial] + omega _ = (d + h).descFactorial h * (m + d).descFactorial (m - h) := by rw [hgap, hremain] _ = (m + d).descFactorial (m - h) * From da25b22eacbd142ee413a30dfd2d321b63663c5f Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:20:52 +0300 Subject: [PATCH 45/59] Remove the warning-fatal congruence style lint --- .../Erdos625/Section8ExactLocalDeficitRatio.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean index ae320ca3..bfd5d73a 100644 --- a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean +++ b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean @@ -150,8 +150,10 @@ theorem localSignRewardNat_pred_mul_pow have hpred3 : 3 ≤ x - 1 := by omega have hchooseRec : x.choose 2 = (x - 1).choose 2 + (x - 1) := by + have hxrec : x - 1 + 1 = x := by omega calc - x.choose 2 = (x - 1 + 1).choose (1 + 1) := by congr <;> omega + x.choose 2 = (x - 1 + 1).choose (1 + 1) := by + simpa only [hxrec] _ = (x - 1).choose 1 + (x - 1).choose 2 := by rw [Nat.choose_succ_succ] _ = (x - 1).choose 2 + (x - 1) := by From c19c7e8ba3e49b7064e3a2123df49cc96f61cba7 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:27:22 +0300 Subject: [PATCH 46/59] Clear the final warning-fatal local ratio lint --- 625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean index bfd5d73a..ef673560 100644 --- a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean +++ b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean @@ -153,7 +153,7 @@ theorem localSignRewardNat_pred_mul_pow have hxrec : x - 1 + 1 = x := by omega calc x.choose 2 = (x - 1 + 1).choose (1 + 1) := by - simpa only [hxrec] + simp only [hxrec] _ = (x - 1).choose 1 + (x - 1).choose 2 := by rw [Nat.choose_succ_succ] _ = (x - 1).choose 2 + (x - 1) := by From 7b86079f8c38e5a54b4d6753a8ad81646db77cb4 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:32:38 +0300 Subject: [PATCH 47/59] Bridge the exact local deficit identity to nearCellTerm --- .../Section8ExactLocalDeficitENNReal.lean | 112 ++++++++++++++++++ 1 file changed, 112 insertions(+) create mode 100644 625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean new file mode 100644 index 00000000..cfb2c919 --- /dev/null +++ b/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean @@ -0,0 +1,112 @@ +import Erdos625.Section8ExactLocalDeficitRatio +import Erdos625.Section8NearCellChoiceLink +import Mathlib.Tactic + +/-! +# Section VIII: exact local deficit ratio in `ENNReal` + +The natural-number module proves the local partial/full identity without any +division. This file performs only the justified finite cancellations needed to +express that identity in the multiplicative language of the Section VIII +partition function. + +The final theorem says exactly: + +`partialWeightedCell * n^h = fullWeightedCell * nearCellTerm n m d h`. + +Thus the existing `nearCellTerm` is not merely a majorant: before the later +three-quarter estimate it is the exact charged ratio between the physical +partial cell and its full-containment reference. +-/ + +namespace Erdos625 + +open scoped ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- Exact uncharged local partial/full ratio. -/ +def exactLocalDeficitRatioENNReal (m d h : Nat) : ENNReal := + ((m.choose h : ENNReal) / + ((endpointDeficitDenominator d h : Nat) : ENNReal)) * + ((2 : ENNReal) ^ (h * m - h * (h + 1) / 2))⁻¹ + +/-- The endpoint-distance denominator is a positive finite natural number. -/ +theorem endpointDeficitDenominator_pos (d h : Nat) : + 0 < endpointDeficitDenominator d h := by + rw [endpointDeficitDenominator_eq_descFactorial] + exact Nat.descFactorial_pos.mpr (by omega) + +/-- The exact natural identity, cancelled only through positive finite factors. -/ +theorem lowerUpperCellWeightedCount_cast_eq_full_mul_exactRatio + (m d h : Nat) (hh : h ≤ m) (hhigh : 3 ≤ m - h) : + (lowerUpperCellWeightedCount m d (m - h) : ENNReal) = + (lowerUpperCellWeightedCount m d m : ENNReal) * + exactLocalDeficitRatioENNReal m d h := by + let D : ENNReal := (endpointDeficitDenominator d h : Nat) + let P : ENNReal := (2 : ENNReal) ^ (h * m - h * (h + 1) / 2) + have hD0 : D ≠ 0 := by + dsimp [D] + exact_mod_cast (endpointDeficitDenominator_pos d h).ne' + have hDtop : D ≠ ∞ := by + dsimp [D] + exact ENNReal.natCast_ne_top _ + have hP0 : P ≠ 0 := by + dsimp [P] + exact pow_ne_zero _ (by norm_num : (2 : ENNReal) ≠ 0) + have hPtop : P ≠ ∞ := by + dsimp [P] + exact ENNReal.pow_ne_top (by norm_num : (2 : ENNReal) ≠ ∞) + have hcross : + (lowerUpperCellWeightedCount m d (m - h) : ENNReal) * D * P = + (lowerUpperCellWeightedCount m d m : ENNReal) * (m.choose h : ENNReal) := by + dsimp [D, P] + exact_mod_cast + lowerUpperCellWeightedCount_deficit_cross_mul m d h hh hhigh + have hdivideP : + (lowerUpperCellWeightedCount m d (m - h) : ENNReal) * D = + ((lowerUpperCellWeightedCount m d m : ENNReal) * + (m.choose h : ENNReal)) / P := by + apply (ENNReal.eq_div_iff hP0 hPtop).2 + exact hcross + have hdivideD : + (lowerUpperCellWeightedCount m d (m - h) : ENNReal) = + (((lowerUpperCellWeightedCount m d m : ENNReal) * + (m.choose h : ENNReal)) / P) / D := by + apply (ENNReal.eq_div_iff hD0 hDtop).2 + exact hdivideP + rw [hdivideD] + unfold exactLocalDeficitRatioENNReal + dsimp only [D, P] + simp only [div_eq_mul_inv] + ring + +/-- The manuscript's charged term is `n^h` times the exact uncharged ratio. -/ +theorem nearCellTerm_eq_pow_mul_exactLocalDeficitRatio + (n m d h : Nat) : + nearCellTerm n m d h = + (n : ENNReal) ^ h * exactLocalDeficitRatioENNReal m d h := by + unfold nearCellTerm exactLocalDeficitRatioENNReal + endpointDeficitDenominator + simp only [div_eq_mul_inv] + ring + +/-- Exact charged one-cell identity used in the direct all-deficit product. -/ +theorem lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + (n m d h : Nat) (hh : h ≤ m) (hhigh : 3 ≤ m - h) : + (lowerUpperCellWeightedCount m d (m - h) : ENNReal) * (n : ENNReal) ^ h = + (lowerUpperCellWeightedCount m d m : ENNReal) * + nearCellTerm n m d h := by + rw [lowerUpperCellWeightedCount_cast_eq_full_mul_exactRatio m d h hh hhigh, + nearCellTerm_eq_pow_mul_exactLocalDeficitRatio] + ring + +#print axioms lowerUpperCellWeightedCount_cast_eq_full_mul_exactRatio +#print axioms nearCellTerm_eq_pow_mul_exactLocalDeficitRatio +#print axioms lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + +end + +end Erdos625 From eea100fa9fe9c29d71f959d2c6bc0ddba73dfc99 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:33:53 +0300 Subject: [PATCH 48/59] Build the exact ENNReal local-ratio bridge --- .github/workflows/erdos625-direct-half-deficit-assembly.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index 29170e69..8c077985 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -7,6 +7,7 @@ on: - "625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean" - "625/formalization/Erdos625/Section8PointwiseChargeProduct.lean" - "625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean" + - "625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean" - "625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean" @@ -49,6 +50,7 @@ jobs: 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ 625/formalization/Erdos625/Section8PointwiseChargeProduct.lean \ 625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean \ + 625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ 625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean \ 625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean \ @@ -72,6 +74,7 @@ jobs: for target in \ Erdos625.Section8PointwiseChargeProduct \ Erdos625.Section8ExactLocalDeficitRatio \ + Erdos625.Section8ExactLocalDeficitENNReal \ Erdos625.Section8CanonicalThreeQuarterRho \ Erdos625.Section8CoarsePhaseCorridor \ Erdos625.Section8FiniteBareSkeletonReduction; do From 90676e77c522b01686b88f0fe68779618bd93fb0 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:38:17 +0300 Subject: [PATCH 49/59] Generalize the exact charged local ratio to arbitrary endpoints --- .../Section8SymmetricLocalDeficitRatio.lean | 88 +++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean diff --git a/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean new file mode 100644 index 00000000..5a8d8b37 --- /dev/null +++ b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean @@ -0,0 +1,88 @@ +import Erdos625.Section8ExactLocalDeficitENNReal +import Mathlib.Tactic + +/-! +# Section VIII: symmetric exact local deficit ratio + +The one-cell algebra was first proved with endpoint sizes `m` and `m+d`. An +actual overlap cell presents its two endpoint sizes in an arbitrary order. This +module removes that orientation issue once and for all. + +For arbitrary endpoint sizes `u,v`, put + +`m = min u v`, `d = Nat.dist u v`. + +The final theorem identifies the exact charged partial/full ratio using these +canonical symmetric parameters. Consequently the global endpoint proof needs +neither a case split over the sixteen endpoint types nor an orientation choice +for every selected block pair. +-/ + +namespace Erdos625 + +open scoped ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- Physical matching count times signed reward for arbitrary endpoint sizes. -/ +def endpointCellWeightedCount (u v j : Nat) : Nat := + Fintype.card (SingleCellStubMatching u v j) * localSignRewardNat j + +/-- The one-cell physical matching cardinality is symmetric in its endpoints. -/ +theorem card_singleCellStubMatching_comm (u v j : Nat) : + Fintype.card (SingleCellStubMatching u v j) = + Fintype.card (SingleCellStubMatching v u j) := by + have huv := card_singleCellStubMatching_mul_factorial u v j + have hvu := card_singleCellStubMatching_mul_factorial v u j + have hmul : + Fintype.card (SingleCellStubMatching u v j) * j.factorial = + Fintype.card (SingleCellStubMatching v u j) * j.factorial := by + calc + Fintype.card (SingleCellStubMatching u v j) * j.factorial = + u.descFactorial j * v.descFactorial j := huv + _ = v.descFactorial j * u.descFactorial j := by rw [mul_comm] + _ = Fintype.card (SingleCellStubMatching v u j) * j.factorial := hvu.symm + exact Nat.mul_right_cancel (Nat.factorial_pos j) hmul + +/-- The weighted one-cell count is symmetric in its endpoints. -/ +theorem endpointCellWeightedCount_comm (u v j : Nat) : + endpointCellWeightedCount u v j = endpointCellWeightedCount v u j := by + unfold endpointCellWeightedCount + rw [card_singleCellStubMatching_comm] + +/-- The oriented and symmetric weighted-cell definitions agree. -/ +theorem endpointCellWeightedCount_lowerUpper + (m d j : Nat) : + endpointCellWeightedCount m (m + d) j = + lowerUpperCellWeightedCount m d j := rfl + +/-- Exact charged partial/full identity for arbitrary endpoint sizes. -/ +theorem endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + (n u v h : Nat) + (hh : h ≤ min u v) (hhigh : 3 ≤ min u v - h) : + (endpointCellWeightedCount u v (min u v - h) : ENNReal) * + (n : ENNReal) ^ h = + (endpointCellWeightedCount u v (min u v) : ENNReal) * + nearCellTerm n (min u v) (Nat.dist u v) h := by + rcases le_total u v with huv | hvu + · have huvEq : u + (v - u) = v := Nat.add_sub_of_le huv + simpa only [min_eq_left huv, Nat.dist_eq_sub_of_le huv, + endpointCellWeightedCount, lowerUpperCellWeightedCount, huvEq] using + lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + n u (v - u) h hh hhigh + · have hvuEq : v + (u - v) = u := Nat.add_sub_of_le hvu + rw [endpointCellWeightedCount_comm u v (min u v - h), + endpointCellWeightedCount_comm u v (min u v)] + simpa only [min_eq_right hvu, Nat.dist_eq_sub_of_le_right hvu, + endpointCellWeightedCount, lowerUpperCellWeightedCount, hvuEq] using + lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + n v (u - v) h hh hhigh + +#print axioms card_singleCellStubMatching_comm +#print axioms endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + +end + +end Erdos625 From 33049fee235efb43dcc626c557e5bc572148b3e4 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:39:30 +0300 Subject: [PATCH 50/59] Build the symmetric exact local-ratio bridge --- .github/workflows/erdos625-direct-half-deficit-assembly.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index 8c077985..567374db 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -8,6 +8,7 @@ on: - "625/formalization/Erdos625/Section8PointwiseChargeProduct.lean" - "625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean" - "625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean" + - "625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean" - "625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean" @@ -51,6 +52,7 @@ jobs: 625/formalization/Erdos625/Section8PointwiseChargeProduct.lean \ 625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean \ 625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean \ + 625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ 625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean \ 625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean \ @@ -75,6 +77,7 @@ jobs: Erdos625.Section8PointwiseChargeProduct \ Erdos625.Section8ExactLocalDeficitRatio \ Erdos625.Section8ExactLocalDeficitENNReal \ + Erdos625.Section8SymmetricLocalDeficitRatio \ Erdos625.Section8CanonicalThreeQuarterRho \ Erdos625.Section8CoarsePhaseCorridor \ Erdos625.Section8FiniteBareSkeletonReduction; do From d722cf213c6fec6a7e981d8c4ae8ef0382ea8d33 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:45:20 +0300 Subject: [PATCH 51/59] Commute the justified ENNReal denominator cancellations explicitly --- .../Erdos625/Section8ExactLocalDeficitENNReal.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean index cfb2c919..2fbcf861 100644 --- a/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean +++ b/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean @@ -70,13 +70,13 @@ theorem lowerUpperCellWeightedCount_cast_eq_full_mul_exactRatio ((lowerUpperCellWeightedCount m d m : ENNReal) * (m.choose h : ENNReal)) / P := by apply (ENNReal.eq_div_iff hP0 hPtop).2 - exact hcross + simpa only [mul_comm] using hcross have hdivideD : (lowerUpperCellWeightedCount m d (m - h) : ENNReal) = (((lowerUpperCellWeightedCount m d m : ENNReal) * (m.choose h : ENNReal)) / P) / D := by apply (ENNReal.eq_div_iff hD0 hDtop).2 - exact hdivideP + simpa only [mul_comm] using hdivideP rw [hdivideD] unfold exactLocalDeficitRatioENNReal dsimp only [D, P] From e552becb914807d8a220552acf693e17c33e49ef Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Wed, 29 Jul 2026 23:50:20 +0300 Subject: [PATCH 52/59] Group support products by endpoint type and expose the full reference product --- .../Section8SupportProductGrouping.lean | 168 ++++++++++++++++++ 1 file changed, 168 insertions(+) create mode 100644 625/formalization/Erdos625/Section8SupportProductGrouping.lean diff --git a/625/formalization/Erdos625/Section8SupportProductGrouping.lean b/625/formalization/Erdos625/Section8SupportProductGrouping.lean new file mode 100644 index 00000000..a871d241 --- /dev/null +++ b/625/formalization/Erdos625/Section8SupportProductGrouping.lean @@ -0,0 +1,168 @@ +import Erdos625.Section8DirectReferenceGrouping +import Erdos625.Section8SymmetricLocalDeficitRatio +import Mathlib.Tactic + +/-! +# Section VIII: support products grouped by endpoint type + +A block support is a finite matching whose edges carry one of sixteen endpoint +coordinate pairs. Products and sums over selected physical block pairs can +therefore be regrouped by the support's `4 x 4` type table. + +This module extracts that finite identity from the decorated-pairing count and +uses it to rewrite the zero-deficit reference of one support as the literal +product of full one-cell weighted counts times the single ambient reciprocal +falling factorial. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- Product over support edges, grouped by their endpoint types. -/ +theorem fourEndpointSupport_prod_by_type + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) + {R : Type*} [CommMonoid R] + (f : Fin 4 → Fin 4 → R) : + (∏ e : ↥P.edges, f e.1.1.1 e.1.2.1) = + ∏ i : Fin 4, ∏ j : Fin 4, (f i j) ^ P.typeTable i j := by + rw [← Finset.prod_subtype P.edges (fun _ => Iff.rfl) + (fun e => f e.1.1 e.2.1)] + rw [← Finset.prod_fiberwise' P.edges + (fun e => (e.1.1, e.2.1)) + (fun ij : Fin 4 × Fin 4 => f ij.1 ij.2)] + rw [Fintype.prod_prod_type] + apply Finset.prod_congr rfl + intro i _ + apply Finset.prod_congr rfl + intro j _ + rw [Finset.prod_const] + apply congrArg (fun count => (f i j) ^ count) + change (P.edges.filter fun e => (e.1.1, e.2.1) = (i, j)).card = _ + change (P.edges.filter fun e => e.1.1 = i ∧ e.2.1 = j).card = _ + rfl + +/-- Sum over support edges, grouped by endpoint type. -/ +theorem fourEndpointSupport_sum_by_type + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) + {R : Type*} [AddCommMonoid R] + (f : Fin 4 → Fin 4 → R) : + (∑ e : ↥P.edges, f e.1.1.1 e.1.2.1) = + ∑ i : Fin 4, ∑ j : Fin 4, P.typeTable i j • f i j := by + rw [← Finset.sum_subtype P.edges (fun _ => Iff.rfl) + (fun e => f e.1.1 e.2.1)] + rw [← Finset.sum_fiberwise' P.edges + (fun e => (e.1.1, e.2.1)) + (fun ij : Fin 4 × Fin 4 => f ij.1 ij.2)] + rw [Fintype.sum_prod_type] + apply Finset.sum_congr rfl + intro i _ + apply Finset.sum_congr rfl + intro j _ + rw [Finset.sum_const] + congr 1 + change (P.edges.filter fun e => (e.1.1, e.2.1) = (i, j)).card = _ + change (P.edges.filter fun e => e.1.1 = i ∧ e.2.1 = j).card = _ + rfl + +/-- Full exposed multiplicity of one support. -/ +def fourEndpointSupportFullTotalMultiplicity + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : Nat := + ∑ e : ↥P.edges, + fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1 + +/-- The edgewise total equals `J` of the support's endpoint table. -/ +theorem fourEndpointSupportFullTotalMultiplicity_eq_J + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : + fourEndpointSupportFullTotalMultiplicity alpha hAlpha P = + fourEndpointJ alpha hAlpha + (fourEndpointSupportTable alpha hAlpha P) := by + unfold fourEndpointSupportFullTotalMultiplicity fourEndpointJ + fourEndpointSupportTable + rw [fourEndpointSupport_sum_by_type alpha hAlpha P] + simp only [nsmul_eq_mul, mul_comm] + +/-- Product of full weighted one-cell counts on a support. -/ +def fourEndpointSupportFullCellWeightProduct + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : ENNReal := + ∏ e : ↥P.edges, + (endpointCellWeightedCount + (fourEndpointSize alpha hAlpha e.1.1.1) + (fourEndpointSize alpha hAlpha e.1.2.1) + (fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1) : Nat) + +/-- Cardinality of all full local stub decorations equals the product of the +one-cell cardinalities. -/ +theorem card_fourEndpointFullDecorationOfSupport + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : + Fintype.card (FourEndpointFullDecorationOfSupport alpha hAlpha P) = + ∏ e : ↥P.edges, + Fintype.card (SingleCellStubMatching + (fourEndpointSize alpha hAlpha e.1.1.1) + (fourEndpointSize alpha hAlpha e.1.2.1) + (fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1)) := by + rw [Fintype.card_pi] + +/-- The table reward product is the edgewise product of local rewards. -/ +theorem fourEndpointFullRewardProduct_supportTable + (alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : + fourEndpointFullRewardProduct alpha hAlpha + (fourEndpointSupportTable alpha hAlpha P) = + ∏ e : ↥P.edges, + (localSignRewardNat + (fourEndpointOverlapSize alpha hAlpha e.1.1.1 e.1.2.1) : ENNReal) := by + unfold fourEndpointFullRewardProduct fourEndpointSupportTable + symm + exact fourEndpointSupport_prod_by_type alpha hAlpha P + (fun i j => + (localSignRewardNat + (fourEndpointOverlapSize alpha hAlpha i j) : ENNReal)) + +/-- Exact algebraic form of the full-support reference weight. -/ +theorem fourEndpointFullSupportReferenceWeight_eq_cellProduct + (n alpha : Nat) (hAlpha : 5 < alpha) + {k : ColoringProfile (alpha + 1)} + (P : FourEndpointAbstractBlockSkeleton alpha hAlpha k) : + fourEndpointFullSupportReferenceWeight n alpha hAlpha P = + fourEndpointSupportFullCellWeightProduct alpha hAlpha P * + (((n.descFactorial + (fourEndpointSupportFullTotalMultiplicity alpha hAlpha P) : Nat) : + ENNReal)⁻¹) := by + unfold fourEndpointFullSupportReferenceWeight + fourEndpointFullSupportAtomWeight + fourEndpointDecoratedReferenceAtomWeight + fourEndpointSupportFullCellWeightProduct + rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] + rw [card_fourEndpointFullDecorationOfSupport] + rw [fourEndpointFullRewardProduct_supportTable] + rw [← fourEndpointSupportFullTotalMultiplicity_eq_J] + simp only [div_eq_mul_inv, Nat.cast_prod, Nat.cast_mul] + rw [Finset.prod_mul_distrib] + ring + +#print axioms fourEndpointSupport_prod_by_type +#print axioms fourEndpointSupport_sum_by_type +#print axioms fourEndpointSupportFullTotalMultiplicity_eq_J +#print axioms fourEndpointFullSupportReferenceWeight_eq_cellProduct + +end + +end Erdos625 From f85eff906ac259e49bcd3028cc0eb02b19e36e96 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 30 Jul 2026 18:49:41 +0300 Subject: [PATCH 53/59] Fix branch-local half-deficit hypotheses in symmetric ratio --- .../Erdos625/Section8SymmetricLocalDeficitRatio.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean index 5a8d8b37..01c9eed5 100644 --- a/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean +++ b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean @@ -68,17 +68,21 @@ theorem endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm nearCellTerm n (min u v) (Nat.dist u v) h := by rcases le_total u v with huv | hvu · have huvEq : u + (v - u) = v := Nat.add_sub_of_le huv + have hhu : h ≤ u := by simpa only [min_eq_left huv] using hh + have hhighu : 3 ≤ u - h := by simpa only [min_eq_left huv] using hhigh simpa only [min_eq_left huv, Nat.dist_eq_sub_of_le huv, endpointCellWeightedCount, lowerUpperCellWeightedCount, huvEq] using lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm - n u (v - u) h hh hhigh + n u (v - u) h hhu hhighu · have hvuEq : v + (u - v) = u := Nat.add_sub_of_le hvu + have hhv : h ≤ v := by simpa only [min_eq_right hvu] using hh + have hhighv : 3 ≤ v - h := by simpa only [min_eq_right hvu] using hhigh rw [endpointCellWeightedCount_comm u v (min u v - h), endpointCellWeightedCount_comm u v (min u v)] simpa only [min_eq_right hvu, Nat.dist_eq_sub_of_le_right hvu, endpointCellWeightedCount, lowerUpperCellWeightedCount, hvuEq] using lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm - n v (u - v) h hh hhigh + n v (u - v) h hhv hhighv #print axioms card_singleCellStubMatching_comm #print axioms endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm From f6d16509a6cc72b757fc1a3181c5f3108479a6be Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 30 Jul 2026 19:01:03 +0300 Subject: [PATCH 54/59] Rewrite symmetric cells through oriented weighted counts --- .../Section8SymmetricLocalDeficitRatio.lean | 28 ++++++++++++------- 1 file changed, 18 insertions(+), 10 deletions(-) diff --git a/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean index 01c9eed5..2f84014a 100644 --- a/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean +++ b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean @@ -70,19 +70,27 @@ theorem endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm · have huvEq : u + (v - u) = v := Nat.add_sub_of_le huv have hhu : h ≤ u := by simpa only [min_eq_left huv] using hh have hhighu : 3 ≤ u - h := by simpa only [min_eq_left huv] using hhigh - simpa only [min_eq_left huv, Nat.dist_eq_sub_of_le huv, - endpointCellWeightedCount, lowerUpperCellWeightedCount, huvEq] using - lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm - n u (v - u) h hhu hhighu + have hcell (j : Nat) : + endpointCellWeightedCount u v j = + lowerUpperCellWeightedCount u (v - u) j := by + rw [← huvEq] + rfl + rw [min_eq_left huv, Nat.dist_eq_sub_of_le huv, + hcell (u - h), hcell u] + exact lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + n u (v - u) h hhu hhighu · have hvuEq : v + (u - v) = u := Nat.add_sub_of_le hvu have hhv : h ≤ v := by simpa only [min_eq_right hvu] using hh have hhighv : 3 ≤ v - h := by simpa only [min_eq_right hvu] using hhigh - rw [endpointCellWeightedCount_comm u v (min u v - h), - endpointCellWeightedCount_comm u v (min u v)] - simpa only [min_eq_right hvu, Nat.dist_eq_sub_of_le_right hvu, - endpointCellWeightedCount, lowerUpperCellWeightedCount, hvuEq] using - lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm - n v (u - v) h hhv hhighv + have hcell (j : Nat) : + endpointCellWeightedCount u v j = + lowerUpperCellWeightedCount v (u - v) j := by + rw [endpointCellWeightedCount_comm u v j, ← hvuEq] + rfl + rw [min_eq_right hvu, Nat.dist_eq_sub_of_le_right hvu, + hcell (v - h), hcell v] + exact lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + n v (u - v) h hhv hhighv #print axioms card_singleCellStubMatching_comm #print axioms endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm From 9d51a696931946bfc36165d5344e63a2f4661776 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 30 Jul 2026 19:09:16 +0300 Subject: [PATCH 55/59] Unfold oriented cell counts in symmetric ratio bridge --- .../Erdos625/Section8SymmetricLocalDeficitRatio.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean index 2f84014a..2c3ff2c9 100644 --- a/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean +++ b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean @@ -73,8 +73,8 @@ theorem endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm have hcell (j : Nat) : endpointCellWeightedCount u v j = lowerUpperCellWeightedCount u (v - u) j := by - rw [← huvEq] - rfl + simp only [endpointCellWeightedCount, lowerUpperCellWeightedCount, + lowerUpperCellMatchingCount, huvEq] rw [min_eq_left huv, Nat.dist_eq_sub_of_le huv, hcell (u - h), hcell u] exact lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm @@ -85,8 +85,9 @@ theorem endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm have hcell (j : Nat) : endpointCellWeightedCount u v j = lowerUpperCellWeightedCount v (u - v) j := by - rw [endpointCellWeightedCount_comm u v j, ← hvuEq] - rfl + rw [endpointCellWeightedCount_comm u v j] + simp only [endpointCellWeightedCount, lowerUpperCellWeightedCount, + lowerUpperCellMatchingCount, hvuEq] rw [min_eq_right hvu, Nat.dist_eq_sub_of_le_right hvu, hcell (v - h), hcell v] exact lowerUpperCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm From 6a5d8a26443756045d521939b94bb9a624547ecb Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 30 Jul 2026 19:13:22 +0300 Subject: [PATCH 56/59] Validate support-product grouping in focused Section 8 CI --- .github/workflows/erdos625-direct-half-deficit-assembly.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/erdos625-direct-half-deficit-assembly.yml b/.github/workflows/erdos625-direct-half-deficit-assembly.yml index 567374db..a2e2ddbb 100644 --- a/.github/workflows/erdos625-direct-half-deficit-assembly.yml +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -9,6 +9,7 @@ on: - "625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean" - "625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean" - "625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean" + - "625/formalization/Erdos625/Section8SupportProductGrouping.lean" - "625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean" - "625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean" - "625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean" @@ -53,6 +54,7 @@ jobs: 625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean \ 625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean \ 625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean \ + 625/formalization/Erdos625/Section8SupportProductGrouping.lean \ 625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean \ 625/formalization/Erdos625/Section8CanonicalThreeQuarterRho.lean \ 625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean \ @@ -78,6 +80,7 @@ jobs: Erdos625.Section8ExactLocalDeficitRatio \ Erdos625.Section8ExactLocalDeficitENNReal \ Erdos625.Section8SymmetricLocalDeficitRatio \ + Erdos625.Section8SupportProductGrouping \ Erdos625.Section8CanonicalThreeQuarterRho \ Erdos625.Section8CoarsePhaseCorridor \ Erdos625.Section8FiniteBareSkeletonReduction; do From 32220eb965e320b6feb4083c5b8050f317b6bb1a Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 30 Jul 2026 19:23:57 +0300 Subject: [PATCH 57/59] Repair exact support grouping and reference expansion --- .../Section8SupportProductGrouping.lean | 29 ++++++++++++------- 1 file changed, 19 insertions(+), 10 deletions(-) diff --git a/625/formalization/Erdos625/Section8SupportProductGrouping.lean b/625/formalization/Erdos625/Section8SupportProductGrouping.lean index a871d241..e44e5fd7 100644 --- a/625/formalization/Erdos625/Section8SupportProductGrouping.lean +++ b/625/formalization/Erdos625/Section8SupportProductGrouping.lean @@ -44,9 +44,13 @@ theorem fourEndpointSupport_prod_by_type intro j _ rw [Finset.prod_const] apply congrArg (fun count => (f i j) ^ count) - change (P.edges.filter fun e => (e.1.1, e.2.1) = (i, j)).card = _ - change (P.edges.filter fun e => e.1.1 = i ∧ e.2.1 = j).card = _ - rfl + calc + (P.edges.filter fun e => (e.1.1, e.2.1) = (i, j)).card = + (P.edges.filter fun e => e.1.1 = i ∧ e.2.1 = j).card := by + congr 1 + ext e + simp [Prod.ext_iff] + _ = P.typeTable i j := rfl /-- Sum over support edges, grouped by endpoint type. -/ theorem fourEndpointSupport_sum_by_type @@ -69,9 +73,13 @@ theorem fourEndpointSupport_sum_by_type intro j _ rw [Finset.sum_const] congr 1 - change (P.edges.filter fun e => (e.1.1, e.2.1) = (i, j)).card = _ - change (P.edges.filter fun e => e.1.1 = i ∧ e.2.1 = j).card = _ - rfl + calc + (P.edges.filter fun e => (e.1.1, e.2.1) = (i, j)).card = + (P.edges.filter fun e => e.1.1 = i ∧ e.2.1 = j).card := by + congr 1 + ext e + simp [Prod.ext_iff] + _ = P.typeTable i j := rfl /-- Full exposed multiplicity of one support. -/ def fourEndpointSupportFullTotalMultiplicity @@ -89,10 +97,10 @@ theorem fourEndpointSupportFullTotalMultiplicity_eq_J fourEndpointSupportFullTotalMultiplicity alpha hAlpha P = fourEndpointJ alpha hAlpha (fourEndpointSupportTable alpha hAlpha P) := by - unfold fourEndpointSupportFullTotalMultiplicity fourEndpointJ - fourEndpointSupportTable - rw [fourEndpointSupport_sum_by_type alpha hAlpha P] - simp only [nsmul_eq_mul, mul_comm] + simpa [fourEndpointSupportFullTotalMultiplicity, fourEndpointJ, + fourEndpointSupportTable, nsmul_eq_mul, Nat.cast_id, mul_comm] using + (fourEndpointSupport_sum_by_type alpha hAlpha P + (fun i j => fourEndpointOverlapSize alpha hAlpha i j)) /-- Product of full weighted one-cell counts on a support. -/ def fourEndpointSupportFullCellWeightProduct @@ -150,6 +158,7 @@ theorem fourEndpointFullSupportReferenceWeight_eq_cellProduct fourEndpointFullSupportAtomWeight fourEndpointDecoratedReferenceAtomWeight fourEndpointSupportFullCellWeightProduct + endpointCellWeightedCount rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] rw [card_fourEndpointFullDecorationOfSupport] rw [fourEndpointFullRewardProduct_supportTable] From dba04e04ee10dd2e84b65d97a0a250b74fe78512 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 30 Jul 2026 19:39:03 +0300 Subject: [PATCH 58/59] Supply the correct one-lower-bound for common powers --- .../Erdos625/Section8FiniteBareSkeletonReduction.lean | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean index 48e34b37..2bf1995a 100644 --- a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean +++ b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean @@ -97,6 +97,9 @@ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W let common : ENNReal := (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ fourEndpointTotalBlockCount alpha hAlpha k + have hOne : (1 : ENNReal) ≤ + 1 + ((alpha + 1 : Nat) : ENNReal) * rho := by + exact le_add_of_nonneg_right bot_le calc (∑ demand, weightDemand demand) ≤ ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, @@ -111,7 +114,7 @@ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W apply Finset.sum_le_sum intro P _ exact mul_le_mul_left - (pow_le_pow_right₀ bot_le + (pow_le_pow_right₀ hOne (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) (fourEndpointFullSupportReferenceWeight n alpha hAlpha P) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, @@ -148,6 +151,10 @@ theorem sum_profileCanonicalHighSkeleton_le_canonicalDeficitFactor_mul_sum_W (1 + ((alpha + 1 : Nat) : ENNReal) * fourEndpointThreeQuarterRho n alpha hAlpha) ^ fourEndpointTotalBlockCount alpha hAlpha k + have hOne : (1 : ENNReal) ≤ + 1 + ((alpha + 1 : Nat) : ENNReal) * + fourEndpointThreeQuarterRho n alpha hAlpha := by + exact le_add_of_nonneg_right bot_le calc (∑ demand, weightDemand demand) ≤ ∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, @@ -163,7 +170,7 @@ theorem sum_profileCanonicalHighSkeleton_le_canonicalDeficitFactor_mul_sum_W apply Finset.sum_le_sum intro P _ exact mul_le_mul_left - (pow_le_pow_right₀ bot_le + (pow_le_pow_right₀ hOne (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) (fourEndpointFullSupportReferenceWeight n alpha hAlpha P) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, From 094dfcc6168378c0807557f76268021cc2a5d283 Mon Sep 17 00:00:00 2001 From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com> Date: Thu, 30 Jul 2026 19:49:47 +0300 Subject: [PATCH 59/59] Normalize multiplication order in common-power bounds --- .../Section8FiniteBareSkeletonReduction.lean | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean index 2bf1995a..a1bdf39a 100644 --- a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean +++ b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean @@ -113,10 +113,11 @@ theorem sum_profileCanonicalHighSkeleton_le_commonDeficitFactor_mul_sum_W fourEndpointFullSupportReferenceWeight n alpha hAlpha P * common := by apply Finset.sum_le_sum intro P _ - exact mul_le_mul_left - (pow_le_pow_right₀ hOne - (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) - (fourEndpointFullSupportReferenceWeight n alpha hAlpha P) + have hp := pow_le_pow_right₀ hOne + (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P) + simpa only [common, mul_comm] using + (mul_le_mul_left hp + (fourEndpointFullSupportReferenceWeight n alpha hAlpha P)) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, fourEndpointFullSupportReferenceWeight n alpha hAlpha P) * common := by rw [Finset.sum_mul] @@ -169,10 +170,11 @@ theorem sum_profileCanonicalHighSkeleton_le_canonicalDeficitFactor_mul_sum_W fourEndpointFullSupportReferenceWeight n alpha hAlpha P * common := by apply Finset.sum_le_sum intro P _ - exact mul_le_mul_left - (pow_le_pow_right₀ hOne - (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P)) - (fourEndpointFullSupportReferenceWeight n alpha hAlpha P) + have hp := pow_le_pow_right₀ hOne + (fourEndpointAbstractBlockSkeleton_edges_card_le alpha hAlpha P) + simpa only [common, mul_comm] using + (mul_le_mul_left hp + (fourEndpointFullSupportReferenceWeight n alpha hAlpha P)) _ = (∑ P : FourEndpointAbstractBlockSkeleton alpha hAlpha k, fourEndpointFullSupportReferenceWeight n alpha hAlpha P) * common := by rw [Finset.sum_mul]