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..967a991a
--- /dev/null
+++ b/.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
diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean b/625/formalization/Erdos625/Section9MatchingRestrictionQOnly.lean
new file mode 100644
index 00000000..5d9c5be6
--- /dev/null
+++ b/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
diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean b/625/formalization/Erdos625/Section9ProfileAttachmentIntrinsicSplit.lean
new file mode 100644
index 00000000..aff375fc
--- /dev/null
+++ b/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
diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
new file mode 100644
index 00000000..f3fc1b71
--- /dev/null
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentQOnly.lean
@@ -0,0 +1,141 @@
+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
+  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
+    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
+    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]
+  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
diff --git a/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
new file mode 100644
index 00000000..aab1ce4f
--- /dev/null
+++ b/625/formalization/Erdos625/Section9QOnlyTwoRegimeAssembly.lean
@@ -0,0 +1,238 @@
+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 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
+    (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_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) := by
+      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, 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₂⟩
+    apply eventually_atTop.2
+    refine ⟨Nat.max (Nat.max a₁ a₂) 3, ?_⟩
+    intro n hn
+    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))
+    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]
+    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 _)]
+      congr 1
+      ring)
+  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
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..588bac05
--- /dev/null
+++ b/625/formalization/Q_ONLY_ATTACHMENT_ENVELOPE_AUDIT.md
@@ -0,0 +1,105 @@
+# 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. `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;
+- 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;
+- 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 and to expose a cleaner finite regime split before
+manuscript integration.