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/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/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.