Absorb Section 9 into a q-only intrinsic residual split

.github/workflows/erdos625-q-only-attachment-envelope.yml

@@ -0,0 +1,61 @@
+name: Erdős 625 q-only attachment envelope
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean"
+      - "625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean"
+      - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md"
+      - ".github/workflows/erdos625-q-only-attachment-envelope.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-q-only-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean \
+            625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean; then
+            exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build q-only two-regime assembly warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9QOnlyTwoRegimeAssembly --wfail \
+            > /tmp/q-only-envelope-lean.log 2>&1
+          status=$?
+          tail -n 380 /tmp/q-only-envelope-lean.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: section9-q-only-envelope-lean-log
+          path: /tmp/q-only-envelope-lean.log
+          if-no-files-found: ignore

625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean

@@ -0,0 +1,160 @@
+import Erdos625.Section9MatchingRestrictionEnvelope
+import Mathlib.Tactic
+
+/-!
+# Section IX: absorb the local increment product into the residual-q mass
+
+The direct matching-restriction route initially keeps two products: one for the
+unselected local increments `residualLambda`, and one for the selected-edge
+weight `residualQ`.  Since
+
+`residualQ = theta^2 / 2 + residualLambda`
+
+outside the exposed matching (and both quantities vanish on it), the lambda
+mass is pointwise dominated by the q mass.  Consequently both products are
+controlled by the same total q sum.  This removes the separate cubic
+`U^4 / m` estimate from the final finite attachment envelope.
+-/
+
+universe u v
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- The local-increment weight is pointwise dominated by the selected-edge
+weight. -/
+theorem residualLambda_le_residualQ
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (M : Finset (A × B)) (R : ℕ) (row : A → ℕ) (col : B → ℕ)
+    (a : A) (b : B) :
+    residualLambda M R row col a b ≤ residualQ M R row col a b := by
+  classical
+  unfold residualQ residualLambda
+  by_cases hM : (a, b) ∈ M
+  · simp [hM]
+  · simp only [hM, if_false]
+    exact le_add_of_nonneg_left (by positivity)
+
+/-- If `lambda` is pointwise bounded by `q`, then the lambda product and the
+direct outside-matching q product are jointly bounded by twice one total q
+mass. -/
+theorem lambda_matching_products_le_exp_two_q_bound
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (lambda q : A → B → ENNReal) (M : Finset (A × B))
+    (qBound : ENNReal)
+    (hlq : ∀ a b, lambda a b ≤ q a b)
+    (hqall : (∑ a, ∑ b, q a b) ≤ qBound) :
+    ((∏ a, ∏ b, (1 + lambda a b)) *
+      (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        (1 + q e.1 e.2))) ≤
+      EReal.exp (((2 * qBound : ENNReal) : EReal)) := by
+  have hlambda : (∑ a, ∑ b, lambda a b) ≤ qBound := by
+    apply le_trans _ hqall
+    exact Finset.sum_le_sum fun a _ =>
+      Finset.sum_le_sum fun b _ => hlq a b
+  have hqOutside :
+      (∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        q e.1 e.2) ≤ qBound := by
+    apply le_trans _ hqall
+    calc
+      (∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          q e.1 e.2) ≤
+        ∑ e ∈ (Finset.univ : Finset (A × B)), q e.1 e.2 := by
+          exact Finset.sum_le_sum_of_subset Finset.sdiff_subset
+      _ = ∑ e : A × B, q e.1 e.2 := by simp
+      _ = ∑ a, ∑ b, q a b := by
+        rw [Fintype.sum_prod_type']
+  have h := lambda_matching_products_le_exp_of_sum_bounds
+    lambda q M qBound qBound hlambda hqOutside
+  simpa [two_mul] using h
+
+/-- Natural ceiling of one third, written without introducing a dependency on
+later Section X utilities. -/
+def residualCeilThird (U : Nat) : Nat := (U + 2) / 3
+
+/-- The ceiling-third exponent covers `U`. -/
+theorem le_three_mul_residualCeilThird (U : Nat) :
+    U ≤ 3 * residualCeilThird U := by
+  unfold residualCeilThird
+  omega
+
+/-- If the quadratic large-residual hypothesis fails, the residual mass is
+already below the natural power threshold `2^(ceil(U/3))`.  This gives an
+intrinsic alternative to splitting at `n / (log n)^6`. -/
+theorem residualMass_lt_two_pow_ceilThird_of_not_cube
+    (U m : Nat) (hnot : ¬ 2 ^ U ≤ m ^ 3) :
+    m < 2 ^ residualCeilThird U := by
+  by_contra h
+  have hm : 2 ^ residualCeilThird U ≤ m := Nat.le_of_not_gt h
+  have hcube : (2 ^ residualCeilThird U) ^ 3 ≤ m ^ 3 :=
+    pow_le_pow_left' hm 3
+  have hpow : 2 ^ U ≤ 2 ^ (3 * residualCeilThird U) :=
+    pow_le_pow_right₀ (by decide) (le_three_mul_residualCeilThird U)
+  apply hnot
+  calc
+    2 ^ U ≤ 2 ^ (3 * residualCeilThird U) := hpow
+    _ = (2 ^ residualCeilThird U) ^ 3 := by
+      rw [Nat.mul_comm, pow_mul]
+    _ ≤ m ^ 3 := hcube
+
+/-- One absolute finite constant bounds the literal cap/no-return attachment
+numerator at scale `U^2`.  No separate lambda-total or cubic degree-moment
+estimate is needed. -/
+theorem exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope :
+    ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧
+      ∀ {A : Type u} {B : Type v} [Fintype A] [Fintype B]
+          [DecidableEq A] [DecidableEq B]
+          (M : Finset (A × B)) (U m : ℕ)
+          (row : A → ℕ) (col : B → ℕ)
+          (htotal : Finset.univ.sum row = Finset.univ.sum col),
+        IsBipartiteMatching M →
+        0 < m →
+        (∑ a, row a) = m →
+        (∑ b, col b) = m →
+        (∀ a, row a ≤ U) →
+        (∀ b, col b ≤ U) →
+        2 ^ U ≤ m ^ 3 →
+        residualActualAttachmentNumerator M (U / 2) row col htotal ≤
+          EReal.exp ((((kappa * (U : ENNReal) ^ 2 : ENNReal)) : EReal)) := by
+  obtain ⟨kappaQ, hkQpos, hkQtop, hkQ⟩ :=
+    existsAbsoluteResidualQTotalBound_of_degreeCaps
+  let kappa : ENNReal := 2 * kappaQ
+  have hkappaPos : 0 < kappa := by
+    dsimp [kappa]
+    positivity
+  have hkappaTop : kappa ≠ ∞ := by
+    dsimp [kappa]
+    exact ENNReal.mul_ne_top ENNReal.ofNat_ne_top hkQtop
+  refine ⟨kappa, hkappaPos, hkappaTop, ?_⟩
+  intro A B _ _ _ _ M U m row col htotal hM hm hrow hcol
+    hrowCap hcolCap hpow
+  have hbridge :=
+    residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct
+      M (U / 2) row col htotal (by simpa [hrow] using hm) hM
+  have hqAll :=
+    hkQ M U (U / 2) m row col hm hrow hcol hrowCap hcolCap rfl hpow
+  have hproduct := lambda_matching_products_le_exp_two_q_bound
+    (residualLambda M (U / 2) row col)
+    (residualQ M (U / 2) row col) M
+    (kappaQ * (U : ENNReal) ^ 2)
+    (residualLambda_le_residualQ M (U / 2) row col)
+    hqAll
+  exact hbridge.trans (by
+    simpa [kappa, mul_assoc] using hproduct)
+
+#print axioms residualLambda_le_residualQ
+#print axioms lambda_matching_products_le_exp_two_q_bound
+#print axioms le_three_mul_residualCeilThird
+#print axioms residualMass_lt_two_pow_ceilThird_of_not_cube
+#print axioms exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope
+
+end
+
+end Erdos625

625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean

@@ -0,0 +1,86 @@
+import Erdos625.Section9ProfileAttachmentQOnly
+import Erdos625.Section9SmallResidualAttachmentBound
+import Erdos625.Section8ProfileSkeletonWeight
+import Mathlib.Tactic
+
+/-!
+# Section IX: intrinsic finite residual dichotomy
+
+The q-only estimate requires exactly `2^U <= m^3`.  Rather than introduce an
+external cutoff in `m`, this module splits on that finite proposition itself.
+Its negation forces `m < 2^(ceil(U/3))`, where the deterministic residual bound
+applies directly.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- One absolute q-only constant gives an exact finite dichotomy for every
+attained profile high skeleton.
+
+In the quadratic branch the attachment is bounded by `exp(kappa * U^2)`.  In
+the complementary branch the residual mass is below `2^(ceil(U/3))` and the
+literal deterministic bound `2^(U*m/2)` is retained. -/
+theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split :
+    ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧
+      ∀ {b n : ℕ} {k : ColoringProfile b}
+          (row0 : OrderedProfilePartition n k) (U : ℕ)
+          (_hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
+          (demand : ProfileCanonicalHighSkeleton k U),
+        let m := canonicalDemandResidualTotal
+          (profileBlockMargin k) (profileBlockMargin k) U demand
+        (2 ^ U ≤ m ^ 3 ∧
+          profileHighSkeletonAttachment row0 U demand ≤
+            EReal.exp ((((kappa * (U : ENNReal) ^ 2 : ENNReal)) : EReal))) ∨
+        (¬ 2 ^ U ≤ m ^ 3 ∧
+          m < 2 ^ residualCeilThird U ∧
+          profileHighSkeletonAttachment row0 U demand ≤
+            (2 : ENNReal) ^ (U * m / 2)) := by
+  obtain ⟨kappa, hkpos, hktop, hlarge⟩ :=
+    exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope
+  refine ⟨kappa, hkpos, hktop, ?_⟩
+  intro b n k row0 U hcap demand
+  dsimp only
+  let m := canonicalDemandResidualTotal
+    (profileBlockMargin k) (profileBlockMargin k) U demand
+  by_cases hpow : 2 ^ U ≤ m ^ 3
+  · left
+    have hmpos : 0 < m := by
+      by_contra hm
+      have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm
+      have hm3 : m ^ 3 = 0 := by rw [hm0]; norm_num
+      rw [hm3] at hpow
+      exact (Nat.not_lt_of_ge hpow) (pow_pos (by decide) U)
+    exact ⟨hpow, hlarge row0 U m hcap demand rfl hmpos hpow⟩
+  · right
+    have hmass := residualMass_lt_two_pow_ceilThird_of_not_cube U m hpow
+    let witness := canonicalDemandReferenceWitness
+      (profileBlockMargin k) (profileBlockMargin k) U demand
+    have hmatching :
+        IsBipartiteMatching (positiveDemandSupport demand.1) :=
+      profileHighSkeleton_positiveSupport_isBipartiteMatching k U hcap demand
+    have htotal :
+        (∑ a, residualRowDegree witness a) =
+          ∑ a, residualColumnDegree witness a :=
+      sum_residualRowDegree_eq_sum_residualColumnDegree
+        (profileBlockMargin_total_eq_self row0) witness
+    have hrowSum : (∑ a, residualRowDegree witness a) = m := by
+      simp only [m, canonicalDemandResidualTotal, witness]
+    have hsmall := residualActualAttachmentNumerator_le_two_pow_of_small_mass
+      (positiveDemandSupport demand.1) (U / 2) U m
+      (residualRowDegree witness) (residualColumnDegree witness)
+      htotal hmatching rfl hrowSum
+    refine ⟨hpow, hmass, ?_⟩
+    unfold profileHighSkeletonAttachment
+    simpa only [m, witness] using hsmall
+
+#print axioms exists_absolute_profileHighSkeletonAttachment_intrinsic_split
+
+end
+
+end Erdos625