From 1f11f8a4118737dab81cee879ef54a653604ef2c Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:48:10 +0300
Subject: [PATCH 01/25] Add q-only matching-restriction attachment envelope

---
 .../Section9MatchingRestrictionQOnly.lean     | 130 ++++++++++++++++++
 1 file changed, 130 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean

diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
new file mode 100644
index 00000000..7e4e70ff
--- /dev/null
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
@@ -0,0 +1,130 @@
+import Erdos625.Section9MatchingRestrictionEnvelope
+import Mathlib.Tactic
+
+/-!
+# Section IX: absorb the local increment product into the residual-q mass
+
+The direct matching-restriction route initially keeps two products: one for the
+unselected local increments `residualLambda`, and one for the selected-edge
+weight `residualQ`.  Since
+
+`residualQ = theta^2 / 2 + residualLambda`
+
+outside the exposed matching (and both quantities vanish on it), the lambda
+mass is pointwise dominated by the q mass.  Consequently both products are
+controlled by the same total q sum.  This removes the separate cubic
+`U^4 / m` estimate from the final finite attachment envelope.
+-/
+
+universe u v
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- The local-increment weight is pointwise dominated by the selected-edge
+weight. -/
+theorem residualLambda_le_residualQ
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (M : Finset (A × B)) (R : ℕ) (row : A → ℕ) (col : B → ℕ)
+    (a : A) (b : B) :
+    residualLambda M R row col a b ≤ residualQ M R row col a b := by
+  classical
+  unfold residualQ
+  by_cases hM : (a, b) ∈ M
+  · simp [hM]
+  · simp only [hM, if_false]
+    exact le_add_left (residualLambda M R row col a b)
+      (configurationCellTheta row col (Finset.univ.sum row) a b ^ 2 / 2)
+
+/-- If `lambda` is pointwise bounded by `q`, then the lambda product and the
+direct outside-matching q product are jointly bounded by twice one total q
+mass. -/
+theorem lambda_matching_products_le_exp_two_q_bound
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (lambda q : A → B → ENNReal) (M : Finset (A × B))
+    (qBound : ENNReal)
+    (hlq : ∀ a b, lambda a b ≤ q a b)
+    (hqall : (∑ a, ∑ b, q a b) ≤ qBound) :
+    ((∏ a, ∏ b, (1 + lambda a b)) *
+      (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        (1 + q e.1 e.2))) ≤
+      EReal.exp (((2 * qBound : ENNReal) : EReal)) := by
+  have hlambda : (∑ a, ∑ b, lambda a b) ≤ qBound := by
+    apply le_trans _ hqall
+    exact Finset.sum_le_sum fun a _ =>
+      Finset.sum_le_sum fun b _ => hlq a b
+  have hqOutside :
+      (∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        q e.1 e.2) ≤ qBound := by
+    apply le_trans _ hqall
+    calc
+      (∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          q e.1 e.2) ≤
+        ∑ e ∈ (Finset.univ : Finset (A × B)), q e.1 e.2 := by
+          exact Finset.sum_le_sum_of_subset Finset.sdiff_subset
+      _ = ∑ e : A × B, q e.1 e.2 := by simp
+      _ = ∑ a, ∑ b, q a b := by
+        rw [Fintype.sum_prod_type']
+  have h := lambda_matching_products_le_exp_of_sum_bounds
+    lambda q M qBound qBound hlambda hqOutside
+  simpa [two_mul] using h
+
+/-- One absolute finite constant bounds the literal cap/no-return attachment
+numerator at scale `U^2`.  No separate lambda-total or cubic degree-moment
+estimate is needed. -/
+theorem exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope :
+    ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧
+      ∀ {A : Type u} {B : Type v} [Fintype A] [Fintype B]
+          [DecidableEq A] [DecidableEq B]
+          (M : Finset (A × B)) (U m : ℕ)
+          (row : A → ℕ) (col : B → ℕ)
+          (htotal : Finset.univ.sum row = Finset.univ.sum col),
+        IsBipartiteMatching M →
+        0 < m →
+        (∑ a, row a) = m →
+        (∑ b, col b) = m →
+        (∀ a, row a ≤ U) →
+        (∀ b, col b ≤ U) →
+        2 ^ U ≤ m ^ 3 →
+        residualActualAttachmentNumerator M (U / 2) row col htotal ≤
+          EReal.exp ((((kappa * (U : ENNReal) ^ 2 : ENNReal)) : EReal)) := by
+  obtain ⟨kappaQ, hkQpos, hkQtop, hkQ⟩ :=
+    existsAbsoluteResidualQTotalBound_of_degreeCaps
+  let kappa : ENNReal := 2 * kappaQ
+  have hkappaPos : 0 < kappa := by
+    dsimp [kappa]
+    positivity
+  have hkappaTop : kappa ≠ ∞ := by
+    dsimp [kappa]
+    exact ENNReal.mul_ne_top ENNReal.ofNat_ne_top hkQtop
+  refine ⟨kappa, hkappaPos, hkappaTop, ?_⟩
+  intro A B _ _ _ _ M U m row col htotal hM hm hrow hcol
+    hrowCap hcolCap hpow
+  have hbridge :=
+    residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct
+      M (U / 2) row col htotal (by simpa [hrow] using hm) hM
+  have hqAll :=
+    hkQ M U (U / 2) m row col hm hrow hcol hrowCap hcolCap rfl hpow
+  have hproduct := lambda_matching_products_le_exp_two_q_bound
+    (residualLambda M (U / 2) row col)
+    (residualQ M (U / 2) row col) M
+    (kappaQ * (U : ENNReal) ^ 2)
+    (residualLambda_le_residualQ M (U / 2) row col)
+    hqAll
+  exact hbridge.trans (by
+    simpa [kappa, mul_assoc] using hproduct)
+
+#print axioms residualLambda_le_residualQ
+#print axioms lambda_matching_products_le_exp_two_q_bound
+#print axioms exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope
+
+end
+
+end Erdos625

From f593ec27bc5ff5c85d1aaff9cf4a505d7387a5bd Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:48:28 +0300
Subject: [PATCH 02/25] Add focused q-only attachment Lean workflow

---
 .../erdos625-q-only-attachment-envelope.yml   | 51 +++++++++++++++++++
 1 file changed, 51 insertions(+)
 create mode 100644 .github/workflows/erdos625-q-only-attachment-envelope.yml

diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml
new file mode 100644
index 00000000..cc4d9059
--- /dev/null
+++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml
@@ -0,0 +1,51 @@
+name: Erdős 625 q-only attachment envelope
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean"
+      - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md"
+      - ".github/workflows/erdos625-q-only-attachment-envelope.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean; then
+            exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build q-only endpoint and dependency closure warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9MatchingRestrictionQOnly --wfail \
+            > /tmp/q-only-envelope-lean.log 2>&1
+          status=$?
+          tail -n 260 /tmp/q-only-envelope-lean.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: section9-q-only-envelope-lean-log
+          path: /tmp/q-only-envelope-lean.log
+          if-no-files-found: ignore

From d0f95b59be822d60f4ba6130428f93d9585b74d3 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:48:45 +0300
Subject: [PATCH 03/25] Document q-only attachment envelope audit boundary

---
 .../Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md       | 68 +++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md

diff --git a/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md
new file mode 100644
index 00000000..3f95ac36
--- /dev/null
+++ b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md
@@ -0,0 +1,68 @@
+# Audit: q-only matching-restriction attachment envelope
+
+## Purpose
+
+This follow-up isolates one additional simplification of the direct Section 9
+route.  The preceding branch bounds the literal residual attachment by a
+product of local-increment factors and a direct outside-matching `q` product.
+Here those two products are charged to the same total `q` mass.
+
+Outside the exposed matching,
+
+\[
+q_{ab}=\frac{\theta_{ab}^2}{2}+\lambda_{ab},
+\]
+
+and both quantities vanish on the matching.  Hence
+\(\lambda_{ab}\le q_{ab}\) cellwise.  The accepted total bound
+
+\[
+\sum_{a,b}q_{ab}\le \kappa_Q U^2
+\]
+
+therefore controls both products, giving
+
+\[
+\mathcal A(M,j)
+ \le \exp\!\left(2\sum_{a,b}q_{ab}\right)
+ \le \exp(\kappa U^2).
+\]
+
+## New declarations
+
+`Erdos625/Section9MatchingRestrictionQOnly.lean` proves:
+
+1. `residualLambda_le_residualQ`;
+2. `lambda_matching_products_le_exp_two_q_bound`;
+3. `exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope`.
+
+The last theorem is pointwise in the finite residual data and concerns the
+literal cap/no-return numerator.  It has no separate `U^4/m` term, no cubic
+degree moment, no cycle traversal, and no dependence on the number of profile
+blocks or matching edges.
+
+## Reused inputs
+
+- the exact fixed-family Fubini identity;
+- the matching-restriction product theorem;
+- the direct lambda/q product bridge;
+- the already checked quadratic total-q estimate.
+
+## Trust gates
+
+The focused workflow rejects placeholders, project-defined axioms/constants,
+and `unsafe`; it then builds the new module and its dependency closure under
+the pinned Lean 4.31/mathlib project with warnings fatal.  The source prints
+the axioms of every new public theorem.
+
+## Deliberate boundary
+
+This PR does not by itself:
+
+- rewrite the canonical manuscript;
+- sum the Section 8 skeleton weights;
+- combine the large and small residual regimes;
+- prove Proposition 9.2 or `Erdos625Statement`.
+
+Its role is to remove a redundant analytic branch from the large-residual
+attachment estimate before manuscript integration.

From 095288e9bc45c21b5360605d85944f48bef446e7 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 09:56:16 +0300
Subject: [PATCH 04/25] Fix q-only pointwise domination proof

---
 .../Erdos625/Section9MatchingRestrictionQOnly.lean           | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
index 7e4e70ff..f0c0b59a 100644
--- a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
@@ -35,12 +35,11 @@ theorem residualLambda_le_residualQ
     (a : A) (b : B) :
     residualLambda M R row col a b ≤ residualQ M R row col a b := by
   classical
-  unfold residualQ
+  unfold residualQ residualLambda
   by_cases hM : (a, b) ∈ M
   · simp [hM]
   · simp only [hM, if_false]
-    exact le_add_left (residualLambda M R row col a b)
-      (configurationCellTheta row col (Finset.univ.sum row) a b ^ 2 / 2)
+    exact le_add_of_nonneg_left (by positivity)
 
 /-- If `lambda` is pointwise bounded by `q`, then the lambda product and the
 direct outside-matching q product are jointly bounded by twice one total q

From b1d370fe7e52cfe98a6929fd00a432be8ab1a679 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:04:04 +0300
Subject: [PATCH 05/25] Add natural residual power dichotomy

---
 .../Section9MatchingRestrictionQOnly.lean     | 31 +++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
index f0c0b59a..5d9c5be6 100644
--- a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
@@ -75,6 +75,35 @@ theorem lambda_matching_products_le_exp_two_q_bound
     lambda q M qBound qBound hlambda hqOutside
   simpa [two_mul] using h
 
+/-- Natural ceiling of one third, written without introducing a dependency on
+later Section X utilities. -/
+def residualCeilThird (U : Nat) : Nat := (U + 2) / 3
+
+/-- The ceiling-third exponent covers `U`. -/
+theorem le_three_mul_residualCeilThird (U : Nat) :
+    U ≤ 3 * residualCeilThird U := by
+  unfold residualCeilThird
+  omega
+
+/-- If the quadratic large-residual hypothesis fails, the residual mass is
+already below the natural power threshold `2^(ceil(U/3))`.  This gives an
+intrinsic alternative to splitting at `n / (log n)^6`. -/
+theorem residualMass_lt_two_pow_ceilThird_of_not_cube
+    (U m : Nat) (hnot : ¬ 2 ^ U ≤ m ^ 3) :
+    m < 2 ^ residualCeilThird U := by
+  by_contra h
+  have hm : 2 ^ residualCeilThird U ≤ m := Nat.le_of_not_gt h
+  have hcube : (2 ^ residualCeilThird U) ^ 3 ≤ m ^ 3 :=
+    pow_le_pow_left' hm 3
+  have hpow : 2 ^ U ≤ 2 ^ (3 * residualCeilThird U) :=
+    pow_le_pow_right₀ (by decide) (le_three_mul_residualCeilThird U)
+  apply hnot
+  calc
+    2 ^ U ≤ 2 ^ (3 * residualCeilThird U) := hpow
+    _ = (2 ^ residualCeilThird U) ^ 3 := by
+      rw [Nat.mul_comm, pow_mul]
+    _ ≤ m ^ 3 := hcube
+
 /-- One absolute finite constant bounds the literal cap/no-return attachment
 numerator at scale `U^2`.  No separate lambda-total or cubic degree-moment
 estimate is needed. -/
@@ -122,6 +151,8 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope :
 
 #print axioms residualLambda_le_residualQ
 #print axioms lambda_matching_products_le_exp_two_q_bound
+#print axioms le_three_mul_residualCeilThird
+#print axioms residualMass_lt_two_pow_ceilThird_of_not_cube
 #print axioms exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope
 
 end

From fb59f846a7cf90cd8e4fcddd1623e7c0755c7789 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:05:05 +0300
Subject: [PATCH 06/25] Document the natural Section 9 power split

---
 .../Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md       | 43 +++++++++++++++++--
 1 file changed, 40 insertions(+), 3 deletions(-)

diff --git a/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md
index 3f95ac36..588bac05 100644
--- a/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md
+++ b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md
@@ -34,13 +34,48 @@ therefore controls both products, giving
 
 1. `residualLambda_le_residualQ`;
 2. `lambda_matching_products_le_exp_two_q_bound`;
-3. `exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope`.
+3. `le_three_mul_residualCeilThird`;
+4. `residualMass_lt_two_pow_ceilThird_of_not_cube`;
+5. `exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope`.
 
 The last theorem is pointwise in the finite residual data and concerns the
 literal cap/no-return numerator.  It has no separate `U^4/m` term, no cubic
 degree moment, no cycle traversal, and no dependence on the number of profile
 blocks or matching edges.
 
+## A more intrinsic two-regime split
+
+The finite q-only theorem naturally assumes
+
+\[
+2^U\le m^3.
+\]
+
+There is no need to introduce the manuscript cutoff
+\(m=n/(\log n)^6\) at the finite combinatorial level.  The Lean theorem
+`residualMass_lt_two_pow_ceilThird_of_not_cube` proves the exact complementary
+statement
+
+\[
+2^U\nleq m^3
+\quad\Longrightarrow\quad
+m<2^{\lceil U/3\rceil},
+\qquad
+\lceil U/3\rceil=\frac{U+2}{3}.
+\]
+
+Thus Section 9 may eventually be organized around the intrinsic dichotomy:
+
+- **quadratic regime:** `2^U <= m^3`, use the q-only envelope
+  `exp(O(U^2))`;
+- **small-power regime:** `2^U > m^3`, use the deterministic bound together
+  with `m < 2^(ceil(U/3))`.
+
+At the midpoint phase, `U=(2+o(1)) log_2 n`, so the second exponent is of order
+at most `U 2^(ceil(U/3)) = n^(2/3+o(1))`, still
+`o(n/(log n)^4)`.  That asymptotic specialization is not asserted by this PR;
+only the exact finite dichotomy is kernel-checked here.
+
 ## Reused inputs
 
 - the exact fixed-family Fubini identity;
@@ -61,8 +96,10 @@ This PR does not by itself:
 
 - rewrite the canonical manuscript;
 - sum the Section 8 skeleton weights;
-- combine the large and small residual regimes;
+- prove the phase-asymptotic small-power estimate;
+- combine both residual regimes in the profile-level second moment;
 - prove Proposition 9.2 or `Erdos625Statement`.
 
 Its role is to remove a redundant analytic branch from the large-residual
-attachment estimate before manuscript integration.
+attachment estimate and to expose a cleaner finite regime split before
+manuscript integration.

From 8808f03fc67397725b189222732830a1698b999b Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:06:19 +0300
Subject: [PATCH 07/25] Specialize the q-only envelope to attained profiles

---
 .../Section9ProfileAttachmentQOnly.lean       | 139 ++++++++++++++++++
 1 file changed, 139 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
new file mode 100644
index 00000000..e0a1bb0b
--- /dev/null
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
@@ -0,0 +1,139 @@
+import Erdos625.Section9MatchingRestrictionQOnly
+import Erdos625.Section9CanonicalDemandProductSpecialization
+import Erdos625.Section8ProfileSkeletonWeight
+import Erdos625.Section9ERealENNRealExpTransport
+import Erdos625.PhaseEstimates
+import Mathlib.Tactic
+
+/-!
+# Section IX: attained-profile q-only attachment endpoint
+
+This module transports the q-only finite residual bound to every attained
+canonical high skeleton and then specializes the exponent to the phase scale.
+The large branch is stated using its intrinsic finite hypothesis
+`2^U <= m^3`; no artificial `n / (log n)^6` cutoff is needed here.
+-/
+
+namespace Erdos625
+
+open Filter
+open scoped BigOperators ENNReal Topology
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- One absolute q-only constant controls every attained profile high-skeleton
+attachment whenever its residual mass satisfies the finite quadratic regime. -/
+theorem exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope :
+    ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧
+      ∀ {b n : ℕ} {k : ColoringProfile b}
+          (row0 : OrderedProfilePartition n k) (U m : ℕ)
+          (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
+          (demand : ProfileCanonicalHighSkeleton k U),
+        m = canonicalDemandResidualTotal
+          (profileBlockMargin k) (profileBlockMargin k) U demand →
+        0 < m →
+        2 ^ U ≤ m ^ 3 →
+        profileHighSkeletonAttachment row0 U demand ≤
+          EReal.exp ((((kappa * (U : ENNReal) ^ 2 : ENNReal)) : EReal)) := by
+  obtain ⟨kappa, hkpos, hktop, hbound⟩ :=
+    exists_absolute_residualActualAttachmentNumerator_le_qOnlyEnvelope
+  refine ⟨kappa, hkpos, hktop, ?_⟩
+  intro b n k row0 U m hcap demand hm hmpos hpow
+  let witness := canonicalDemandReferenceWitness
+    (profileBlockMargin k) (profileBlockMargin k) U demand
+  have hparameters := canonicalReference_residual_parameters
+    (profileBlockMargin k) (profileBlockMargin k) U
+    (profileBlockMargin_total_eq_self row0) hcap hcap demand
+  have hrowSum : (∑ a, residualRowDegree witness a) = m := by
+    simpa only [canonicalDemandResidualTotal, witness] using hm.symm
+  have hcolSum : (∑ a, residualColumnDegree witness a) = m := by
+    exact hparameters.2.2.2.symm.trans hrowSum
+  have hactual := hbound (positiveDemandSupport demand.1) U m
+    (residualRowDegree witness) (residualColumnDegree witness)
+    (sum_residualRowDegree_eq_sum_residualColumnDegree
+      (profileBlockMargin_total_eq_self row0) witness)
+    hparameters.1 hmpos hrowSum hcolSum hparameters.2.1 hparameters.2.2.1 hpow
+  unfold profileHighSkeletonAttachment
+  simpa only [witness] using hactual
+
+/-- The q-only exponent is finite for every finite constant and natural cap. -/
+theorem qOnlyEnvelope_ne_top
+    (kappa : ENNReal) (U : Nat) (hkappaTop : kappa ≠ ∞) :
+    kappa * (U : ENNReal) ^ 2 ≠ ∞ :=
+  ENNReal.mul_ne_top hkappaTop
+    (ENNReal.pow_ne_top (ENNReal.natCast_ne_top U))
+
+/-- In the intrinsic quadratic regime, every attained profile high-skeleton
+attachment is uniformly `exp(O((log n)^2))`. -/
+theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale :
+    ∃ C : ℝ, 0 ≤ C ∧
+      ∀ᶠ n : ℕ in atTop,
+        ∀ {b : ℕ} {k : ColoringProfile b}
+          (row0 : OrderedProfilePartition n k) (U : ℕ),
+          U ≤ phaseNat n →
+          (∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U) →
+          ∀ demand : ProfileCanonicalHighSkeleton k U,
+            2 ^ U ≤
+              (canonicalDemandResidualTotal (profileBlockMargin k)
+                (profileBlockMargin k) U demand) ^ 3 →
+            profileHighSkeletonAttachment row0 U demand ≤
+              ENNReal.ofReal
+                (Real.exp (C * Real.log (n : ℝ) ^ 2)) := by
+  obtain ⟨kappa, hkpos, hktop, hfinite⟩ :=
+    exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope
+  let C : ℝ := kappa.toReal * 4 ^ 2
+  have hC : 0 ≤ C := by
+    dsimp [C]
+    positivity
+  refine ⟨C, hC, ?_⟩
+  filter_upwards
+    [eventually_logOrder_le_phaseNat_and_phaseNat_le_four_logOrder,
+      eventually_gt_atTop (1 : ℕ)] with n hphase hn
+  intro b k row0 U hU hcap demand hpow
+  let m := canonicalDemandResidualTotal (profileBlockMargin k)
+    (profileBlockMargin k) U demand
+  have hmpos : 0 < m := by
+    by_contra hm
+    have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm
+    subst m
+    simp at hpow
+  have hbase := hfinite row0 U m hcap demand rfl hmpos hpow
+  let exponent : ENNReal := kappa * (U : ENNReal) ^ 2
+  have hexponent : exponent ≠ ∞ := by
+    exact qOnlyEnvelope_ne_top kappa U hktop
+  have hbaseReal :
+      profileHighSkeletonAttachment row0 U demand ≤
+        ENNReal.ofReal (Real.exp exponent.toReal) := by
+    apply ennreal_le_of_coe_le_ereal_exp_toReal _ _ hexponent
+    exact EReal.coe_ennreal_le_coe_ennreal_iff.mpr hbase
+  apply hbaseReal.trans
+  apply ENNReal.ofReal_le_ofReal
+  apply Real.exp_le_exp.mpr
+  have hlog : 0 < Real.log (n : ℝ) := Real.log_pos (by exact_mod_cast hn)
+  have hUreal : (U : ℝ) ≤ 4 * Real.log (n : ℝ) :=
+    (Nat.cast_le.mpr hU).trans hphase.2
+  have hU2 : (U : ℝ) ^ 2 ≤ (4 * Real.log (n : ℝ)) ^ 2 :=
+    pow_le_pow_left₀ (Nat.cast_nonneg U) hUreal 2
+  have hbound : kappa.toReal * (U : ℝ) ^ 2 ≤
+      C * Real.log (n : ℝ) ^ 2 := by
+    calc
+      kappa.toReal * (U : ℝ) ^ 2 ≤
+          kappa.toReal * (4 * Real.log (n : ℝ)) ^ 2 :=
+        mul_le_mul_of_nonneg_left hU2 ENNReal.toReal_nonneg
+      _ = C * Real.log (n : ℝ) ^ 2 := by
+        simp [C]
+        ring
+  have hexponentReal : exponent.toReal = kappa.toReal * (U : ℝ) ^ 2 := by
+    simp [exponent, hktop]
+  rw [hexponentReal]
+  exact hbound
+
+#print axioms exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope
+#print axioms qOnlyEnvelope_ne_top
+#print axioms eventually_profileHighSkeletonAttachment_le_qOnly_logScale
+
+end
+
+end Erdos625

From d7911a510becbae4eea72332beb39f0bcd419738 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:06:50 +0300
Subject: [PATCH 08/25] Validate the attained-profile q-only endpoint

---
 .../workflows/erdos625-q-only-attachment-envelope.yml  | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml
index cc4d9059..47c39a7a 100644
--- a/.github/workflows/erdos625-q-only-attachment-envelope.yml
+++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml
@@ -4,6 +4,7 @@ on:
   pull_request:
     paths:
       - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean"
       - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md"
       - ".github/workflows/erdos625-q-only-attachment-envelope.yml"
   workflow_dispatch:
@@ -21,7 +22,8 @@ jobs:
         run: |
           if grep -nE \
             '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
-            625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean; then
+            625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean; then
             exit 1
           fi
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
@@ -32,15 +34,15 @@ jobs:
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Build q-only endpoint and dependency closure warning-fatally
+      - name: Build attained-profile q-only endpoint warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
           set +e
-          lake build Erdos625.Section9MatchingRestrictionQOnly --wfail \
+          lake build Erdos625.Section9ProfileAttachmentQOnly --wfail \
             > /tmp/q-only-envelope-lean.log 2>&1
           status=$?
-          tail -n 260 /tmp/q-only-envelope-lean.log
+          tail -n 300 /tmp/q-only-envelope-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()

From 892c413daf44c14e8039b4454eff2b418874440e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:20:05 +0300
Subject: [PATCH 09/25] Fix q-only profile positivity and warning-fatal lint

---
 .../Erdos625/Section9ProfileAttachmentQOnly.lean          | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
index e0a1bb0b..5d2f11a9 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
@@ -29,7 +29,7 @@ theorem exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope :
     ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧
       ∀ {b n : ℕ} {k : ColoringProfile b}
           (row0 : OrderedProfilePartition n k) (U m : ℕ)
-          (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
+          (_hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
           (demand : ProfileCanonicalHighSkeleton k U),
         m = canonicalDemandResidualTotal
           (profileBlockMargin k) (profileBlockMargin k) U demand →
@@ -97,8 +97,8 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale :
   have hmpos : 0 < m := by
     by_contra hm
     have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm
-    subst m
-    simp at hpow
+    have htwoPos : 0 < (2 : Nat) ^ U := pow_pos (by decide) U
+    exact (not_le_of_gt htwoPos) (by simpa [hm0] using hpow)
   have hbase := hfinite row0 U m hcap demand rfl hmpos hpow
   let exponent : ENNReal := kappa * (U : ENNReal) ^ 2
   have hexponent : exponent ≠ ∞ := by
@@ -126,7 +126,7 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale :
         simp [C]
         ring
   have hexponentReal : exponent.toReal = kappa.toReal * (U : ℝ) ^ 2 := by
-    simp [exponent, hktop]
+    simp [exponent]
   rw [hexponentReal]
   exact hbound
 

From 6eb80a228aeae38b021d47ac406fa9e64d6bfeae Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:32:20 +0300
Subject: [PATCH 10/25] Add the intrinsic profile residual dichotomy

---
 ...ction9ProfileAttachmentIntrinsicSplit.lean | 84 +++++++++++++++++++
 1 file changed, 84 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean

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

From 55b9eb080d4cd8c57e9efb3ace52dba8c3dcf6d4 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:32:50 +0300
Subject: [PATCH 11/25] Validate the intrinsic profile residual split

---
 .../workflows/erdos625-q-only-attachment-envelope.yml  | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml
index 47c39a7a..46b6f359 100644
--- a/.github/workflows/erdos625-q-only-attachment-envelope.yml
+++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml
@@ -5,6 +5,7 @@ on:
     paths:
       - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean"
       - "625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean"
       - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md"
       - ".github/workflows/erdos625-q-only-attachment-envelope.yml"
   workflow_dispatch:
@@ -23,7 +24,8 @@ jobs:
           if grep -nE \
             '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
             625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean \
-            625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean; then
+            625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean; then
             exit 1
           fi
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
@@ -34,15 +36,15 @@ jobs:
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Build attained-profile q-only endpoint warning-fatally
+      - name: Build intrinsic profile split warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
           set +e
-          lake build Erdos625.Section9ProfileAttachmentQOnly --wfail \
+          lake build Erdos625.Section9ProfileAttachmentIntrinsicSplit --wfail \
             > /tmp/q-only-envelope-lean.log 2>&1
           status=$?
-          tail -n 300 /tmp/q-only-envelope-lean.log
+          tail -n 320 /tmp/q-only-envelope-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()

From 997d61099d3c21664f07557cf832bfe58c44d08d Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:35:57 +0300
Subject: [PATCH 12/25] Expose the residual-mass abbreviation in the positivity
 proof

---
 625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
index 5d2f11a9..03926b9e 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
@@ -94,6 +94,7 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale :
   intro b k row0 U hU hcap demand hpow
   let m := canonicalDemandResidualTotal (profileBlockMargin k)
     (profileBlockMargin k) U demand
+  change 2 ^ U ≤ m ^ 3 at hpow
   have hmpos : 0 < m := by
     by_contra hm
     have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm

From ada3ea50c09e7b07cbdf511ff6e48eed34d577a0 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:38:12 +0300
Subject: [PATCH 13/25] Normalize the intrinsic-split target before case
 analysis

---
 .../Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean        | 1 +
 1 file changed, 1 insertion(+)

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
index 23b6a867..4de3fe50 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
@@ -45,6 +45,7 @@ theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split :
     exists_absolute_profileHighSkeletonAttachment_le_qOnlyEnvelope
   refine ⟨kappa, hkpos, hktop, ?_⟩
   intro b n k row0 U hcap demand
+  dsimp only
   let m := canonicalDemandResidualTotal
     (profileBlockMargin k) (profileBlockMargin k) U demand
   by_cases hpow : 2 ^ U ≤ m ^ 3

From 146a7bfc80eda23e34f035033f9550b0f6f0424e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 10:44:28 +0300
Subject: [PATCH 14/25] Cancel obsolete q-only validation runs

---
 .github/workflows/erdos625-q-only-attachment-envelope.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml
index 46b6f359..68a49e1b 100644
--- a/.github/workflows/erdos625-q-only-attachment-envelope.yml
+++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml
@@ -10,6 +10,10 @@ on:
       - ".github/workflows/erdos625-q-only-attachment-envelope.yml"
   workflow_dispatch:
 
+concurrency:
+  group: erdos625-q-only-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

From f48c6613a449344c5519079ca6198601b4ec4aa6 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:16:32 +0300
Subject: [PATCH 15/25] Fix warning-fatal q-only profile proof

---
 .../Erdos625/Section9ProfileAttachmentQOnly.lean              | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
index 03926b9e..47aadbe5 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
@@ -98,8 +98,8 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale :
   have hmpos : 0 < m := by
     by_contra hm
     have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm
-    have htwoPos : 0 < (2 : Nat) ^ U := pow_pos (by decide) U
-    exact (not_le_of_gt htwoPos) (by simpa [hm0] using hpow)
+    subst m
+    simp at hpow
   have hbase := hfinite row0 U m hcap demand rfl hmpos hpow
   let exponent : ENNReal := kappa * (U : ENNReal) ^ 2
   have hexponent : exponent ≠ ∞ := by

From 8c47f865e4441841e776d4d16760509a56c985bf Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:17:04 +0300
Subject: [PATCH 16/25] Fix warning-fatal intrinsic split proof

---
 .../Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean   | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
index 4de3fe50..81820bde 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
@@ -30,7 +30,7 @@ theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split :
     ∃ kappa : ENNReal, 0 < kappa ∧ kappa ≠ ∞ ∧
       ∀ {b n : ℕ} {k : ColoringProfile b}
           (row0 : OrderedProfilePartition n k) (U : ℕ)
-          (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
+          (_hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
           (demand : ProfileCanonicalHighSkeleton k U),
         let m := canonicalDemandResidualTotal
           (profileBlockMargin k) (profileBlockMargin k) U demand
@@ -53,8 +53,8 @@ theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split :
     have hmpos : 0 < m := by
       by_contra hm
       have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm
-      have htwoPos : 0 < (2 : Nat) ^ U := pow_pos (by decide) U
-      exact (not_le_of_gt htwoPos) (by simpa [hm0] using hpow)
+      subst m
+      simp at hpow
     exact ⟨hpow, hlarge row0 U m hcap demand rfl hmpos hpow⟩
   · right
     have hmass := residualMass_lt_two_pow_ceilThird_of_not_cube U m hpow

From 2971838d9e91859ef481239049fad4129f5f43c7 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:23:11 +0300
Subject: [PATCH 17/25] Assemble the q-only and small residual attachment
 regimes

---
 .../Section9QOnlyTwoRegimeAssembly.lean       | 229 ++++++++++++++++++
 1 file changed, 229 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean

diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
new file mode 100644
index 00000000..5563b3f8
--- /dev/null
+++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
@@ -0,0 +1,229 @@
+import Erdos625.Section9ProfileAttachmentQOnly
+import Erdos625.Section9ProfileAttachmentSmallResidualLogScale
+import Erdos625.Section9PhaseTwoPowerCorridor
+import Erdos625.Section9ActualAttachmentAggregation
+import Erdos625.Section10AmplificationScales
+import Mathlib.Tactic
+
+/-!
+# Section IX: q-only two-regime attachment assembly
+
+The direct matching-restriction route gives an `exp(O((log n)^2))` attachment
+bound whenever its intrinsic finite hypothesis `2^U <= m^3` holds.  The
+existing phase corridor shows that this hypothesis holds throughout the old
+large-residual range.  Its complement is therefore covered by the literal
+small-residual estimate.
+
+This file combines those two profile-level estimates with the exact bare-times-
+attachment aggregation.  It does not estimate the Section VIII bare skeleton
+sum or prove the final random-graph statement.
+-/
+
+namespace Erdos625
+
+open Filter
+open scoped ENNReal Topology
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- A `log^2` large branch and an `n/log^5` small branch admit one deterministic
+error sequence at the amplification scale `n/log^4`.  The two branches may have
+different nonnegative constants. -/
+theorem exists_uniform_qOnly_twoRegime_error
+    (S : ℕ → Type*)
+    (attachment : ∀ n, S n → ℝ)
+    (m₀ : ∀ n, S n → ℕ)
+    (Cq Cs : ℝ) (hCq : 0 ≤ Cq) (hCs : 0 ≤ Cs)
+    (hlarge : ∀ᶠ n : ℕ in atTop,
+      ∀ s : S n,
+        (n : ℝ) / Real.log (n : ℝ) ^ 6 ≤ (m₀ n s : ℝ) →
+        attachment n s ≤ Real.exp (Cq * Real.log (n : ℝ) ^ 2))
+    (hsmall : ∀ᶠ n : ℕ in atTop,
+      ∀ s : S n,
+        (m₀ n s : ℝ) < (n : ℝ) / Real.log (n : ℝ) ^ 6 →
+        attachment n s ≤
+          Real.exp (Cs * (n : ℝ) / Real.log (n : ℝ) ^ 5)) :
+    ∃ εAtt : ℕ → ℝ,
+      Tendsto εAtt atTop (nhds 0) ∧
+        ∀ᶠ n : ℕ in atTop,
+          0 ≤ εAtt n ∧
+            ∀ s : S n,
+              attachment n s ≤
+                Real.exp
+                  (εAtt n * (n : ℝ) / Real.log (n : ℝ) ^ 4) := by
+  refine ⟨fun n =>
+    Cq * (Real.log (n : ℝ) ^ 6 / (n : ℝ)) +
+      Cs / Real.log (n : ℝ), ?_, ?_⟩
+  · have h_log_div_n :
+        Tendsto
+          (fun n : ℕ => Real.log (n : ℝ) ^ 6 / (n : ℝ))
+          atTop (nhds 0) := by
+      suffices h_log :
+          Tendsto (fun y : ℝ => y ^ 6 / Real.exp y) atTop (nhds 0) by
+        have hcomp := h_log.comp
+          (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
+        exact hcomp.congr' (by
+          filter_upwards [Filter.eventually_gt_atTop 0] with n hn
+          simp +decide [Real.exp_log (Nat.cast_pos.mpr hn)])
+      simpa only [Real.exp_neg, div_eq_mul_inv] using
+        Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero 6
+    have h_inv_log :
+        Tendsto (fun n : ℕ => 1 / Real.log (n : ℝ)) atTop (nhds 0) :=
+      tendsto_inv_atTop_zero.comp
+        (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
+    simpa only [div_eq_mul_inv] using
+      (tendsto_const_nhds.mul h_log_div_n).add
+        (tendsto_const_nhds.mul h_inv_log)
+  · obtain ⟨a₁, ha₁⟩ := hlarge
+    obtain ⟨a₂, ha₂⟩ := hsmall
+    use Nat.max (Nat.max a₁ a₂) 3
+    intro n hn
+    have ha₁n : a₁ ≤ n := by omega
+    have ha₂n : a₂ ≤ n := by omega
+    have hn3 : 3 ≤ n := by omega
+    have hnpos : 0 < (n : ℝ) := by positivity
+    have hlog : 0 < Real.log (n : ℝ) :=
+      Real.log_pos (by exact_mod_cast (lt_of_lt_of_le (by norm_num : 1 < 3) hn3))
+    have hscale :
+        (Cq * (Real.log (n : ℝ) ^ 6 / (n : ℝ)) +
+            Cs / Real.log (n : ℝ)) *
+              (n : ℝ) / Real.log (n : ℝ) ^ 4 =
+          Cq * Real.log (n : ℝ) ^ 2 +
+            Cs * (n : ℝ) / Real.log (n : ℝ) ^ 5 := by
+      field_simp [ne_of_gt hnpos, ne_of_gt hlog]
+      ring
+    refine ⟨?_, ?_⟩
+    · exact add_nonneg
+        (mul_nonneg hCq
+          (div_nonneg (pow_nonneg (Real.log_natCast_nonneg _) _)
+            (Nat.cast_nonneg _)))
+        (div_nonneg hCs (Real.log_natCast_nonneg _))
+    · intro s
+      by_cases hmass :
+          (m₀ n s : ℝ) < (n : ℝ) / Real.log (n : ℝ) ^ 6
+      · refine (ha₂ n ha₂n s hmass).trans (Real.exp_le_exp.mpr ?_)
+        rw [hscale]
+        exact le_add_of_nonneg_left
+          (mul_nonneg hCq (sq_nonneg (Real.log (n : ℝ))))
+      · refine (ha₁ n ha₁n s (le_of_not_gt hmass)).trans
+          (Real.exp_le_exp.mpr ?_)
+        rw [hscale]
+        exact le_add_of_nonneg_right
+          (div_nonneg
+            (mul_nonneg hCs (Nat.cast_nonneg n))
+            (pow_nonneg hlog.le 5))
+
+/-- The q-only large branch and the literal small branch combine into the exact
+midpoint canonical attachment sum with a vanishing amplification-scale error. -/
+theorem exists_midpointCanonicalAttachment_qOnly_twoRegime_error
+    (b U : Nat → Nat)
+    (k : (n : Nat) → ColoringProfile (b n))
+    (row0 : (n : Nat) → OrderedProfilePartition n (k n))
+    (hU : ∀ᶠ n : Nat in atTop, U n ≤ phaseNat n)
+    (hcap : ∀ᶠ n : Nat in atTop,
+      ∀ a : ProfileBlockIndex (k n), profileBlockMargin (k n) a ≤ U n) :
+    ∃ epsilon : Nat → Real,
+      Tendsto epsilon atTop (nhds 0) ∧
+      (∀ᶠ n in atTop, 0 ≤ epsilon n) ∧
+      ∀ᶠ n in atTop,
+        midpointCanonicalAttachmentSum (row0 n) (U n) ≤
+          canonicalBareSkeletonSum (k n) (U n) *
+            ENNReal.ofReal
+              (Real.exp (epsilon n * amplificationBase n)) := by
+  obtain ⟨Cq, hCq, hq⟩ :=
+    eventually_profileHighSkeletonAttachment_le_qOnly_logScale
+  obtain ⟨Cs, hCs, hs⟩ :=
+    eventually_profileHighSkeletonAttachment_le_smallResidual_logScale
+  have hlarge : ∀ᶠ n : Nat in atTop,
+      ∀ demand : ProfileCanonicalHighSkeleton (k n) (U n),
+        (n : Real) / Real.log (n : Real) ^ 6 ≤
+            (canonicalDemandResidualTotal
+              (profileBlockMargin (k n)) (profileBlockMargin (k n))
+              (U n) demand : Real) →
+        (profileHighSkeletonAttachment (row0 n) (U n) demand).toReal ≤
+          Real.exp (Cq * Real.log (n : Real) ^ 2) := by
+    filter_upwards
+      [hq, hU, hcap, eventually_phaseControlled_two_pow_le_cube,
+        eventually_gt_atTop (1 : Nat)] with n hqn hUn hcapn hcorr hn
+    intro demand hmass
+    let m := canonicalDemandResidualTotal
+      (profileBlockMargin (k n)) (profileBlockMargin (k n)) (U n) demand
+    have hlog : 0 < Real.log (n : Real) :=
+      Real.log_pos (by exact_mod_cast hn)
+    have hmpos : 0 < m := by
+      have hmreal : 0 < (m : Real) :=
+        lt_of_lt_of_le
+          (div_pos (by positivity) (pow_pos hlog 6)) hmass
+      exact_mod_cast hmreal
+    have hpow : 2 ^ U n ≤ m ^ 3 := hcorr (U n) m hUn hmpos hmass
+    have hbound := hqn (row0 n) (U n) hUn hcapn demand hpow
+    exact (ENNReal.toReal_mono ENNReal.ofReal_ne_top hbound).trans_eq (by
+      rw [ENNReal.toReal_ofReal (Real.exp_nonneg _)])
+  have hsmall : ∀ᶠ n : Nat in atTop,
+      ∀ demand : ProfileCanonicalHighSkeleton (k n) (U n),
+        (canonicalDemandResidualTotal
+          (profileBlockMargin (k n)) (profileBlockMargin (k n))
+          (U n) demand : Real) <
+            (n : Real) / Real.log (n : Real) ^ 6 →
+        (profileHighSkeletonAttachment (row0 n) (U n) demand).toReal ≤
+          Real.exp (Cs * (n : Real) / Real.log (n : Real) ^ 5) := by
+    filter_upwards [hs, hU, hcap] with n hsn hUn hcapn
+    intro demand hmass
+    have hbound := hsn (row0 n) (U n) hUn hcapn demand hmass
+    exact (ENNReal.toReal_mono ENNReal.ofReal_ne_top hbound).trans_eq (by
+      rw [ENNReal.toReal_ofReal (Real.exp_nonneg _)])
+  obtain ⟨epsilon, hepsilon, hevent⟩ :=
+    exists_uniform_qOnly_twoRegime_error
+      (fun n => ProfileCanonicalHighSkeleton (k n) (U n))
+      (fun n demand =>
+        (profileHighSkeletonAttachment (row0 n) (U n) demand).toReal)
+      (fun n demand =>
+        canonicalDemandResidualTotal
+          (profileBlockMargin (k n)) (profileBlockMargin (k n))
+          (U n) demand)
+      Cq Cs hCq hCs hlarge hsmall
+  refine ⟨epsilon, hepsilon, hevent.mono fun _ hn => hn.1, ?_⟩
+  filter_upwards
+    [hevent, hq, hs, hU, hcap, eventually_phaseControlled_two_pow_le_cube,
+      eventually_gt_atTop (1 : Nat)] with n hn hqn hsn hUn hcapn hcorr hnlarge
+  apply midpointCanonicalAttachmentSum_le_bare_mul
+  intro demand
+  have hfinite :
+      profileHighSkeletonAttachment (row0 n) (U n) demand ≠ ⊤ := by
+    by_cases hmass :
+        (canonicalDemandResidualTotal
+          (profileBlockMargin (k n)) (profileBlockMargin (k n))
+          (U n) demand : Real) <
+            (n : Real) / Real.log (n : Real) ^ 6
+    · have hbound := hsn (row0 n) (U n) hUn hcapn demand hmass
+      intro htop
+      rw [htop] at hbound
+      exact ENNReal.ofReal_ne_top (top_le_iff.mp hbound)
+    · let m := canonicalDemandResidualTotal
+        (profileBlockMargin (k n)) (profileBlockMargin (k n)) (U n) demand
+      have hlog : 0 < Real.log (n : Real) :=
+        Real.log_pos (by exact_mod_cast hnlarge)
+      have hmpos : 0 < m := by
+        have hmreal : 0 < (m : Real) :=
+          lt_of_lt_of_le
+            (div_pos (by positivity) (pow_pos hlog 6))
+            (le_of_not_gt hmass)
+        exact_mod_cast hmreal
+      have hpow : 2 ^ U n ≤ m ^ 3 :=
+        hcorr (U n) m hUn hmpos (le_of_not_gt hmass)
+      have hbound := hqn (row0 n) (U n) hUn hcapn demand hpow
+      intro htop
+      rw [htop] at hbound
+      exact ENNReal.ofReal_ne_top (top_le_iff.mp hbound)
+  rw [← ENNReal.ofReal_toReal hfinite]
+  apply ENNReal.ofReal_le_ofReal
+  simpa only [amplificationBase, mul_div_assoc] using hn.2 demand
+
+#print axioms exists_uniform_qOnly_twoRegime_error
+#print axioms exists_midpointCanonicalAttachment_qOnly_twoRegime_error
+
+end
+
+end Erdos625

From 8333bc77433d3fbfdaaeb5fa4a7991c34da54657 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:23:57 +0300
Subject: [PATCH 18/25] Validate the q-only two-regime assembly

---
 .../workflows/erdos625-q-only-attachment-envelope.yml  | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/erdos625-q-only-attachment-envelope.yml b/.github/workflows/erdos625-q-only-attachment-envelope.yml
index 68a49e1b..967a991a 100644
--- a/.github/workflows/erdos625-q-only-attachment-envelope.yml
+++ b/.github/workflows/erdos625-q-only-attachment-envelope.yml
@@ -6,6 +6,7 @@ on:
       - "625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean"
       - "625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean"
       - "625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean"
+      - "625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean"
       - "625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md"
       - ".github/workflows/erdos625-q-only-attachment-envelope.yml"
   workflow_dispatch:
@@ -29,7 +30,8 @@ jobs:
             '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
             625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean \
             625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean \
-            625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean; then
+            625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean \
+            625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean; then
             exit 1
           fi
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
@@ -40,15 +42,15 @@ jobs:
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Build intrinsic profile split warning-fatally
+      - name: Build q-only two-regime assembly warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
           set +e
-          lake build Erdos625.Section9ProfileAttachmentIntrinsicSplit --wfail \
+          lake build Erdos625.Section9QOnlyTwoRegimeAssembly --wfail \
             > /tmp/q-only-envelope-lean.log 2>&1
           status=$?
-          tail -n 320 /tmp/q-only-envelope-lean.log
+          tail -n 380 /tmp/q-only-envelope-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()

From 2dd427978fd4199733b665e24c11a17da0237b2e Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:34:45 +0300
Subject: [PATCH 19/25] Avoid placeholder-word false positive in assembly
 documentation

---
 625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
index 5563b3f8..f566d705 100644
--- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
+++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
@@ -28,7 +28,7 @@ noncomputable section
 
 set_option autoImplicit false
 
-/-- A `log^2` large branch and an `n/log^5` small branch admit one deterministic
+/-- A `log^2` large branch and an `n/log^5` small branch yield one deterministic
 error sequence at the amplification scale `n/log^4`.  The two branches may have
 different nonnegative constants. -/
 theorem exists_uniform_qOnly_twoRegime_error

From 33866e2330689468acf71557ceabc0dc0c21c87a Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:46:28 +0300
Subject: [PATCH 20/25] Use an explicit positivity contradiction in the q-only
 profile adapter

---
 .../Erdos625/Section9ProfileAttachmentQOnly.lean             | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
index 47aadbe5..f3fc1b71 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
@@ -98,8 +98,9 @@ theorem eventually_profileHighSkeletonAttachment_le_qOnly_logScale :
   have hmpos : 0 < m := by
     by_contra hm
     have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm
-    subst m
-    simp at hpow
+    have hm3 : m ^ 3 = 0 := by rw [hm0]; norm_num
+    rw [hm3] at hpow
+    exact (Nat.not_lt_of_ge hpow) (pow_pos (by decide) U)
   have hbase := hfinite row0 U m hcap demand rfl hmpos hpow
   let exponent : ENNReal := kappa * (U : ENNReal) ^ 2
   have hexponent : exponent ≠ ∞ := by

From 96f8e82ffbf3851002a7995f42872014d89425a2 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:47:10 +0300
Subject: [PATCH 21/25] Use an explicit positivity contradiction in the
 intrinsic split

---
 .../Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean    | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
index 81820bde..aff375fc 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
@@ -53,8 +53,9 @@ theorem exists_absolute_profileHighSkeletonAttachment_intrinsic_split :
     have hmpos : 0 < m := by
       by_contra hm
       have hm0 : m = 0 := Nat.eq_zero_of_not_pos hm
-      subst m
-      simp at hpow
+      have hm3 : m ^ 3 = 0 := by rw [hm0]; norm_num
+      rw [hm3] at hpow
+      exact (Nat.not_lt_of_ge hpow) (pow_pos (by decide) U)
     exact ⟨hpow, hlarge row0 U m hcap demand rfl hmpos hpow⟩
   · right
     have hmass := residualMass_lt_two_pow_ceilThird_of_not_cube U m hpow

From 7836b7d446ec29e95eaf3cdd6b52e87d583a5b97 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 13:58:06 +0300
Subject: [PATCH 22/25] Repair the q-only two-regime filter and normalization
 bridges

---
 .../Section9QOnlyTwoRegimeAssembly.lean       | 29 ++++++++++---------
 1 file changed, 16 insertions(+), 13 deletions(-)

diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
index f566d705..ea8b191a 100644
--- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
+++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
@@ -9,13 +9,13 @@ import Mathlib.Tactic
 # Section IX: q-only two-regime attachment assembly
 
 The direct matching-restriction route gives an `exp(O((log n)^2))` attachment
-bound whenever its intrinsic finite hypothesis `2^U <= m^3` holds.  The
+bound whenever its intrinsic finite hypothesis `2^U <= m^3` holds. The
 existing phase corridor shows that this hypothesis holds throughout the old
-large-residual range.  Its complement is therefore covered by the literal
+large-residual range. Its complement is therefore covered by the literal
 small-residual estimate.
 
 This file combines those two profile-level estimates with the exact bare-times-
-attachment aggregation.  It does not estimate the Section VIII bare skeleton
+attachment aggregation. It does not estimate the Section VIII bare skeleton
 sum or prove the final random-graph statement.
 -/
 
@@ -29,7 +29,7 @@ noncomputable section
 set_option autoImplicit false
 
 /-- A `log^2` large branch and an `n/log^5` small branch yield one deterministic
-error sequence at the amplification scale `n/log^4`.  The two branches may have
+error sequence at the amplification scale `n/log^4`. The two branches may have
 different nonnegative constants. -/
 theorem exists_uniform_qOnly_twoRegime_error
     (S : ℕ → Type*)
@@ -69,15 +69,16 @@ theorem exists_uniform_qOnly_twoRegime_error
           simp +decide [Real.exp_log (Nat.cast_pos.mpr hn)])
       simpa only [Real.exp_neg, div_eq_mul_inv] using
         Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero 6
+    have h_inv_log_raw := tendsto_inv_atTop_zero.comp
+      (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
     have h_inv_log :
-        Tendsto (fun n : ℕ => 1 / Real.log (n : ℝ)) atTop (nhds 0) :=
-      tendsto_inv_atTop_zero.comp
-        (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
-    simpa only [div_eq_mul_inv] using
-      (tendsto_const_nhds.mul h_log_div_n).add
-        (tendsto_const_nhds.mul h_inv_log)
-  · obtain ⟨a₁, ha₁⟩ := hlarge
-    obtain ⟨a₂, ha₂⟩ := hsmall
+        Tendsto (fun n : ℕ => 1 / Real.log (n : ℝ)) atTop (nhds 0) := by
+      simpa only [Function.comp_apply, one_div] using h_inv_log_raw
+    have hq := h_log_div_n.const_mul Cq
+    have hs := h_inv_log.const_mul Cs
+    simpa only [div_eq_mul_inv, one_div, mul_zero, add_zero] using hq.add hs
+  · rcases (eventually_atTop.1 hlarge) with ⟨a₁, ha₁⟩
+    rcases (eventually_atTop.1 hsmall) with ⟨a₂, ha₂⟩
     use Nat.max (Nat.max a₁ a₂) 3
     intro n hn
     have ha₁n : a₁ ≤ n := by omega
@@ -173,7 +174,9 @@ theorem exists_midpointCanonicalAttachment_qOnly_twoRegime_error
     intro demand hmass
     have hbound := hsn (row0 n) (U n) hUn hcapn demand hmass
     exact (ENNReal.toReal_mono ENNReal.ofReal_ne_top hbound).trans_eq (by
-      rw [ENNReal.toReal_ofReal (Real.exp_nonneg _)])
+      rw [ENNReal.toReal_ofReal (Real.exp_nonneg _)]
+      congr 1
+      ring)
   obtain ⟨epsilon, hepsilon, hevent⟩ :=
     exists_uniform_qOnly_twoRegime_error
       (fun n => ProfileCanonicalHighSkeleton (k n) (U n))

From c7d21751f66727a9a0c6101e927278f5234a8b57 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 14:09:24 +0300
Subject: [PATCH 23/25] Construct the q-only two-regime eventual bound
 explicitly

---
 .../Erdos625/Section9QOnlyTwoRegimeAssembly.lean          | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
index ea8b191a..01dbedd0 100644
--- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
+++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
@@ -73,13 +73,15 @@ theorem exists_uniform_qOnly_twoRegime_error
       (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
     have h_inv_log :
         Tendsto (fun n : ℕ => 1 / Real.log (n : ℝ)) atTop (nhds 0) := by
-      simpa only [Function.comp_apply, one_div] using h_inv_log_raw
+      simpa only [Function.comp_def, one_div] using h_inv_log_raw
     have hq := h_log_div_n.const_mul Cq
     have hs := h_inv_log.const_mul Cs
-    simpa only [div_eq_mul_inv, one_div, mul_zero, add_zero] using hq.add hs
+    simpa only [div_eq_mul_inv, one_div, one_mul, mul_zero, add_zero] using
+      hq.add hs
   · rcases (eventually_atTop.1 hlarge) with ⟨a₁, ha₁⟩
     rcases (eventually_atTop.1 hsmall) with ⟨a₂, ha₂⟩
-    use Nat.max (Nat.max a₁ a₂) 3
+    apply eventually_atTop.2
+    refine ⟨Nat.max (Nat.max a₁ a₂) 3, ?_⟩
     intro n hn
     have ha₁n : a₁ ≤ n := by omega
     have ha₂n : a₂ ≤ n := by omega

From d33b06d47aaba00914046fdbca4bdf625fa1bdce Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 20:44:36 +0300
Subject: [PATCH 24/25] Repair q-only two-regime focused Lean target

---
 .../Erdos625/Section9QOnlyTwoRegimeAssembly.lean   | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
index 01dbedd0..9303ae20 100644
--- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
+++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
@@ -83,9 +83,14 @@ theorem exists_uniform_qOnly_twoRegime_error
     apply eventually_atTop.2
     refine ⟨Nat.max (Nat.max a₁ a₂) 3, ?_⟩
     intro n hn
-    have ha₁n : a₁ ≤ n := by omega
-    have ha₂n : a₂ ≤ n := by omega
-    have hn3 : 3 ≤ n := by omega
+    have ha₁n : a₁ ≤ n :=
+      (Nat.le_max_left a₁ a₂).trans
+        ((Nat.le_max_left (Nat.max a₁ a₂) 3).trans hn)
+    have ha₂n : a₂ ≤ n :=
+      (Nat.le_max_right a₁ a₂).trans
+        ((Nat.le_max_left (Nat.max a₁ a₂) 3).trans hn)
+    have hn3 : 3 ≤ n :=
+      (Nat.le_max_right (Nat.max a₁ a₂) 3).trans hn
     have hnpos : 0 < (n : ℝ) := by positivity
     have hlog : 0 < Real.log (n : ℝ) :=
       Real.log_pos (by exact_mod_cast (lt_of_lt_of_le (by norm_num : 1 < 3) hn3))
@@ -96,7 +101,6 @@ theorem exists_uniform_qOnly_twoRegime_error
           Cq * Real.log (n : ℝ) ^ 2 +
             Cs * (n : ℝ) / Real.log (n : ℝ) ^ 5 := by
       field_simp [ne_of_gt hnpos, ne_of_gt hlog]
-      ring
     refine ⟨?_, ?_⟩
     · exact add_nonneg
         (mul_nonneg hCq
@@ -223,7 +227,7 @@ theorem exists_midpointCanonicalAttachment_qOnly_twoRegime_error
       rw [htop] at hbound
       exact ENNReal.ofReal_ne_top (top_le_iff.mp hbound)
   rw [← ENNReal.ofReal_toReal hfinite]
-  apply ENNReal.ofReal_le_ofReal
+  apply ENNREAL.ofReal_le_ofReal
   simpa only [amplificationBase, mul_div_assoc] using hn.2 demand
 
 #print axioms exists_uniform_qOnly_twoRegime_error

From 2ea82c988218dee89d3639f598090ce813501c40 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 20:47:01 +0300
Subject: [PATCH 25/25] Correct ENNReal namespace in q-only assembly

---
 625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
index 9303ae20..aab1ce4f 100644
--- a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
+++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
@@ -227,7 +227,7 @@ theorem exists_midpointCanonicalAttachment_qOnly_twoRegime_error
       rw [htop] at hbound
       exact ENNReal.ofReal_ne_top (top_le_iff.mp hbound)
   rw [← ENNReal.ofReal_toReal hfinite]
-  apply ENNREAL.ofReal_le_ofReal
+  apply ENNReal.ofReal_le_ofReal
   simpa only [amplificationBase, mul_div_assoc] using hn.2 demand
 
 #print axioms exists_uniform_qOnly_twoRegime_error