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..a2e2ddbb --- /dev/null +++ b/.github/workflows/erdos625-direct-half-deficit-assembly.yml @@ -0,0 +1,105 @@ +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/Section8PointwiseChargeProduct.lean" + - "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" + - "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" + 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/Section8FourDeficitProfileCover.lean \ + 625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean \ + 625/formalization/Erdos625/Section8PointwiseChargeProduct.lean \ + 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 \ + 625/formalization/Erdos625/Section8DirectReferenceGrouping.lean \ + 625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.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 simplified Section VIII interfaces warning-fatally + working-directory: 625/formalization + shell: bash + run: | + : > /tmp/erdos625-direct-half-deficit.log + for target in \ + Erdos625.Section8PointwiseChargeProduct \ + Erdos625.Section8ExactLocalDeficitRatio \ + Erdos625.Section8ExactLocalDeficitENNReal \ + Erdos625.Section8SymmetricLocalDeficitRatio \ + Erdos625.Section8SupportProductGrouping \ + Erdos625.Section8CanonicalThreeQuarterRho \ + Erdos625.Section8CoarsePhaseCorridor \ + 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 + - 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 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..c018f689 --- /dev/null +++ b/625/experiments/section8_direct_half_deficit_assembly.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Exact regression for the simplified Section VIII half-deficit assembly. + +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, factorial + + +def require(condition: bool, message: str) -> None: + if not condition: + 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) + + +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 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): + 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_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): + 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() + local_ratios = check_exact_local_ratio() + global_ratios = check_global_charged_comparison() + 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" 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") + + +if __name__ == "__main__": + main() diff --git a/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean b/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean index 77bb47c1..1aba689d 100644 --- a/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean +++ b/625/formalization/Erdos625/Section8AttainedAllDeficitReindexing.lean @@ -125,13 +125,14 @@ 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, - fourEndpointCellMultiplicityOfDeficit, - fourEndpointCellFullMultiplicity, e, hab] using hrec + fourEndpointDemandDeficit, + fourEndpointCellFullMultiplicity, e, hab] at hle ⊢ + omega · have hz : demand.1 (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex a) (fourEndpointActualBlockOfAtom alpha hAlpha k slotIndex b) = 0 := by 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 diff --git a/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean b/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean new file mode 100644 index 00000000..7244757f --- /dev/null +++ b/625/formalization/Erdos625/Section8CoarseHalfDeficitCharge.lean @@ -0,0 +1,229 @@ +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 + (card_fourEndpointHalfDeficitAllowed_le alpha hAlpha P) + (by + intro cell deficit hdeficit + 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 + 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. -/ +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 : FourEndpointAbstractBlockSkeleton alpha hAlpha k) + (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 _ + 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 hchoice (reference P)) + +#print axioms nearCellTerm_le_threeQuarterCellBase_pow +#print axioms sum_fourEndpointHalfDeficitChoiceWeight_le_uniform +#print axioms sum_profileCanonicalHighSkeleton_le_uniformHalfDeficitSupportSum + +end + +end Erdos625 diff --git a/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean b/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean new file mode 100644 index 00000000..50f2b4c9 --- /dev/null +++ b/625/formalization/Erdos625/Section8CoarsePhaseCorridor.lean @@ -0,0 +1,174 @@ +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 : + ((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 + 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 + change (5 / 4 : Real) * logOrder n - 19 / 6 ≤ q * (budget : Real) + nlinarith + +/-- 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, + ∀ (hAlpha : 5 < phaseNat n) (i j : Fin 4), + (5 / 4 : Real) * logOrder n - 19 / 6 ≤ + q * (((3 * fourEndpointOverlapSize (phaseNat n) + 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 hAlpha i j + exact five_fourths_log_sub_le_q_mul_endpointBudget + n (phaseNat n) hAlpha 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 diff --git a/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean new file mode 100644 index 00000000..687d557f --- /dev/null +++ b/625/formalization/Erdos625/Section8DirectHalfDeficitAssembly.lean @@ -0,0 +1,279 @@ +import Erdos625.Section8AttainedAllDeficitReindexing +import Erdos625.Section8SharpDeficitProduct +import Erdos625.Section8EndpointAllHighDecoration +import Mathlib.Tactic + +/-! +# Section VIII: direct support/choice assembly over the half-deficit envelope + +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. + +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 + +open scoped BigOperators ENNReal + +noncomputable section + +set_option autoImplicit false + +/-- 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 + fin_cases i <;> fin_cases j <;> + simp [fourEndpointOverlapSize, fourEndpointSize, + fourEndpointCoordinate, fourDeficitCoordinate, fourDeficit] <;> omega + +/-- Positive deficits in the enlarged half-deficit envelope. -/ +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 + +/-- Charged local ratio 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 block matching together with one optional positive deficit in each +selected cell. -/ +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) + +/-- Decode optional choices to the corresponding multiplicity table. -/ +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 dependent deficit data to the optional-choice representation. -/ +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 viewed 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 and dependent-deficit decoders agree. -/ +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 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 encoding recovers the attained abstract demand 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/choice encoding is injective. -/ +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 + +/-- Reference support weight times the exact optional-deficit charge. -/ +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 + +/-- The support/choice sum factors exactly into local 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 + classical + rw [Fintype.sum_sigma] + apply Finset.sum_congr rfl + intro P _ + 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] + +/-- 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)) + (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 + +#print axioms fourEndpointSupportChoiceTable_toChoice_eq +#print axioms fourEndpointDemandSupportChoiceEncoding_injective +#print axioms sum_fourEndpointSupportChoiceChargedWeight_eq +#print axioms sum_profileCanonicalHighSkeleton_le_directSupportChoiceProduct + +end + +end Erdos625 diff --git a/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean new file mode 100644 index 00000000..617f7d38 --- /dev/null +++ b/625/formalization/Erdos625/Section8DirectReferenceGrouping.lean @@ -0,0 +1,170 @@ +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 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 the finite attained-table sum +of `fourEndpointW`. No endpoint transport inequality or asymptotic estimate is +asserted here. +-/ + +namespace Erdos625 + +open scoped BigOperators ENNReal + +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) + {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 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 := + 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 +attained endpoint-table fibres. -/ +def fourEndpointAllDecoratedSupportEquivSigmaTable + (alpha : Nat) (hAlpha : 5 < alpha) + (k : ColoringProfile (alpha + 1)) : + FourEndpointAllDecoratedSupport alpha hAlpha k ≃ + Σ L : FourEndpointAttainedFullTable alpha hAlpha k, + FourEndpointDecoratedBlockPairing alpha hAlpha k L.1 where + toFun z := + 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, hL⟩, ⟨P, hP⟩, decoration⟩ + have htable : 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 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 : FourEndpointAttainedFullTable alpha hAlpha k, + 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) = + ∑ z : FourEndpointAllDecoratedSupport alpha hAlpha k, + 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, + 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] + _ = ∑ 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.1 + +#print axioms fourEndpointAllDecoratedSupportEquivSigmaTable +#print axioms sum_fourEndpointFullSupportReferenceWeight_eq_sum_attained_W + +end + +end Erdos625 diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitENNReal.lean new file mode 100644 index 00000000..2fbcf861 --- /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 + 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 + simpa only [mul_comm] using 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 diff --git a/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean new file mode 100644 index 00000000..ef673560 --- /dev/null +++ b/625/formalization/Erdos625/Section8ExactLocalDeficitRatio.lean @@ -0,0 +1,234 @@ +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 := + 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. -/ +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)] + change d.factorial * + (endpointDeficitDenominator d h * (d + (h + 1))) = + (d + (h + 1)).factorial + 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, mul_comm] + +/-- 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 (Nat.factorial_pos d) (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 m j + 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 (Nat.factorial_pos j) 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 hremain : m - (m - h) = h := by omega + calc + (m + d).descFactorial m = + (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) * + (d + h).descFactorial h := by rw [mul_comm] + +/-- 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, + 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 + calc + x.choose 2 = (x - 1 + 1).choose (1 + 1) := by + simp only [hxrec] + _ = (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 + 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 + 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 +#print axioms localSignRewardNat_deficit_mul_pow +#print axioms lowerUpperCellWeightedCount_deficit_cross_mul + +end + +end Erdos625 diff --git a/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean new file mode 100644 index 00000000..a1bdf39a --- /dev/null +++ b/625/formalization/Erdos625/Section8FiniteBareSkeletonReduction.lean @@ -0,0 +1,193 @@ +import Erdos625.Section8CanonicalThreeQuarterRho +import Erdos625.Section8DirectReferenceGrouping +import Mathlib.Tactic + +/-! +# Section VIII: finite bare-skeleton reduction + +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 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; +* smallness of one explicit sixteen-term quantity. + +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 + +/-- 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)) + (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 : 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 : 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 := + (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, + 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 _ + 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] + _ = (∑ L : FourEndpointAttainedFullTable alpha hAlpha k, + fourEndpointW n alpha hAlpha k L.1) * common := by + 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 + 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, + 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 _ + 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] + _ = (∑ 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 + +end Erdos625 diff --git a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean index 21733164..add238bf 100644 --- a/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean +++ b/625/formalization/Erdos625/Section8FourDeficitProfileCover.lean @@ -18,6 +18,27 @@ 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 + have hnat : coord.val + 1 = target.val + 1 := by + unfold profileClassSize at hclass + exact_mod_cast hclass + apply Fin.ext + 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 +53,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 +74,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 diff --git a/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean b/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean new file mode 100644 index 00000000..4232001f --- /dev/null +++ b/625/formalization/Erdos625/Section8PointwiseChargeProduct.lean @@ -0,0 +1,142 @@ +import Erdos625.Section8NearArithmeticFoundation +import Mathlib.Data.ENNReal.BigOperators +import Mathlib.Tactic + +/-! +# Section VIII: pointwise product reduction + +The remaining charged comparison has two logically independent inputs: + +* 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 +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] + (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, actual c) ≤ ∏ c, full c * localCharge c := by + apply Finset.prod_le_prod' + intro c _ + exact hlocal c + calc + (∏ c, actual c) * actualGlobal ≤ + (∏ 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] + (actual full localRatio : Cell → ENNReal) + (deficit : Cell → Nat) + (actualGlobal fullGlobal base : ENNReal) + (hlocal : ∀ c, actual c ≤ full c * localRatio c) + (hglobal : actualGlobal ≤ + fullGlobal * base ^ (∑ c, deficit c)) : + (∏ c, actual c) * actualGlobal ≤ + ((∏ c, full c) * fullGlobal) * + ∏ c, (base ^ deficit c * localRatio c) := by + have h := finiteProduct_mul_global_le + actual full localRatio actualGlobal 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] + 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 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 : 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 : smallDenom⁻¹ = fullDenom⁻¹ * denominatorLoss n J H := by + unfold denominatorLoss + change smallDenom⁻¹ = fullDenom⁻¹ * (fullDenom / smallDenom) + rw [ENNReal.div_eq_inv_mul] + calc + smallDenom⁻¹ = smallDenom⁻¹ * (fullDenom⁻¹ * fullDenom) := by + rw [ENNReal.inv_mul_cancel hfull0 hfullTop, mul_one] + _ = fullDenom⁻¹ * (smallDenom⁻¹ * fullDenom) := by ac_rfl + rw [hinv] + simpa [mul_comm] using (mul_le_mul_right hloss fullDenom⁻¹) + +/-- Exact aggregate endpoint for the denominator bookkeeping. If each local +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] + (actual full localRatio : Cell → ENNReal) + (deficit : Cell → Nat) + (n J : Nat) + (hdeficit : (∑ c, deficit c) ≤ J) + (hJ : J ≤ n) + (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 + actual 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 + +end Erdos625 diff --git a/625/formalization/Erdos625/Section8SupportProductGrouping.lean b/625/formalization/Erdos625/Section8SupportProductGrouping.lean new file mode 100644 index 00000000..e44e5fd7 --- /dev/null +++ b/625/formalization/Erdos625/Section8SupportProductGrouping.lean @@ -0,0 +1,177 @@ +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) + 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 + (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 + 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 + (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 + 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 + (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 + endpointCellWeightedCount + 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 diff --git a/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean new file mode 100644 index 00000000..2c3ff2c9 --- /dev/null +++ b/625/formalization/Erdos625/Section8SymmetricLocalDeficitRatio.lean @@ -0,0 +1,101 @@ +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 + 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 + have hcell (j : Nat) : + endpointCellWeightedCount u v j = + lowerUpperCellWeightedCount u (v - u) j := by + 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 + 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 + have hcell (j : Nat) : + endpointCellWeightedCount u v j = + lowerUpperCellWeightedCount v (u - v) j := by + 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 + n v (u - v) h hhv hhighv + +#print axioms card_singleCellStubMatching_comm +#print axioms endpointCellWeightedCount_cast_mul_pow_eq_full_mul_nearCellTerm + +end + +end Erdos625 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..75cc8b0d --- /dev/null +++ b/625/proofs/SECTION8_DIRECT_HALF_DEFICIT_SIMPLIFICATION.md @@ -0,0 +1,372 @@ +# 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 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 + +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 direct finite assembly gives + +```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. 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 + +```text +rho(n,m) = n*m / 2^floor((3m-1)/4). +``` + +Under `2h supportTable(P)). +``` + +The total decorated-support space is equivalent to + +```text +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_(attained L) W(L). +``` + +No new cell factorial or block-pairing cardinality formula is required, and no +sum over the infinite type `Nat^(4x4)` is introduced. + +## 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 + +```text +|P| <= total number of row block slots. +``` + +Thus every support may be charged by the same power. Combining direct deficit +summation, the canonical common base, the support-card bound, and direct +reference grouping gives the finite reduction + +```text +sum_(attained demands) weight(demand) +<= +(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. + +## 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: + +1. the middle regime entirely; +2. `allHighDeficitCut` from the global analytic assembly; +3. repeated reconstruction of the global cutoff `U/2`; +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; +8. support-dependent local-base hypotheses; +9. the sharp phase estimate as a necessary prerequisite. + +The analytic assembly now uses only: + +- `2h