diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml
new file mode 100644
index 00000000..3c8b30a7
--- /dev/null
+++ b/.github/workflows/erdos625-matching-restriction-envelope.yml
@@ -0,0 +1,59 @@
+name: Erdős 625 matching-restriction envelope
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean"
+      - "625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md"
+      - ".github/workflows/erdos625-matching-restriction-envelope.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ 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 in the new modules
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean; then
+            exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the log-square endpoint and dependency closure warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9ProfileAttachmentMatchingLogScale --wfail \
+            > /tmp/section9-envelope-lean.log 2>&1
+          status=$?
+          tail -n 300 /tmp/section9-envelope-lean.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: section9-matching-envelope-lean-log
+          path: /tmp/section9-envelope-lean.log
+          if-no-files-found: ignore
diff --git a/.github/workflows/erdos625-matching-restriction-product.yml b/.github/workflows/erdos625-matching-restriction-product.yml
new file mode 100644
index 00000000..61c6c4ed
--- /dev/null
+++ b/.github/workflows/erdos625-matching-restriction-product.yml
@@ -0,0 +1,42 @@
+name: Erdős 625 matching-restriction product
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean"
+      - "625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md"
+      - ".github/workflows/erdos625-matching-restriction-product.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 in the new module
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean; then
+            exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: true
+          build-args: --wfail
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Compile the module warning-fatally after dependency build
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          lake env lean -DwarningAsError=true \
+            Erdos625/Section9MatchingRestrictionProduct.lean \
+            -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionProduct.olean
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/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
new file mode 100644
index 00000000..3e588e6d
--- /dev/null
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
@@ -0,0 +1,306 @@
+import Erdos625.Section9MatchingRestrictionProduct
+import Erdos625.Section9ActualResidualENNRealExpBridge
+import Erdos625.Section9FixedFFubiniBridge
+import Erdos625.Section9ResidualQQuadratic
+import Erdos625.Section9ResidualLambdaTotalBound
+import Erdos625.Section9ThetaCap
+import Erdos625.ConfigurationThetaMoments
+import Mathlib.Tactic
+
+/-!
+# Section IX: direct matching-restriction attachment envelope
+
+This module continues the direct matching-restriction route.  It first identifies
+its fixed-even-family bound with the literal event-restricted attachment
+numerator.  It then proves the global quadratic configuration-theta estimate,
+sums the literal residual-q bound at scale `U^2`, and combines the two finite
+products into one exponential envelope.
+
+The result is pointwise in the finite residual data.  It does not perform the
+Section VIII skeleton sum, specialize to the midpoint profile, or prove
+`Erdos625Statement`.
+-/
+
+universe u v
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+/-- Exact global factorization of the squared configuration-cell parameters. -/
+theorem sum_configurationCellTheta_sq_global
+    {A : Type u} {B : Type v} [Fintype A] [Fintype B]
+    (row : A → ℕ) (col : B → ℕ) (m : ℕ) :
+    (∑ a, ∑ b, configurationCellTheta row col m a b ^ 2) =
+      (eulerENNReal / (m : ENNReal)) ^ 2 *
+        (∑ a, (row a : ENNReal) ^ 2) *
+        (∑ b, (col b : ENNReal) ^ 2) := by
+  calc
+    (∑ a, ∑ b, configurationCellTheta row col m a b ^ 2) =
+        ∑ a, ((eulerENNReal / (m : ENNReal)) ^ 2 *
+          (row a : ENNReal) ^ 2) *
+          (∑ b, (col b : ENNReal) ^ 2) := by
+      apply Finset.sum_congr rfl
+      intro a _
+      simpa only [mul_assoc] using
+        (sum_configurationCellTheta_sq_row row col m a)
+    _ = (∑ a, (eulerENNReal / (m : ENNReal)) ^ 2 *
+          (row a : ENNReal) ^ 2) *
+          (∑ b, (col b : ENNReal) ^ 2) := by
+      rw [Finset.sum_mul]
+    _ = ((eulerENNReal / (m : ENNReal)) ^ 2 *
+          (∑ a, (row a : ENNReal) ^ 2)) *
+          (∑ b, (col b : ENNReal) ^ 2) := by
+      congr 1
+      rw [Finset.mul_sum]
+    _ = (eulerENNReal / (m : ENNReal)) ^ 2 *
+        (∑ a, (row a : ENNReal) ^ 2) *
+        (∑ b, (col b : ENNReal) ^ 2) := by
+      rfl
+
+/-- Under equal positive total mass and degree caps, the complete quadratic
+configuration-theta mass is at most `e^2 U^2`. -/
+theorem sum_configurationCellTheta_sq_le_euler_sq_cap_sq
+    {A : Type u} {B : Type v} [Fintype A] [Fintype B]
+    (row : A → ℕ) (col : B → ℕ) (m U : ℕ)
+    (hm : 0 < m)
+    (hrowCap : ∀ a, row a ≤ U) (hcolCap : ∀ b, col b ≤ U)
+    (hrowTotal : ∑ a, row a = m) (hcolTotal : ∑ b, col b = m) :
+    (∑ a, ∑ b, configurationCellTheta row col m a b ^ 2) ≤
+      eulerENNReal ^ 2 * (U : ENNReal) ^ 2 := by
+  have hrow :=
+    degreeSquareSum_ennreal_le_cap_mul_total row U m hrowCap hrowTotal
+  have hcol :=
+    degreeSquareSum_ennreal_le_cap_mul_total col U m hcolCap hcolTotal
+  calc
+    (∑ a, ∑ b, configurationCellTheta row col m a b ^ 2) =
+        (eulerENNReal / (m : ENNReal)) ^ 2 *
+          (∑ a, (row a : ENNReal) ^ 2) *
+          (∑ b, (col b : ENNReal) ^ 2) :=
+      sum_configurationCellTheta_sq_global row col m
+    _ ≤ (eulerENNReal / (m : ENNReal)) ^ 2 *
+          ((U : ENNReal) * (m : ENNReal)) *
+          (∑ b, (col b : ENNReal) ^ 2) :=
+      mul_le_mul_left
+        (mul_le_mul_right hrow
+          ((eulerENNReal / (m : ENNReal)) ^ 2))
+        (∑ b, (col b : ENNReal) ^ 2)
+    _ ≤ (eulerENNReal / (m : ENNReal)) ^ 2 *
+          ((U : ENNReal) * (m : ENNReal)) *
+          ((U : ENNReal) * (m : ENNReal)) :=
+      mul_le_mul_right hcol
+        ((eulerENNReal / (m : ENNReal)) ^ 2 *
+          ((U : ENNReal) * (m : ENNReal)))
+    _ = eulerENNReal ^ 2 * (U : ENNReal) ^ 2 := by
+      have hm0 : (m : ENNReal) ≠ 0 := by
+        exact_mod_cast hm.ne'
+      have hmt : (m : ENNReal) ≠ ∞ := ENNReal.natCast_ne_top m
+      rw [div_eq_mul_inv]
+      calc
+        (eulerENNReal * (m : ENNReal)⁻¹) ^ 2 *
+            ((U : ENNReal) * (m : ENNReal)) *
+            ((U : ENNReal) * (m : ENNReal)) =
+          eulerENNReal ^ 2 * (U : ENNReal) ^ 2 *
+            ((m : ENNReal) * (m : ENNReal)⁻¹) ^ 2 := by
+          ring
+        _ = eulerENNReal ^ 2 * (U : ENNReal) ^ 2 := by
+          rw [ENNReal.mul_inv_cancel hm0 hmt, one_pow, mul_one]
+
+/-- One absolute finite constant bounds the total literal residual-q mass at
+scale `U^2`, with no factor depending on the number of row or column types. -/
+theorem existsAbsoluteResidualQTotalBound_of_degreeCaps :
+    ∃ κ : ENNReal, 0 < κ ∧ κ ≠ ∞ ∧
+      ∀ {A : Type u} {B : Type v} [Fintype A] [Fintype B]
+          [DecidableEq A] [DecidableEq B]
+          (M : Finset (A × B)) (U R m : ℕ)
+          (row : A → ℕ) (col : B → ℕ),
+        0 < m →
+        (∑ a, row a) = m →
+        (∑ b, col b) = m →
+        (∀ a, row a ≤ U) →
+        (∀ b, col b ≤ U) →
+        R = U / 2 →
+        2 ^ U ≤ m ^ 3 →
+        (∑ a, ∑ b, residualQ M R row col a b) ≤
+          κ * (U : ENNReal) ^ 2 := by
+  obtain ⟨K, hKpos, hKtop, hquadratic⟩ :=
+    existsAbsoluteResidualQQuadraticBound
+  have heulerPos : 0 < eulerENNReal := by
+    rw [eulerENNReal, ENNReal.ofReal_pos]
+    exact Real.exp_pos 1
+  have heulerTop : eulerENNReal ≠ ∞ := ENNReal.ofReal_ne_top
+  refine ⟨K * eulerENNReal ^ 2,
+    ENNReal.mul_pos hKpos.ne' (pow_ne_zero 2 heulerPos.ne'),
+    ENNReal.mul_ne_top hKtop (ENNReal.pow_ne_top heulerTop), ?_⟩
+  intro A B _ _ _ _ M U R m row col hm hrowTotal hcolTotal
+    hrowCap hcolCap hR hpow
+  have htheta : ∀ a b, (a, b) ∉ M →
+      (configurationCellTheta row col m a b).toReal ≤
+        Real.exp 1 * (U : ℝ) ^ 2 / (m : ℝ) := by
+    intro a b _
+    exact configurationCellTheta_toReal_le_of_caps
+      row col m U a b hm (hrowCap a) (hcolCap b)
+  have hqtheta : ∀ a b,
+      residualQ M R row col a b ≤
+        K * configurationCellTheta row col m a b ^ 2 :=
+    hquadratic M U R m row col hm hrowTotal hR htheta hpow
+  calc
+    (∑ a, ∑ b, residualQ M R row col a b) ≤
+        ∑ a, ∑ b,
+          K * configurationCellTheta row col m a b ^ 2 := by
+      exact Finset.sum_le_sum fun a _ =>
+        Finset.sum_le_sum fun b _ => hqtheta a b
+    _ = K * (∑ a, ∑ b,
+          configurationCellTheta row col m a b ^ 2) := by
+      rw [Finset.mul_sum]
+      apply Finset.sum_congr rfl
+      intro a _
+      rw [Finset.mul_sum]
+    _ ≤ K * (eulerENNReal ^ 2 * (U : ENNReal) ^ 2) :=
+      mul_le_mul_right
+        (sum_configurationCellTheta_sq_le_euler_sq_cap_sq
+          row col m U hm hrowCap hcolCap hrowTotal hcolTotal) K
+    _ = (K * eulerENNReal ^ 2) * (U : ENNReal) ^ 2 := by
+      ring
+
+/-- The literal event-restricted attachment numerator inherits the direct
+matching-restriction product bound through the exact fixed-family Fubini
+identity. -/
+theorem residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (M : Finset (A × B)) (R : ℕ) (row : A → ℕ) (col : B → ℕ)
+    (htotal : Finset.univ.sum row = Finset.univ.sum col)
+    (hm : 0 < Finset.univ.sum row)
+    (hM : IsBipartiteMatching M) :
+    residualActualAttachmentNumerator M R row col htotal ≤
+      (∏ a : A, ∏ b : B, (1 + residualLambda M R row col a b)) *
+      (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        (1 + residualQ M R row col e.1 e.2)) := by
+  rw [residualActualAttachmentNumerator_eq_residualCappedEvenFixedFSum]
+  exact residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct
+    M R row col htotal hm hM
+
+/-- Generic exponential endpoint for the lambda product and the direct
+outside-matching residual-q product. -/
+theorem lambda_matching_products_le_exp_of_sum_bounds
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (lambda q : A → B → ENNReal) (M : Finset (A × B))
+    (lambdaBound qBound : ENNReal)
+    (hlambda : (∑ a, ∑ b, lambda a b) ≤ lambdaBound)
+    (hq : (∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+      q e.1 e.2) ≤ qBound) :
+    ((∏ a, ∏ b, (1 + lambda a b)) *
+      (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        (1 + q e.1 e.2))) ≤
+      EReal.exp (((lambdaBound + qBound : ENNReal) : EReal)) := by
+  have hlambdaProduct :
+      (∏ a, ∏ b, (1 + lambda a b)) ≤
+        EReal.exp (((∑ a, ∑ b, lambda a b : ENNReal) : EReal)) := by
+    rw [← Fintype.prod_prod_type', ← Fintype.sum_prod_type']
+    exact ennreal_polymer_product_le_ereal_exp_sum
+      (Finset.univ : Finset (A × B)) (fun x => lambda x.1 x.2)
+  have hqProduct :
+      (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        (1 + q e.1 e.2)) ≤
+        EReal.exp (((∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          q e.1 e.2 : ENNReal) : EReal)) :=
+    ennreal_polymer_product_le_ereal_exp_sum
+      ((Finset.univ : Finset (A × B)) \ M) (fun e => q e.1 e.2)
+  calc
+    ((∏ a, ∏ b, (1 + lambda a b)) *
+        (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          (1 + q e.1 e.2))) ≤
+      EReal.exp (((∑ a, ∑ b, lambda a b : ENNReal) : EReal)) *
+        EReal.exp (((∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          q e.1 e.2 : ENNReal) : EReal)) :=
+      mul_le_mul' hlambdaProduct hqProduct
+    _ = EReal.exp
+        ((((∑ a, ∑ b, lambda a b : ENNReal) : EReal)) +
+          (((∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+            q e.1 e.2 : ENNReal) : EReal))) := by
+      rw [EReal.exp_add]
+    _ = EReal.exp
+        ((((∑ a, ∑ b, lambda a b : ENNReal) +
+          ∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+            q e.1 e.2 : ENNReal) : EReal)) := by
+      rw [EReal.coe_ennreal_add]
+    _ ≤ EReal.exp (((lambdaBound + qBound : ENNReal) : EReal)) := by
+      rw [EReal.exp_le_exp_iff, EReal.coe_ennreal_le_coe_ennreal_iff]
+      exact add_le_add hlambda hq
+
+/-- Direct finite large-residual attachment envelope.  It has no traversal
+parameter and no dependence on the number of profile blocks or matching edges. -/
+theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope :
+    ∃ kappaLambda kappaQ : ENNReal,
+      0 < kappaLambda ∧ kappaLambda ≠ ∞ ∧
+      0 < kappaQ ∧ kappaQ ≠ ∞ ∧
+      ∀ {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
+            (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) +
+              kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) := by
+  obtain ⟨kappaLambda, hkLpos, hkLtop, hkL⟩ :=
+    existsAbsoluteResidualLambdaTotalBound
+  obtain ⟨kappaQ, hkQpos, hkQtop, hkQ⟩ :=
+    existsAbsoluteResidualQTotalBound_of_degreeCaps
+  refine ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, ?_⟩
+  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 hlambda :=
+    hkL M U (U / 2) m row col hm hrow hcol hrowCap hcolCap rfl hpow
+  have hqAll :=
+    hkQ M U (U / 2) m row col hm hrow hcol hrowCap hcolCap rfl hpow
+  have hqFull :
+      (∑ e : A × B, residualQ M (U / 2) row col e.1 e.2) ≤
+        kappaQ * (U : ENNReal) ^ 2 := by
+    simpa only [Fintype.sum_prod_type'] using hqAll
+  have hqOutside :
+      (∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        residualQ M (U / 2) row col e.1 e.2) ≤
+        kappaQ * (U : ENNReal) ^ 2 := by
+    calc
+      (∑ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          residualQ M (U / 2) row col e.1 e.2) ≤
+        ∑ e ∈ (Finset.univ : Finset (A × B)),
+          residualQ M (U / 2) row col e.1 e.2 := by
+        exact Finset.sum_le_sum_of_subset Finset.sdiff_subset
+      _ = ∑ e : A × B,
+          residualQ M (U / 2) row col e.1 e.2 := by
+        simp
+      _ ≤ kappaQ * (U : ENNReal) ^ 2 := hqFull
+  have hproduct :=
+    lambda_matching_products_le_exp_of_sum_bounds
+      (residualLambda M (U / 2) row col)
+      (residualQ M (U / 2) row col) M
+      (kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal))
+      (kappaQ * (U : ENNReal) ^ 2) hlambda hqOutside
+  exact hbridge.trans hproduct
+
+#print axioms sum_configurationCellTheta_sq_global
+#print axioms sum_configurationCellTheta_sq_le_euler_sq_cap_sq
+#print axioms existsAbsoluteResidualQTotalBound_of_degreeCaps
+#print axioms residualActualAttachmentNumerator_le_lambdaProduct_mul_matchingProduct
+#print axioms lambda_matching_products_le_exp_of_sum_bounds
+#print axioms exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope
+
+end
+
+end Erdos625
diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean b/625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean
new file mode 100644
index 00000000..8b0b7352
--- /dev/null
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean
@@ -0,0 +1,140 @@
+import Erdos625.Section9FixedFEvenAggregation
+import Erdos625.EvenMatchingRestriction
+import Mathlib.Tactic
+
+/-!
+# Section IX: direct product bound from matching restriction
+
+For an exposed bipartite matching `M`, an even edge set is uniquely determined
+by its restriction outside `M`.  This gives a direct subset-product bound for
+the weighted even-family sum and avoids the cycle/polymer decomposition at the
+finite algebraic level.
+
+The final theorem composes this injection with the already checked fixed-`F`
+aggregation.  It does not identify the fixed-`F` sum with the actual tagged
+attachment expectation, prove the residual-`q` analytic envelope, or establish
+Lemma 9.1.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+/-- On the finite family of even bipartite edge sets, deleting a matching is
+injective.  Equivalently, an even completion of a prescribed outside-matching
+edge set is unique when it exists. -/
+theorem sdiff_matching_injective_on_bipartiteEvenEdgeSets
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (M : Finset (A × B)) (hM : IsBipartiteMatching M) :
+    ∀ F ∈ bipartiteEvenEdgeSets A B,
+      ∀ G ∈ bipartiteEvenEdgeSets A B,
+        F \ M = G \ M → F = G := by
+  intro F hF G hG hdiff
+  apply bipartiteEdgeMatrix_injective
+  apply evenMatrix_eq_of_eq_on_residual
+    (bipartiteEdgeMatrix F) (bipartiteEdgeMatrix G)
+    (fun a b => (a, b) ∈ M) (fun a b => (a, b) ∉ M)
+  · apply (bipartiteEdgeMatrix_even_iff F).2
+    apply (bipartiteEvenEdgeSet_iff_isBipartiteEven F).2
+    simpa [bipartiteEvenEdgeSets] using hF
+  · apply (bipartiteEdgeMatrix_even_iff G).2
+    apply (bipartiteEvenEdgeSet_iff_isBipartiteEven G).2
+    simpa [bipartiteEvenEdgeSets] using hG
+  · exact hM.1
+  · intro a b _hab
+    by_cases hmem : (a, b) ∈ M
+    · exact Or.inl hmem
+    · exact Or.inr hmem
+  · intro a b _hab
+    by_cases hmem : (a, b) ∈ M
+    · exact Or.inl hmem
+    · exact Or.inr hmem
+  · intro a b hab
+    have hmem : ((a, b) ∈ F) ↔ ((a, b) ∈ G) := by
+      have h := congrArg (fun S : Finset (A × B) => (a, b) ∈ S) hdiff
+      simpa [hab] using h
+    by_cases hFmem : (a, b) ∈ F
+    · have hGmem : (a, b) ∈ G := hmem.mp hFmem
+      simp [bipartiteEdgeMatrix, hFmem, hGmem]
+    · have hGmem : (a, b) ∉ G := by
+        intro hG
+        exact hFmem (hmem.mpr hG)
+      simp [bipartiteEdgeMatrix, hFmem, hGmem]
+
+/-- The weighted even-family sum is bounded directly by the full subset product
+on the cells outside the matching.  No cycle decomposition is used. -/
+theorem weighted_evenSubgraph_ennreal_matching_product
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (q : A → B → ENNReal) (M : Finset (A × B))
+    (hM : IsBipartiteMatching M) :
+    (∑ F ∈ bipartiteEvenEdgeSets A B,
+      edgeWeightOutsideENN q M F) ≤
+      ∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        (1 + q e.1 e.2) := by
+  classical
+  unfold edgeWeightOutsideENN
+  calc
+    (∑ F ∈ bipartiteEvenEdgeSets A B,
+        ∏ e ∈ F \ M, q e.1 e.2) =
+        ∑ S ∈ Finset.image (fun F : Finset (A × B) => F \ M)
+            (bipartiteEvenEdgeSets A B),
+          ∏ e ∈ S, q e.1 e.2 := by
+      symm
+      rw [Finset.sum_image]
+      exact sdiff_matching_injective_on_bipartiteEvenEdgeSets M hM
+    _ ≤ ∑ S ∈ Finset.powerset
+          ((Finset.univ : Finset (A × B)) \ M),
+          ∏ e ∈ S, q e.1 e.2 := by
+      apply Finset.sum_le_sum_of_subset
+      exact Finset.image_subset_iff.mpr fun F _hF =>
+        Finset.mem_powerset.mpr (by
+          intro e he
+          exact Finset.mem_sdiff.mpr
+            ⟨Finset.mem_univ e, (Finset.mem_sdiff.mp he).2⟩)
+    _ = ∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          (1 + q e.1 e.2) := by
+      simp +decide [Finset.prod_add, add_comm]
+
+/-- Direct matching-restriction replacement for the polymer-product endpoint
+in the finite capped fixed-`F` aggregation. -/
+theorem residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct
+    {A B : Type*} [Fintype A] [Fintype B]
+    [DecidableEq A] [DecidableEq B]
+    (M : Finset (A × B)) (R : ℕ) (row : A → ℕ) (col : B → ℕ)
+    (htotal : Finset.univ.sum row = Finset.univ.sum col)
+    (hm : 0 < Finset.univ.sum row)
+    (hM : IsBipartiteMatching M) :
+    residualCappedEvenFixedFSum M R row col htotal ≤
+      (∏ a : A, ∏ b : B,
+        (1 + residualLambda M R row col a b)) *
+      (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+        (1 + residualQ M R row col e.1 e.2)) := by
+  calc
+    residualCappedEvenFixedFSum M R row col htotal ≤
+        (∏ a : A, ∏ b : B,
+          (1 + residualLambda M R row col a b)) *
+        (∑ F ∈ bipartiteEvenEdgeSets A B,
+          edgeWeightOutsideENN (residualQ M R row col) M F) :=
+      residualCappedEvenFixedFSum_le_lambdaProduct_mul_evenWeightSum
+        M R row col htotal hm
+    _ ≤
+        (∏ a : A, ∏ b : B,
+          (1 + residualLambda M R row col a b)) *
+        (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          (1 + residualQ M R row col e.1 e.2)) :=
+      mul_le_mul_right
+        (weighted_evenSubgraph_ennreal_matching_product
+          (residualQ M R row col) M hM)
+        _
+
+#print axioms sdiff_matching_injective_on_bipartiteEvenEdgeSets
+#print axioms weighted_evenSubgraph_ennreal_matching_product
+#print axioms residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct
+
+end
+
+end Erdos625
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/Section9ProfileAttachmentMatchingEnvelope.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean
new file mode 100644
index 00000000..b95852c7
--- /dev/null
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean
@@ -0,0 +1,68 @@
+import Erdos625.Section9MatchingRestrictionEnvelope
+import Erdos625.Section9CanonicalDemandProductSpecialization
+import Erdos625.Section8ProfileSkeletonWeight
+
+/-!
+# Section IX: attained-profile matching-restriction envelope
+
+This module specializes the direct finite matching-restriction attachment
+bound to the canonical reference witness of an attained profile high skeleton.
+It keeps the literal cap/no-return attachment observable and introduces no
+cycle traversal or polymer majorant.
+
+No asymptotic profile substitution or Section VIII skeleton summation is made.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- The direct matching-restriction envelope applies uniformly to every
+attained profile high skeleton, with the residual degrees supplied by its
+canonical reference witness. -/
+theorem exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope :
+    ∃ kappaLambda kappaQ : ENNReal,
+      0 < kappaLambda ∧ kappaLambda ≠ ∞ ∧
+      0 < kappaQ ∧ kappaQ ≠ ∞ ∧
+      ∀ {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
+            (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) +
+              kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) := by
+  obtain ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, hbound⟩ :=
+    exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope
+  refine ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, ?_⟩
+  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
+
+#print axioms exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope
+
+end
+
+end Erdos625
diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean
new file mode 100644
index 00000000..97c5a1e1
--- /dev/null
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean
@@ -0,0 +1,199 @@
+import Erdos625.Section9ProfileAttachmentMatchingEnvelope
+import Erdos625.Section9PhaseTwoPowerCorridor
+import Erdos625.Section9ResidualRegimeScaleAdapters
+import Erdos625.Section9ERealENNRealExpTransport
+
+/-!
+# Section IX: direct matching-restriction profile log scale
+
+This module specializes the direct attained-profile attachment envelope to the
+large-residual midpoint scale.  The new finite exponent
+
+`kappaLambda * U^4 / m + kappaQ * U^2`
+
+is uniformly `O((log n)^2)` when `U <= phaseNat n` and
+`m >= n / (log n)^6`.  No type-cardinality, matching-cardinality, or traversal
+parameter remains.
+
+The theorem is still pointwise in an attained canonical skeleton.  It does not
+sum the Section VIII skeleton weights or prove the final random-graph event.
+-/
+
+namespace Erdos625
+
+open Filter
+open scoped ENNReal Topology
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- Exact real arithmetic for the direct matching-restriction exponent. -/
+theorem matchingRestrictionEnvelope_bound
+    (n L U m kappaLambda kappaQ C_U : ℝ)
+    (hn : 0 < n)
+    (hL : 0 < L)
+    (hU0 : 0 ≤ U)
+    (hm0 : 0 < m)
+    (hkappaLambda0 : 0 ≤ kappaLambda)
+    (hkappaQ0 : 0 ≤ kappaQ)
+    (_hCU0 : 0 ≤ C_U)
+    (hm : n / L ^ 6 ≤ m)
+    (hU : U ≤ C_U * L)
+    (hL8 : L ^ 8 ≤ n) :
+    kappaLambda * U ^ 4 / m + kappaQ * U ^ 2 ≤
+      (kappaLambda * C_U ^ 4 + kappaQ * C_U ^ 2) * L ^ 2 := by
+  have hn_le_mL6 : n ≤ m * L ^ 6 := by
+    rwa [div_le_iff₀ (pow_pos hL 6)] at hm
+  have h1m_le_L6n : 1 / m ≤ L ^ 6 / n := by
+    rw [div_le_div_iff₀ hm0 hn]
+    simpa [mul_comm] using hn_le_mL6
+  have hU4 : U ^ 4 ≤ (C_U * L) ^ 4 :=
+    pow_le_pow_left₀ hU0 hU 4
+  have hL10_div_n_le_L2 : L ^ 10 / n ≤ L ^ 2 := by
+    rw [div_le_iff₀ hn]
+    calc
+      L ^ 10 = L ^ 2 * L ^ 8 := by ring
+      _ ≤ L ^ 2 * n :=
+        mul_le_mul_of_nonneg_left hL8 (by positivity)
+  have hterm1Base : U ^ 4 / m ≤ C_U ^ 4 * L ^ 2 := by
+    calc
+      U ^ 4 / m = U ^ 4 * (1 / m) := by ring
+      _ ≤ (C_U * L) ^ 4 * (L ^ 6 / n) :=
+        mul_le_mul hU4 h1m_le_L6n (by positivity) (by positivity)
+      _ = C_U ^ 4 * (L ^ 10 / n) := by ring
+      _ ≤ C_U ^ 4 * L ^ 2 :=
+        mul_le_mul_of_nonneg_left hL10_div_n_le_L2 (by positivity)
+  have hterm1 : kappaLambda * U ^ 4 / m ≤
+      kappaLambda * C_U ^ 4 * L ^ 2 := by
+    calc
+      kappaLambda * U ^ 4 / m = kappaLambda * (U ^ 4 / m) := by ring
+      _ ≤ kappaLambda * (C_U ^ 4 * L ^ 2) :=
+        mul_le_mul_of_nonneg_left hterm1Base hkappaLambda0
+      _ = kappaLambda * C_U ^ 4 * L ^ 2 := by ring
+  have hU2 : U ^ 2 ≤ (C_U * L) ^ 2 :=
+    pow_le_pow_left₀ hU0 hU 2
+  have hterm2 : kappaQ * U ^ 2 ≤
+      kappaQ * C_U ^ 2 * L ^ 2 := by
+    calc
+      kappaQ * U ^ 2 ≤ kappaQ * (C_U * L) ^ 2 :=
+        mul_le_mul_of_nonneg_left hU2 hkappaQ0
+      _ = kappaQ * C_U ^ 2 * L ^ 2 := by ring
+  calc
+    kappaLambda * U ^ 4 / m + kappaQ * U ^ 2 ≤
+        kappaLambda * C_U ^ 4 * L ^ 2 +
+          kappaQ * C_U ^ 2 * L ^ 2 := add_le_add hterm1 hterm2
+    _ = (kappaLambda * C_U ^ 4 + kappaQ * C_U ^ 2) * L ^ 2 := by
+      ring
+
+/-- Eventually `(log n)^8 <= n`, in the exact form used by the direct
+large-residual envelope. -/
+theorem eventually_log_pow_eight_le_nat :
+    ∀ᶠ n : ℕ in atTop, Real.log (n : ℝ) ^ 8 ≤ (n : ℝ) := by
+  have hlim : Tendsto
+      (fun n : ℕ => Real.log (n : ℝ) ^ 8 / (n : ℝ)) atTop (nhds 0) :=
+    Real.isLittleO_pow_log_id_atTop.tendsto_div_nhds_zero.comp
+      tendsto_natCast_atTop_atTop
+  filter_upwards [hlim.eventually (gt_mem_nhds zero_lt_one),
+    eventually_gt_atTop 0] with n hn hn0
+  rw [div_lt_one (by positivity)] at hn
+  linarith
+
+/-- The finite direct exponent is finite whenever its constants are finite and
+its residual mass is positive. -/
+theorem matchingRestrictionEnvelope_ne_top
+    (kappaLambda kappaQ : ENNReal) (U m : ℕ)
+    (hkappaLambdaTop : kappaLambda ≠ ∞)
+    (hkappaQTop : kappaQ ≠ ∞)
+    (hm : 0 < m) :
+    (kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) +
+      kappaQ * (U : ENNReal) ^ 2) ≠ ∞ := by
+  have hUTop : (U : ENNReal) ≠ ∞ := ENNReal.natCast_ne_top U
+  have hm0 : (m : ENNReal) ≠ 0 := by
+    exact_mod_cast hm.ne'
+  have hlambdaTop :
+      kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) ≠ ∞ :=
+    ENNReal.div_ne_top
+      (ENNReal.mul_ne_top hkappaLambdaTop (ENNReal.pow_ne_top hUTop)) hm0
+  have hqTop : kappaQ * (U : ENNReal) ^ 2 ≠ ∞ :=
+    ENNReal.mul_ne_top hkappaQTop (ENNReal.pow_ne_top hUTop)
+  exact ENNReal.add_ne_top.mpr ⟨hlambdaTop, hqTop⟩
+
+/-- The attained-profile direct matching-restriction attachment is uniformly
+`exp(O((log n)^2))` in the large-residual regime. -/
+theorem eventually_profileHighSkeletonAttachment_le_matching_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,
+            (n : ℝ) / Real.log (n : ℝ) ^ 6 ≤
+              (canonicalDemandResidualTotal (profileBlockMargin k)
+                (profileBlockMargin k) U demand : ℝ) →
+            profileHighSkeletonAttachment row0 U demand ≤
+              ENNReal.ofReal
+                (Real.exp (C * Real.log (n : ℝ) ^ 2)) := by
+  obtain ⟨kappaLambda, kappaQ, hkLpos, hkLtop, hkQpos, hkQtop, hfinite⟩ :=
+    exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope
+  let C : ℝ := kappaLambda.toReal * 4 ^ 4 + kappaQ.toReal * 4 ^ 2
+  have hC : 0 ≤ C := by
+    dsimp [C]
+    positivity
+  refine ⟨C, hC, ?_⟩
+  filter_upwards
+    [eventually_phaseControlled_two_pow_le_cube,
+      eventually_logOrder_le_phaseNat_and_phaseNat_le_four_logOrder,
+      eventually_log_pow_eight_le_nat,
+      eventually_gt_atTop (1 : ℕ)] with n hpow hphase hlog8 hn
+  intro b k row0 U hU hcap demand hm
+  let m := canonicalDemandResidualTotal (profileBlockMargin k)
+    (profileBlockMargin k) U demand
+  have hlog : 0 < Real.log (n : ℝ) := Real.log_pos (by exact_mod_cast hn)
+  have hmpos : 0 < m := by
+    have : 0 < (m : ℝ) := lt_of_lt_of_le
+      (div_pos (by positivity) (pow_pos hlog 6)) hm
+    exact_mod_cast this
+  have hbase := hfinite row0 U m hcap demand rfl hmpos
+    (hpow U m hU hmpos hm)
+  let exponent : ENNReal :=
+    kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) +
+      kappaQ * (U : ENNReal) ^ 2
+  have hexponent : exponent ≠ ∞ := by
+    exact matchingRestrictionEnvelope_ne_top
+      kappaLambda kappaQ U m hkLtop hkQtop hmpos
+  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 hUreal : (U : ℝ) ≤ 4 * Real.log (n : ℝ) :=
+    (Nat.cast_le.mpr hU).trans hphase.2
+  have henv := matchingRestrictionEnvelope_bound
+    (n : ℝ) (Real.log (n : ℝ)) (U : ℝ) (m : ℝ)
+    kappaLambda.toReal kappaQ.toReal 4
+    (by positivity) hlog (Nat.cast_nonneg U) (by exact_mod_cast hmpos)
+    ENNReal.toReal_nonneg ENNReal.toReal_nonneg (by norm_num)
+    hm hUreal hlog8
+  have hparts := ENNReal.add_ne_top.mp hexponent
+  rw [ENNReal.toReal_add hparts.1 hparts.2]
+  simp only [ENNReal.toReal_mul, ENNReal.toReal_div,
+    ENNReal.toReal_pow, ENNReal.toReal_natCast]
+  change
+    kappaLambda.toReal * (U : ℝ) ^ 4 / (m : ℝ) +
+      kappaQ.toReal * (U : ℝ) ^ 2 ≤
+        C * Real.log (n : ℝ) ^ 2
+  simpa [C] using henv
+
+#print axioms matchingRestrictionEnvelope_bound
+#print axioms eventually_log_pow_eight_le_nat
+#print axioms matchingRestrictionEnvelope_ne_top
+#print axioms eventually_profileHighSkeletonAttachment_le_matching_logScale
+
+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/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
new file mode 100644
index 00000000..7c412a2b
--- /dev/null
+++ b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
@@ -0,0 +1,125 @@
+# Audit: direct matching-restriction attachment envelope
+
+## Scope
+
+This audit accompanies:
+
+- `Erdos625/Section9MatchingRestrictionEnvelope.lean`;
+- `Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean`;
+- `Erdos625/Section9ProfileAttachmentMatchingLogScale.lean`.
+
+The branch is stacked on PR #34 and therefore assumes the finite
+matching-restriction product theorem from
+`Section9MatchingRestrictionProduct.lean`.
+
+## New checked targets
+
+The first module is intended to prove the following finite statements.
+
+1. The complete square mass of the configuration-cell parameters factorizes as
+
+   \[
+   \sum_{a,b}\theta_{ab}^2
+   =\left(\frac e m\right)^2
+     \left(\sum_a d_a^2\right)
+     \left(\sum_b (d_b')^2\right).
+   \]
+
+2. If both degree families have common positive total `m` and are capped by
+   `U`, then
+
+   \[
+   \sum_{a,b}\theta_{ab}^2\le e^2U^2.
+   \]
+
+3. The existing pointwise quadratic bound on `residualQ` therefore sums to
+
+   \[
+   \sum_{a,b}q_{ab}\le \kappa_Q U^2
+   \]
+
+   for one absolute positive finite constant.
+
+4. The exact fixed-family Fubini identity transports the direct product theorem
+   of PR #34 to the literal event-restricted attachment numerator.
+
+5. Combining the lambda and residual-q products gives
+
+   \[
+   \mathcal A(M,j)
+   \le
+   \exp\!\left(
+      \kappa_\Lambda\frac{U^4}{m}
+      +\kappa_Q U^2
+   \right).
+   \]
+
+The second module specializes this statement to every attained profile high
+skeleton by using its canonical reference witness, literal positive-demand
+matching support, residual degree caps, equal residual totals, and the exact
+definition of `profileHighSkeletonAttachment`.
+
+The third module proves the exact real arithmetic
+
+\[
+ \kappa_\Lambda\frac{U^4}{m}+\kappa_Q U^2
+ \le
+ (\kappa_\Lambda C_U^4+\kappa_Q C_U^2)L^2
+\]
+
+under `m >= n/L^6`, `U <= C_U L`, and `L^8 <= n`. It then proves the eventual
+phase specialization
+
+\[
+ \operatorname{profileHighSkeletonAttachment}
+ \le \exp\!\bigl(C(\log n)^2\bigr)
+\]
+
+uniformly over all attained profile high skeletons in the large-residual
+regime.
+
+The resulting profile theorem has no traversal parameter, no factor depending
+on the number of profile blocks, and no factor depending on the number of
+matching edges.
+
+## Dependencies reused
+
+- `residualActualAttachmentNumerator_eq_residualCappedEvenFixedFSum`;
+- `residualCappedEvenFixedFSum_le_lambdaProduct_mul_matchingProduct` from the
+  stacked PR #34;
+- `existsAbsoluteResidualQQuadraticBound`;
+- `existsAbsoluteResidualLambdaTotalBound`;
+- exact degree-square and configuration-theta identities from
+  `ConfigurationThetaMoments.lean`;
+- `ennreal_polymer_product_le_ereal_exp_sum` for finite products;
+- `canonicalReference_residual_parameters` and
+  `profileBlockMargin_total_eq_self` for the attained-profile specialization;
+- the existing phase upper bound, residual two-power corridor, and logarithmic
+  little-o infrastructure for the `O((log n)^2)` adapter.
+
+## Trust gates
+
+The focused workflow:
+
+- rejects `sorry`, `admit`, `sorryAx`, project `axiom`/`constant`, and `unsafe`;
+- prepares the pinned Lean 4.31/mathlib project;
+- builds the log-square profile endpoint and its complete dependency closure
+  with `--wfail`;
+- prints the axioms of every new public theorem.
+
+The ordinary repository Lean workflow also runs because this PR changes the
+formalization tree.
+
+## Deliberate boundary
+
+These modules still do not prove the complete Erdős 625 theorem. In particular
+they do not:
+
+- sum the Section VIII bare skeleton weights;
+- update the root aggregate or generated self-contained checkpoint;
+- prove the chromatic lower tail, rare seed, or final event intersection;
+- combine the large-residual log-square estimate with the small-residual branch
+  into one profile-level two-regime theorem on this branch.
+
+The next integration step, after review, is the Section VIII skeleton sum and a
+single two-regime profile theorem using this direct large-residual endpoint.
diff --git a/625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md
new file mode 100644
index 00000000..0deffde8
--- /dev/null
+++ b/625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md
@@ -0,0 +1,66 @@
+# Matching-restriction product formalization audit
+
+**Date:** 25 July 2026  
+**Target module:** `Erdos625/Section9MatchingRestrictionProduct.lean`  
+**Status:** focused finite Lean checkpoint; not Lemma 9.1 or `Erdos625Statement`.
+
+## Exact claims
+
+The module proves three finite statements.
+
+1. If `M` is a bipartite matching, the map
+
+   ```text
+   F ↦ F \ M
+   ```
+
+   is injective on the finite family of bipartite even edge sets.
+
+2. For arbitrary `ENNReal` cell weights,
+
+   ```text
+   sum_{F even} product_{e in F\M} q_e
+     <= product_{e notin M} (1 + q_e).
+   ```
+
+3. The existing capped fixed-`F` aggregation is bounded by the common local
+   `residualLambda` product times this direct outside-matching product.
+
+## Proof dependencies
+
+The proof reuses only accepted finite modules:
+
+- `BipartiteEdgeMatrix.lean` for the injective zero-one incidence encoding and
+  the equivalence between even edge sets and zero row/column sums over
+  `ZMod 2`;
+- `EvenMatchingRestriction.lean` for uniqueness of an even matrix after its
+  values away from a row matching are fixed;
+- `Section9ActualResidualENNRealPolymerBridge.lean` for the definition of
+  `edgeWeightOutsideENN` and the finite even-edge family;
+- `Section9FixedFEvenAggregation.lean` for the previously checked fixed-`F`
+  threshold expansion and aggregation.
+
+No cycle decomposition, walk kernel, marked-cycle encoder, asymptotic estimate,
+probability conditioning, or external theorem is used.
+
+## Trust checks
+
+The source contains no `sorry`, `admit`, project-defined `axiom`, `constant`, or
+`unsafe` declaration.  Each public theorem is followed by `#print axioms`.
+The focused workflow compiles the module with `-DwarningAsError=true`; the full
+repository Lean workflow also builds every formalization module with `--wfail`.
+
+## Deliberate boundary
+
+This checkpoint does not prove the manuscript's complete large-residual
+attachment estimate.  Remaining bridges include:
+
+1. the precise tagged-law identification of the actual attachment numerator;
+2. a finite bound on the direct product in terms of the total `residualQ` mass;
+3. the deterministic estimate
+   `sum residualQ = O(U^2 + U^4/m_0)` under the large-residual hypotheses;
+4. the asymptotic specialization to `exp(O((log n)^2))`;
+5. the global Section 8 skeleton sum and Proposition 9.2.
+
+The module is therefore a genuine simplification of the finite Section IX
+algebra, but not a completed proof of the theorem.
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.