diff --git a/.github/workflows/erdos625-full-proof-audit.yml b/.github/workflows/erdos625-full-proof-audit.yml
new file mode 100644
index 00000000..49aaf2cb
--- /dev/null
+++ b/.github/workflows/erdos625-full-proof-audit.yml
@@ -0,0 +1,111 @@
+name: Erdős 625 full proof audit
+
+on:
+  pull_request:
+    paths:
+      - "625/audits/FULL_THEOREM_LEMMA_AUDIT_2026-07-25.md"
+      - "625/audits/POST_INTEGRATION_STATUS_2026-07-25.md"
+      - "625/proofs/SECTION8_GLOBAL_DECORATION_BRIDGE.md"
+      - "625/proofs/TRANSFERABLE_RESULTS_AND_COROLLARIES_2026-07-25.md"
+      - "625/experiments/full_proof_audit_regression.py"
+      - "625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean"
+      - "625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean"
+      - "625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean"
+      - ".github/workflows/erdos625-full-proof-audit.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-full-audit-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  audit-regression:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Compile audit checker
+        run: python -m py_compile 625/experiments/full_proof_audit_regression.py
+      - name: Run exact audit checks
+        run: python 625/experiments/full_proof_audit_regression.py
+      - name: Run audit checks with optimization enabled
+        run: python -O 625/experiments/full_proof_audit_regression.py
+
+  focused-section8-repair:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in repaired modules
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean \
+            625/formalization/Erdos625/Section8AllHighDeficitProductBound.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 Section 8 simplification dependency closure warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section8SimplificationCore --wfail \
+            > /tmp/erdos625-full-audit-section8.log 2>&1
+          status=$?
+          tail -n 500 /tmp/erdos625-full-audit-section8.log
+          exit $status
+      - name: Upload focused Section 8 compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-full-audit-section8-log
+          path: /tmp/erdos625-full-audit-section8.log
+          if-no-files-found: ignore
+
+  focused-section9-frontier:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in the frontier module
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.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 exact q-only second-moment frontier warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9QOnlySecondMomentFrontier --wfail \
+            > /tmp/erdos625-full-audit-section9.log 2>&1
+          status=$?
+          tail -n 500 /tmp/erdos625-full-audit-section9.log
+          exit $status
+      - name: Upload focused Section 9 compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-full-audit-section9-log
+          path: /tmp/erdos625-full-audit-section9.log
+          if-no-files-found: ignore
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..2a3d3c74
--- /dev/null
+++ b/.github/workflows/erdos625-matching-restriction-product.yml
@@ -0,0 +1,57 @@
+name: Erdős 625 matching-restriction product
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/FiniteRestrictionProduct.lean"
+      - "625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean"
+      - "625/formalization/MATCHING_RESTRICTION_PRODUCT_AUDIT.md"
+      - ".github/workflows/erdos625-matching-restriction-product.yml"
+  workflow_dispatch:
+
+concurrency:
+  group: erdos625-matching-restriction-product-${{ 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 in the finite modules
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/FiniteRestrictionProduct.lean \
+            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: false
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Build the matching-restriction product warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          set +e
+          lake build Erdos625.Section9MatchingRestrictionProduct --wfail \
+            > /tmp/section9-matching-restriction-product.log 2>&1
+          status=$?
+          tail -n 500 /tmp/section9-matching-restriction-product.log
+          exit $status
+      - name: Upload focused compiler log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: erdos625-matching-restriction-product-log
+          path: /tmp/section9-matching-restriction-product.log
+          if-no-files-found: ignore
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/audits/FULL_THEOREM_LEMMA_AUDIT_2026-07-25.md b/625/audits/FULL_THEOREM_LEMMA_AUDIT_2026-07-25.md
new file mode 100644
index 00000000..b6a7a419
--- /dev/null
+++ b/625/audits/FULL_THEOREM_LEMMA_AUDIT_2026-07-25.md
@@ -0,0 +1,543 @@
+# Erdős Problem 625: full theorem-by-theorem and lemma-by-lemma audit
+
+**Audit date:** 25 July 2026  
+**Canonical text audited:** `625/arxiv/main.tex` on `main`, together with public PRs #27 and #30--#39  
+**Status of this document:** adversarial mathematical review and integration plan; not external peer review and not a declaration that the theorem is proved
+
+## 1. Executive verdict
+
+The candidate manuscript has a coherent global strategy and a large sound core. I found no contradiction in the location calculation (Sections 2--5), the exact signed overlap identities (Section 6), the partial-diagonal estimate (Section 7), or the rare-seed amplification (Section 10). The final event intersection in Section 11 is also correct once its inputs are available.
+
+The proof should nevertheless **not yet be described as closed**. The load-bearing unresolved boundary is concentrated in the following two bridges:
+
+1. **Section 8 physical assembly.** The endpoint transportation inequality and the one-cell high-deficit estimates must be transported through the exact labelled/unlabelled quotient, the dependent family of physical endpoint cells, and the global stub-matching normalization. The present public branches contain most finite ingredients, but not one theorem that identifies their product with the complete canonical high-skeleton sum.
+2. **Section 9 asymptotic assembly.** The simplified matching-restriction/q-only attachment theorem must be combined with the attained midpoint profile in both intrinsic residual regimes, including the complementary phase-asymptotic estimate, and then inserted into the exact decomposition defining Proposition 9.2.
+
+These are narrower obligations than the original near/middle/cycle-walk analysis, but they are substantive. Until they are discharged, Proposition 9.2 and hence Theorem 1 remain conditional.
+
+### Audit labels
+
+- **GREEN:** the displayed result and its local proof are logically sound at manuscript level; suggested edits improve exposition or modularity only.
+- **GREEN-FINITE:** an exact finite theorem is kernel-checked or exhaustively regression-tested, but its asymptotic/profile specialization is separate.
+- **AMBER:** the argument is plausible and no counterexample was found, but a quantified bridge, normalization, or uniformity statement is not fully supplied.
+- **BLOCKED:** the stated downstream conclusion depends on an AMBER bridge and must not yet be treated as established.
+- **IMPROVEMENT:** a stronger statement follows from the accepted chain once a short explicit bridge is added.
+
+## 2. Dependency graph
+
+The proof has the following logical spine.
+
+```text
+Lemma 2.1
+   |
+   +--> Lemma 3.1 --> Section 4 chromatic lower location
+   |          |
+   |          +--> Lemma 5.1 --> midpoint profile and root separation
+   |                                      |
+   |                                      +--> Lemmas 6.1--6.2
+   |                                                   |
+   |                                                   +--> Lemma 7.1
+   |                                                           |
+   |                                                           +--> Lemmas 8.1--8.3
+   |                                                                     |
+   |                                                                     +--> Lemma 9.1
+   |                                                                              |
+   |                                                                              +--> Proposition 9.2
+   |                                                                                         |
+   +-----------------------------------------------------------------------------------------+
+                                                                                             |
+                                                               Lemmas 10.1--10.2 <-----------+
+                                                                         |
+                                                                         +--> Section 11 --> Theorem 1
+```
+
+The exact finite overlap algebra in Section 6 is independent of the asymptotic root calculation. Lemma 10.2 is also an abstract amplification mechanism: it needs only a rare seed for a hereditary induced-subgraph feasibility event and a simultaneous leftover-coloring estimate.
+
+## 3. Preliminary inequalities and conventions
+
+### 3.1 Stirling, bounded differences, Paley--Zygmund, binomial tail, Markov
+
+**Verdict: GREEN.**
+
+The manuscript uses standard forms with the correct directions. The binomial estimate
+
+\[
+ \Pr\{\operatorname{Bin}(m,1/2)\le m/4\}\le e^{-m/16}
+\]
+
+is weaker than the sharp Chernoff exponent but sufficient. The one-sided bounded-differences inequalities used later follow from the stated two-sided form.
+
+**Recommended edit.** State once that all asymptotic constants in Sections 2--11 are deterministic and, whenever claimed, uniform over the closed phase interval used for compactness. This prevents later uses of `o(1)` from silently changing quantifier order.
+
+## 4. Section 2: complete independence-number phase
+
+### 4.1 Lemma 2.1 (phase expansion)
+
+**Verdict: GREEN.**
+
+The expansion of `ln mu_alpha` follows from the exact identity
+
+\[
+ \ln\mu_\alpha=\ln(n)_\alpha-\ln(\alpha!)-(\ln2)\binom\alpha2
+\]
+
+and a uniform expansion of `ln alpha`. The adjacent-size ratios in (2.8) are exact. They correctly imply
+
+\[
+ \mu_{\alpha+2}=n^{\delta-2+o(1)}=o(1)
+\]
+
+uniformly in the phase and the lower bound on `mu_(alpha-2)` used in the empty-corner estimate.
+
+The endpoint `delta=1` is used only as a compact limiting endpoint; the actual fractional part lies in `[0,1)`. The formulas extend continuously and uniformly to the closed interval, so this is legitimate.
+
+**Recommended edits.**
+
+1. Add a one-sentence statement that the error in (2.2) is uniform on the closed interval `[0,1]`, with `delta=1` interpreted by continuous extension.
+2. Isolate the adjacent-ratio corollary as a named statement. It is used repeatedly in Sections 4 and 7 and is easier to audit as a reusable lemma.
+
+## 5. Section 3: continuous profile roots
+
+### 5.1 Lemma 3.1 (root phase, derivative, and support comparison)
+
+**Verdict: GREEN, with one modularity improvement.**
+
+The affine-plus-curved decomposition (3.11) is exact. Under the fixed mean constraint, its affine terms cancel, leaving the finite entropy variational problem. The Gaussian upper bound on `h_n(i)` gives uniform summability for the unrestricted support. The tilted mean has derivative equal to a positive variance, so the inverse mean map is well-defined and uniformly Lipschitz on the compact target interval.
+
+The root corridor follows from the sign change of the scalar objective and the uniform derivative
+
+\[
+ \frac{\partial}{\partial k}\{L_S(n,k)+ck\}
+   =\frac{2}{\ln2}(\ln n)^2+O((\ln n)(\ln\ln n)).
+\]
+
+The statement says “unique zero in the root corridor,” not global uniqueness outside that corridor; the proof establishes exactly that claim.
+
+**Required explicit bridge for later constant improvements.** Add a named compactness lemma:
+
+> The limiting value functions `F_(S_+)` and `F_(S_4)`, their optimizing tilts, and `D_4(delta)` are continuous on `delta in [0,1]`.
+
+The proof is already implicit in the uniform convergence/inverse-map argument, but PR #31 needs the conclusion in this explicit form to convert a pointwise strict entropy inequality into a uniform positive margin.
+
+**Recommended decomposition.** Split Lemma 3.1 into:
+
+1. finite/limiting tilt existence and compact convergence;
+2. the exact support-comparison identity;
+3. root corridor and derivative asymptotics.
+
+This does not change the mathematics, but substantially lowers the cognitive load of later citations.
+
+## 6. Section 4: unrestricted chromatic lower location
+
+### 6.1 Profile enumeration and first-moment lower bound
+
+**Verdict: GREEN.**
+
+The exact expectation (4.2) is correct for unordered colorings with a prescribed profile. The number of bounded profiles is at most `(n+1)^(alpha+1)=exp(O((ln n)^2))`, which is negligible compared with the negative displacement `-Theta((ln n)^3)` obtained by moving `ceil(ln n)` parts to the left of the root.
+
+On the event `alpha(G_n)<=alpha+1`, any coloring with at most `k_chi^-` parts can be refined to exactly `k_chi^-` nonempty independent parts of size at most `alpha+1`; for large `n`, `k_chi^-<n`, so splitting is possible. This justifies (4.5).
+
+**Recommended edit.** State `k_chi^-<n` explicitly before invoking refinement. It is immediate from `k_chi^-=Theta(n/ln n)` but removes a hidden finite condition.
+
+## 7. Section 5: signed four-size first moment
+
+### 7.1 Lemma 5.1 (uniform entropy certificate)
+
+**Verdict: GREEN; a strictly stronger certificate is available.**
+
+The tilt bracketing, monotonicity of the omitted low/high ratios, and the dual evaluation are logically correct. The manuscript proves
+
+\[
+ D_4(\delta)<\ln(153/100),\qquad
+ \ln2-D_4(\delta)>\ln(200/153).
+\]
+
+PR #32 supplies a sharper exact rational certificate for the same support:
+
+\[
+ D_4(\delta)<\ln(639/500),\qquad
+ \ln2-D_4(\delta)>\ln(1000/639).
+\]
+
+The latter uses exact rational enclosures for `ln 2`, `2^(1/20)`, both endpoint mean comparisons, and four omitted-weight ratios. It changes neither the profile nor any second-moment argument.
+
+**Integration condition.** The finite-to-limiting convergence from Lemma 3.1 must remain stated uniformly on the entire target interval. No additional probabilistic argument is needed.
+
+### 7.2 Exact integer midpoint profile
+
+**Verdict: GREEN.**
+
+The correction
+
+\[
+ \Delta k_2=e_1-3e_0,\qquad \Delta k_3=2e_0-e_1
+\]
+
+solves both integer conservation equations exactly. Since the four limiting type proportions are uniformly bounded below, the `O(1)` correction preserves positivity. The displacement is tangent to the feasible affine plane, and the entropy Hessian gives only an `O(1/k_co)` loss.
+
+The signed first moment at the midpoint has a uniform positive exponential margin of order `k_co`; this is much larger than all polynomial profile-count losses.
+
+### 7.3 Root separation and theorem constant
+
+**Verdict: IMPROVEMENT.**
+
+Equation (5.11) gives the phase-resolved separation
+
+\[
+ r_+-r_4^{\mathrm{co}}
+ =\left(\frac{(\ln2)^2}{4}\{\ln2-D_4(\delta_n)\}+o(1)\right)
+   \frac{n}{(\ln n)^3}.
+\]
+
+The midpoint retains one half of this separation. The floor/ceiling losses are additive `O(ln n)`, and the amplification loss is `o(n/(ln n)^3)`. Neither causes another fixed halving. Therefore the natural phase-resolved final coefficient is
+
+\[
+ \frac{(\ln2)^2}{8}\{\ln2-D_4(\delta_n)\}.
+\]
+
+To obtain a fixed explicit constant from a strict limiting inequality, define
+
+\[
+ \eta_0:=\min_{0\le\delta\le1}
+  \left[\ln2-D_4(\delta)-\gamma\right].
+\]
+
+Continuity and strict positivity imply `eta_0>0`. The uniform `o(1)` can then be absorbed without halving the target coefficient. With the canonical entropy certificate this gives
+
+\[
+ c=\frac{(\ln2)^2}{8}\ln(200/153),
+\]
+
+four times the displayed constant. Combining PRs #31 and #32 gives
+
+\[
+ \boxed{c=\frac{(\ln2)^2}{8}\ln(1000/639)
+        =0.026896409808379\ldots .}
+\]
+
+This improvement remains conditional on the complete second-moment chain, but it does not require changing that chain.
+
+## 8. Section 6: exact signed second moment
+
+### 8.1 Lemma 6.1 (exact sign sum)
+
+**Verdict: GREEN and independently reusable.**
+
+For two partitions, signs must agree across every overlap cell of size at least two. Hence signs are constant on each connected component of the support graph `H`. The compatible sign-pair count is exactly
+
+\[
+ 2^{2k-|V(H)|+c(H)}.
+\]
+
+After dividing by the square of the one-partition signed probability, the normalized factor is
+
+\[
+ A_\zeta(r)=2^{W+c(H)-|V(H)|}
+ =\left(\prod_{a,b}g(r_{ab})\right)2^{\beta(H)}.
+\]
+
+The second equality follows by separating one binary factor per support edge. The cycle-space identity
+
+\[
+ 2^{\beta(H)}=\#\{F\subseteq E(H):\deg_F(v)\text{ is even for all }v\}
+\]
+
+is exact.
+
+**Paper-strengthening opportunity.** Isolate this as a general proposition for two signed set partitions. It is a clean finite theorem with potential use in other random partition and spin-compatibility problems.
+
+### 8.2 Lemma 6.2 (joint prescribed-cell bound)
+
+**Verdict: GREEN.**
+
+The witness count assigns disjoint row and column stubs to every demanded cell and then pairs them inside each cell. A fixed witness has probability `1/(m_0)_x`; the union bound yields (6.8). The simplification
+
+\[
+ (m_0)_x\ge(m_0/e)^x
+\]
+
+has the correct direction and gives (6.9).
+
+**Recommended edit.** State the `m_0=0` boundary separately wherever the lemma is invoked, although the residual decomposition normally treats it deterministically.
+
+## 9. Section 7: exact partial diagonals
+
+### 9.1 Exact marked identities and recurrences
+
+**Verdict: GREEN.**
+
+The common-subprofile weight `D(ell)`, the forward ratio (7.4), the reverse representation (7.5), and the reverse ratio (7.6) follow by exact factorial cancellation. Marking intentionally overcounts overlaps containing several common blocks; because every term is nonnegative, this is valid for an upper bound.
+
+### 9.2 Lemma 7.1 (all common subprofiles)
+
+**Verdict: GREEN.**
+
+The three ranges are exhaustive:
+
+1. `m<=eta n` (empty corner);
+2. `m>eta n` and `n-m>n/32` (central range);
+3. `n-m<=n/32` (full corner).
+
+In the empty corner, the forward recurrence gives a Poissonized majorant with total intensity `o(1)`. In the central range, the exact Stirling identity reduces the exponent to the rate function
+
+\[
+ \Phi_T(z)=R\ln R+\frac{\ln2}{2}(I_r-TR),
+\]
+
+plus lower-order entropy terms. The manuscript's numerical certificate `Phi_T<=-Y/5000` is sufficient. PR #30 proves the stronger exact rational endpoint certificate
+
+\[
+ \Phi_T\le -Y/100
+\]
+
+on the same domain. In the full corner, the reverse recurrence is decreasing and the exponentially large complete first moment suppresses all residual vectors.
+
+**Recommended integration.** Replace the decimal endpoint checks by the exact rational/logarithmic certificate from PR #30. This is stronger, shorter, and easier to reproduce.
+
+## 10. Section 8: canonical high skeletons
+
+This is the principal unresolved part of the proof.
+
+### 10.1 Lemma 8.1 (geometric-mean transportation comparison)
+
+**Verdict: GREEN-FINITE / AMBER-INTEGRATION.**
+
+The local falling-factorial/log-concavity comparison is algebraically correct. PR #36 proves a denominator-free squared version in Lean, including the exact product identity over the four endpoint types. This is the preferable formal form because it avoids cancellation before positivity is established.
+
+**Remaining manuscript bridge.** State all factorial factors as positive on the feasible domain, then derive the unsquared geometric-mean inequality. Alternatively, keep the complete Section 8 argument square-free and use the AM--GM route of PR #38.
+
+### 10.2 Lemma 8.2 (sum of endpoint tables)
+
+**Verdict: AMBER in the canonical presentation; simplification available.**
+
+The current Cauchy--Schwarz summation is plausible, but it introduces an unnecessary square of a margin sum and a polynomial count of margin vectors. PR #38 observes the termwise implication
+
+\[
+ W(L)\le\sqrt{D(r)A_LD(c)C_L}\,Q^L
+ \quad\Longrightarrow\quad
+ W(L)\le\frac{D(r)A_L+D(c)C_L}{2}Q^L.
+\]
+
+Each half can then be summed by dropping only one family of margin constraints and using a one-sided multinomial expansion. This removes the global Cauchy step and its polynomial loss.
+
+**Required bridge.** The linear endpoint inequality must be stated for the exact physical table weight, not merely for an abstract type table. The quotient by permutations of indistinguishable slots and the dependence of the allowed cells on the endpoint pairing must be included in the theorem statement.
+
+### 10.3 Lemma 8.3 (all nonendpoint high multiplicities)
+
+**Verdict: BLOCKED in the canonical manuscript; promising replacement in PR #38.**
+
+The canonical near/middle split contains several proof-audit hazards:
+
+- asymptotic notation such as `3a/4+O(1)` appears inside finite summation limits and should be replaced by exact floor/ceiling cutoffs;
+- the relation between labelled physical cells, type tables, and the unlabelled canonical skeleton weight is not stated as one disjoint-union/quotient identity;
+- the global allocation of falling-factorial denominators across decorated cells is compressed into prose;
+- the no-return/cap event and the residual attachment are not kept completely separate in every intermediate bound.
+
+PR #38 replaces the near/middle split by one deficit coordinate. If a high cell has endpoint size `m` and multiplicity `j=m-e`, then `2e<m`, and the exact local ratio satisfies
+
+\[
+ n^e R_{m,d}(e)
+ \le\left(\frac{nm}{2^{\lfloor2m/3\rfloor}}\right)^e.
+\]
+
+For the four endpoint sizes this produces a common base
+
+\[
+ \rho_n=O\!\left(\frac{(\ln n)^{7/3}}{n^{1/3}}\right)=o(1),
+\]
+
+and a total all-high decoration cost
+
+\[
+ \exp\{O(n^{2/3}(\ln n)^{4/3})\}
+ =\exp\{o(n/(\ln n)^4)\}.
+\]
+
+The exact arithmetic checker passes. PR #39 repairs two local Lean elaboration failures in the product and one-cell modules. However, the following global obligations remain:
+
+1. identify the physical endpoint-decoration family as an exact dependent finite fibre over endpoint pairings;
+2. transport the one-cell ENNReal bound through the exact stub-matching cardinality ratio;
+3. prove that the product over distinguishable physical cells corresponds to the intended canonical skeleton sum, with no omitted symmetry factor;
+4. combine the endpoint-table and all-high-decoration sums in one quantified theorem uniform over the attained midpoint profile.
+
+Until these are supplied, Lemma 8.3 is not established by the simplified branch.
+
+## 11. Section 9: residual local and cycle attachments
+
+### 11.1 Exact conditional decomposition
+
+**Verdict: GREEN as an identity, subject to the precise definition of the Section 8 skeleton index.**
+
+Once a canonical high skeleton has been exposed and the conditional residual matching law is fixed, the normalized moment decomposes as
+
+\[
+ \frac{\mathbb E Z^2}{(\mathbb EZ)^2}
+ =\sum_{(\mathcal M,j)}w_{\mathrm{hi}}(\mathcal M,j)
+   \mathcal A(\mathcal M,j).
+\]
+
+The high-skeleton index and residual event must match exactly the quotient used in Section 8; this is why the two sections cannot be verified independently at the final assembly step.
+
+### 11.2 Lemma 9.1 (uniform attachment bound)
+
+**Verdict: AMBER canonically; substantially simpler finite route available.**
+
+The manuscript's local-increment expansion and deterministic small-residual bound have correct directions. No explicit counterexample was found to the cycle-kernel argument. Nevertheless, the matching-restriction route is both shorter and less fragile.
+
+Let `M` be the exposed matching. Restriction
+
+\[
+ F\longmapsto F\setminus M
+\]
+
+is injective on even edge sets: if two even sets have the same residual part, their symmetric difference is an even subset of a matching, hence empty. Therefore, for nonnegative residual weights,
+
+\[
+ \sum_{F\text{ even}}\prod_{e\in F\setminus M}q_e
+ \le\prod_{e\notin M}(1+q_e)
+ \le\exp\!\left(\sum_{e\notin M}q_e\right).
+\]
+
+PR #34 kernel-checks this finite theorem. PR #35 carries it to a green `exp(O((ln n)^2))` large-residual profile envelope. PR #37 further observes `lambda_e<=q_e` and proposes the intrinsic split
+
+\[
+ 2^U\le m_0^3
+ \quad\text{versus}\quad
+ m_0<2^{\lceil U/3\rceil}.
+\]
+
+In the first regime, the attachment is `exp(O(U^2))`; in the second, the deterministic bound has exponent `O(U 2^(U/3))=n^(2/3+o(1))` at the midpoint phase.
+
+**Current CI boundary.** PR #37's full repository Lean job is green, but its focused two-regime target is not green at the audited head. The failed exported assembly theorem therefore must not be cited as kernel-checked until the local arithmetic proof is repaired and the focused workflow passes.
+
+**Remaining mathematical bridge.** Prove the complementary phase-asymptotic estimate with the exact midpoint cap `U=(2+o(1))log_2 n`, and package both regimes into one uniform deterministic sequence `epsilon_n->0` at scale `n/(ln n)^4`.
+
+### 11.3 Proposition 9.2 (normalized signed second moment)
+
+**Verdict: BLOCKED.**
+
+The final multiplication is correct:
+
+\[
+ \sup\mathcal A\cdot\sum w_{\mathrm{hi}}
+ \le\exp\{o(n/(\ln n)^4)\}.
+\]
+
+The logarithm is nonnegative because the normalized second moment is at least one. But the proposition depends exactly on the unresolved global Section 8 sum and the Section 9 two-regime adapter. It is the single decisive bottleneck for Theorem 1.
+
+## 12. Section 10: rare-event amplification
+
+### 12.1 Lemma 10.1 (simultaneous leftover coloring)
+
+**Verdict: GREEN.**
+
+A union bound shows that every `n^(1/4)`-set has complement density at least `1/4` with high probability; averaging extends this to every larger set. Iterating maximum-degree neighborhoods in the complement produces an independent set of size `c ln n` inside every set of size at least `n^(1/3)`. Greedy removal yields simultaneously for all `S`
+
+\[
+ \chi(G_n[S])\le C|S|/\ln n+n^{1/3}.
+\]
+
+The constants are deliberately coarse but adequate.
+
+### 12.2 Lemma 10.2 (amplification from a seed)
+
+**Verdict: GREEN and independently reusable.**
+
+The maximum size `S_k` of a `k_n`-cocolorable induced subgraph is one-Lipschitz under vertex-block exposure: deleting the altered vertex transfers a feasible set between the two configurations. The seed event is exactly `S_k=n`. The upper bounded-differences tail converts its probability into a bound on `n-E S_k`; the lower tail then bounds the leftover size. Lemma 10.1 colors the leftover and completes the graph.
+
+The quantifier order is correct: the same simultaneous leftover event works for every deterministic `k_n`, `Lambda_n`, and `r`.
+
+**Paper-strengthening opportunity.** Extract an abstract “rare seed to typical completion” lemma for vertex-hereditary partition properties. This method is useful independently of cochromatic number.
+
+## 13. Section 11 and Theorem 1
+
+### 13.1 Final event intersection
+
+**Verdict: GREEN conditional on Proposition 9.2.**
+
+The chromatic lower event and cocoloring upper event each have probability tending to one. A union bound is sufficient; no independence is required. The amplification loss is `o(n/(ln n)^3)`.
+
+### 13.2 Theorem 1
+
+**Verdict: BLOCKED by Proposition 9.2, not by the final arithmetic.**
+
+Once Proposition 9.2 is proved with phase-uniform errors, the all-integer conclusion follows. The theorem should then be stated first in its stronger phase-resolved form and second as a fixed-constant corollary.
+
+Recommended phase-resolved statement:
+
+\[
+ \chi(G_n)-\zeta(G_n)
+ \ge\left(\frac{(\ln2)^2}{8}
+     \{\ln2-D_4(\delta_n)\}-o(1)\right)
+   \frac{n}{(\ln n)^3}
+\]
+
+with high probability.
+
+Recommended certified fixed constant after integrating PRs #31 and #32:
+
+\[
+ \chi(G_n)-\zeta(G_n)
+ \ge\frac{(\ln2)^2}{8}\ln(1000/639)
+   \frac{n}{(\ln n)^3}
+\]
+
+with high probability.
+
+## 14. Public PR audit and integration order
+
+The open PRs are **not one linear stack**. There is an independent review layer, a Section 9 stack, and a Section 8 stack.
+
+| PR | Role | Audit status | Recommended action |
+|---|---|---|---|
+| #27 | broad research notebook and early rewrites | draft; useful provenance, too broad to merge canonically | keep as notebook; do not merge wholesale |
+| #30 | exact Section 7 rate and direct Section 9 restriction idea | green regression layer | merge/cherry-pick the Section 7 certificate; retain Section 9 note as motivation for #34--#35 |
+| #31 | factor-four constant propagation | mathematically sound conditional on compact uniform slack | integrate after adding the explicit continuity/minimum lemma |
+| #32 | stronger four-support entropy certificate | exact elementary certificate; conditional only on existing variational bridge | integrate into Lemma 5.1 after independent arithmetic review |
+| #33 | review roadmap and support scan | diagnostic/coordination only | retain; do not cite scans as proof |
+| #34 | finite matching-restriction product in Lean | green focused and full workflows | merge first in Section 9 stack |
+| #35 | attained-profile direct attachment envelope | green focused and full workflows | merge after #34 |
+| #37 | q-only intrinsic residual split | conceptually strong, focused workflow currently failing | keep draft; repair before merge or citation as kernel-checked |
+| #36 | finite endpoint transport core in Lean | green focused and full workflows | merge first in Section 8 stack |
+| #38 | endpoint AM--GM and all-high-deficit simplification | exact checker green; focused workflow failed at audited head | keep draft; PR #39 contains local Lean repairs and the audit layer |
+| #39 | this full audit, local Section 8 repairs, and reusable-results dossier | stacked on #38 | keep draft until focused Lean and audit workflow are green |
+
+### Recommended merge/integration sequence
+
+1. Merge the independent, green finite modules: #34 and #36.
+2. Merge/cherry-pick the clean independent improvements from #30, then #31 and #32 after their explicit bridges are inserted.
+3. Merge #35 on top of #34.
+4. Repair and green #37; retain only the q-only statements that pass the focused target without placeholders or hidden axioms.
+5. Green #38/#39 on top of #36.
+6. Create one new integration branch containing both the Section 8 and Section 9 stacks. Do not attempt to merge #37 directly into #38 without resolving their common-base topology.
+7. Prove the exact Section 8 physical assembly theorem.
+8. Prove the Section 9 midpoint phase adapter and instantiate the two intrinsic regimes.
+9. Derive Proposition 9.2 in one theorem with no manuscript-only assumptions.
+10. Only then replace canonical Sections 8--9 and update Theorem 1's constant.
+
+## 15. Formalization status
+
+The repository contains a substantial partial Lean development, but it does not prove `Erdos625Statement`. Green finite modules should be described exactly as finite or conditional endpoints. A successful full repository build can coexist with a failing focused target when the new module is not imported into the root aggregate; therefore focused workflow status is load-bearing for every new PR.
+
+The final formalization frontier is not “event plumbing.” It is the same mathematical boundary identified by the manuscript audit: the exact global Section 8 quotient/product and the attained-profile Section 9 asymptotic assembly.
+
+## 16. Minimal acceptance checklist for a submission-grade proof
+
+Before presenting the paper as a resolution, the following must all be true.
+
+- [ ] The exact physical high-skeleton index is defined once and used identically in Sections 8 and 9.
+- [ ] The endpoint table quotient and all symmetry factors are proved by a finite disjoint-union or bijection statement.
+- [ ] Every high-cell decoration factor is derived from the literal stub-matching ratio.
+- [ ] The product/sum interchange is justified over the dependent physical cell family.
+- [ ] Both intrinsic residual regimes are specialized uniformly to the exact midpoint profile.
+- [ ] Proposition 9.2 is proved from those two integrated statements, not asserted by prose.
+- [ ] Every `o(1)` used in the final chain is uniform in the full phase parameter.
+- [ ] The stronger entropy constant and factor-four propagation are inserted only after the compact uniform-slack lemma is explicit.
+- [ ] All focused workflows and the full Lean workflow are green at the exact submitted commit.
+- [ ] The manuscript, generated PDF, audit notes, and formalization status use consistent claims.
+
+## 17. Bottom line
+
+The project is materially stronger than the canonical manuscript suggests: the first-moment constant can be improved, the Section 7 rate can be sharpened, the Section 9 cycle walk can be eliminated, and most of the Section 8 near/middle split can be replaced by one deficit calculation. These are real advances.
+
+The remaining work is not a vague request for “more rigor.” It consists of two explicit integration theorems. Proving them would convert the present candidate solution into a substantially shorter and stronger all-phase proof. Failing to prove them would leave the second-moment proposition unsupported. The audit therefore recommends concentrating all new proof effort on these two bridges rather than adding further numerical experiments or unrelated formal lemmas.
diff --git a/625/audits/POST_INTEGRATION_STATUS_2026-07-25.md b/625/audits/POST_INTEGRATION_STATUS_2026-07-25.md
new file mode 100644
index 00000000..fdfdcac7
--- /dev/null
+++ b/625/audits/POST_INTEGRATION_STATUS_2026-07-25.md
@@ -0,0 +1,231 @@
+# Erdős 625: post-integration proof status
+
+**Date:** 25 July 2026  
+**Cumulative branch:** `agent/625-full-proof-audit-frontier`  
+**Primary review PR:** #39  
+**Purpose:** authoritative update to the time-stamped status paragraphs in
+`FULL_THEOREM_LEMMA_AUDIT_2026-07-25.md` after integrating and repairing the
+Section IX branch
+
+## 1. Branch integration completed
+
+PR #40 mechanically merged the public Section IX stack
+
+\[
+  \#34\longrightarrow\#35\longrightarrow\#37
+\]
+
+into the head branch of PR #39, which was already stacked on the Section VIII
+line
+
+\[
+  \#36\longrightarrow\#38\longrightarrow\#39.
+\]
+
+The cumulative review branch therefore contains both proof directions. The
+merge does not by itself establish Proposition 9.2; it makes the remaining
+interface visible in one tree.
+
+## 2. Corrected Section IX verdict
+
+The initial audit recorded PR #37's focused target as failing. That statement
+is now obsolete.
+
+The local Lean failures in
+`Section9QOnlyTwoRegimeAssembly.lean` were mechanical:
+
+1. `omega` was asked to discharge inequalities through nested `Nat.max`
+   expressions;
+2. a trailing `ring` was called after `field_simp` had already closed its goal;
+3. one namespace spelling was corrected.
+
+After explicit monotonicity proofs and the algebra cleanup, the focused q-only
+workflow is green at commit
+`2ea82c988218dee89d3639f598090ce813501c40`.
+
+More importantly, the repaired theorem controls the **literal attained
+attachment sum**, not an independent table law or a polymer surrogate. The
+relevant finite/asymptotic chain is now:
+
+1. `normalizedSignedProfileSecondMoment_eq_midpointCanonicalAttachmentSum`
+   identifies the normalized signed-profile second moment exactly with the
+   attained canonical attachment sum;
+2. `midpointCanonicalAttachmentSum_le_bare_mul` factors a pointwise literal
+   attachment bound from that exact sum;
+3. `exists_midpointCanonicalAttachment_qOnly_twoRegime_error` proves, under
+   the eventual phase cap and the exact profile degree cap,
+
+   \[
+     \operatorname{AttachmentSum}_n
+     \le
+     \operatorname{BareSkeletonSum}_n
+     \exp\!\left\{\varepsilon_n\frac{n}{(\ln n)^4}\right\},
+     \qquad \varepsilon_n\to0.
+   \]
+
+For the four-size midpoint profile, the hypotheses are the intended structural
+ones: the largest block size is at most the phase integer and every profile
+margin is at most that largest size.
+
+**Current Section IX classification:** **GREEN conditional only on the Section
+VIII bare-skeleton estimate.** It is no longer an independent analytic
+bottleneck.
+
+## 3. Current Section VIII verdict
+
+The repository already has kernel-checked finite components for:
+
+- the exact signed-overlap/canonical-demand decomposition;
+- the labelled-witness incidence and unlabelled-skeleton fibre quotient;
+- the endpoint block-pairing factorial identity;
+- the denominator-free squared endpoint transportation inequality;
+- the square-free AM--GM linearization;
+- the exact all-high deficit arithmetic;
+- the literal one-cell high-deficit weight bound;
+- the optional-deficit product for one fixed physical endpoint block pairing.
+
+The note `SECTION8_GLOBAL_DECORATION_BRIDGE.md` now states the paper-level
+assembly without a false unique-completion claim. A partial physical stub
+matching generally has many full completions. The exact finite decomposition
+is instead by
+
+\[
+  (\text{endpoint block pairing},\ \text{deficit vector},\
+    \text{per-cell partial stub matchings}).
+\]
+
+After summing the partial stub-matching fibres, the aggregate bare weight for a
+fixed block pairing \(P\) and multiplicity vector \(j\) is
+
+\[
+ w(P,j)
+ =
+ \frac{\prod_{e\in P}(s_e)_{j_e}(t_e)_{j_e}}
+      {(n)_J\prod_{e\in P}j_e!}
+ \prod_{e\in P}g(j_e).
+\]
+
+Its comparison with the aggregate full-containment reference weight on the
+same block support is
+
+\[
+  \frac{w(P,m-h)}{w_{\mathrm{full}}(P)}
+  \le
+  \prod_{e\in P}n^{h_e}R_{m_e,d_e}(h_e),
+\]
+
+where the single global denominator ratio is
+
+\[
+  \frac{(n)_{J+H}}{(n)_J}=(n-J)_H\le n^H.
+\]
+
+There is no asserted bijection between one partial physical matching and one
+full physical matching. Summing the geometric deficit charges over each
+block-pairing fibre and then applying endpoint transportation yields
+
+\[
+  \operatorname{BareSkeletonSum}_n
+  \le
+  \exp\!\left\{
+    O(n^{2/3}(\ln n)^{4/3})+O(\sqrt{n\ln n})
+  \right\}
+  =
+  \exp\!\left\{o\!\left(\frac n{(\ln n)^4}\right)\right\}.
+\]
+
+The exact local aggregate ratio, the global falling-factorial identity, the
+product comparison, and the geometric fibre sum are regression-tested in
+`full_proof_audit_regression.py`.
+
+### Remaining formal theorem
+
+The main unresolved Lean obligation is one global Section VIII theorem, with
+four explicit subinterfaces:
+
+1. identify every attained canonical high physical skeleton uniquely as an
+   endpoint block pairing, an allowed deficit per selected cell, and a
+   per-cell partial stub matching;
+2. sum the partial physical fibres and prove the global aggregate weight
+   comparison, including the single denominator ratio above;
+3. identify the aggregate full-reference block-pairing sum with the exact
+   endpoint table sum `sum_L fourEndpointW(L)` using the existing fibre
+   cardinality theorem;
+4. combine the endpoint AM--GM/multinomial sum and the all-deficit fibre sum at
+   the attained four-size midpoint profile.
+
+The current generic Lean product theorem incurs one extra factor of order
+`ln n` in the exponent, giving
+
+\[
+  O(n^{2/3}(\ln n)^{7/3})
+\]
+
+rather than the sharper paper-level
+`O(n^{2/3}(\ln n)^{4/3})`. Both are
+`o(n/(ln n)^4)`. Thus the weaker formal endpoint is sufficient for
+Proposition 9.2; a geometric-series lemma is needed only to match the sharper
+exponent in the paper.
+
+## 4. Current theorem status
+
+The theorem-level status is now:
+
+| Layer | Status |
+|---|---|
+| Sections 2--7: locations, entropy, exact overlap algebra, partial diagonals | logically coherent; finite improvements available |
+| Section 8 bare-skeleton estimate | corrected paper-level aggregate bridge written; global Lean assembly pending |
+| Section 9 literal attained attachment estimate | repaired and focused-CI green on its source branch |
+| Proposition 9.2 | follows once the Section 8 bare-skeleton theorem is instantiated and composed with the existing exact Section 9 identity |
+| Lemmas 10.1--10.2 and final event intersection | logically coherent conditional on Proposition 9.2 |
+| `Erdos625Statement` | not yet kernel-proved |
+
+The proof effort should therefore be concentrated on the single global
+Section VIII assembly theorem. Additional cycle decompositions, residual
+surrogates, or support scans do not address the current bottleneck.
+
+## 5. Stronger paper once Section VIII is closed
+
+The cumulative audit supports the following upgraded main-paper package:
+
+1. a phase-resolved gap coefficient
+   \[
+     \frac{(\ln2)^2}{8}\bigl(\ln2-D_4(\delta_n)\bigr);
+   \]
+2. the certified uniform coefficient
+   \[
+     \frac{(\ln2)^2}{8}\ln(1000/639)
+     =0.026896409808379\ldots;
+   \]
+3. the simultaneous complement corollary
+   \[
+     \min\{\chi(G_n),\chi(\overline G_n)\}-\zeta(G_n)
+     \ge c\frac n{(\ln n)^3};
+   \]
+4. the matching-restriction theorem for weighted even subgraphs;
+5. the abstract rare-seed-to-typical-completion method;
+6. the aggregate matching-decoration transfer principle isolated in the new
+   Section VIII bridge.
+
+Items 1--3 remain conditional on completion of the normalized second moment;
+items 4--6 are reusable finite or method-level results whose exact scope is
+recorded in `TRANSFERABLE_RESULTS_AND_COROLLARIES_2026-07-25.md`.
+
+## 6. CI interpretation
+
+For this repository, a green root `Lean` workflow is not enough to certify a
+new isolated module if that module is absent from the root aggregate. The
+focused workflow attached to each proof branch is therefore load-bearing.
+
+At the time of this update:
+
+- the repaired q-only focused target has a recorded successful run on its
+  source branch;
+- the expanded exact Python audit is green under normal and optimized Python;
+- the cumulative head is rerunning the root and focused workflows after a
+  local Section VIII coercion repair.
+
+The PR must remain draft until the exact cumulative head has green focused
+Section VIII, focused Section IX, audit-regression, and root Lean checks, and it
+must remain mathematically conditional until the global Section VIII assembly
+theorem is proved.
diff --git a/625/experiments/full_proof_audit_regression.py b/625/experiments/full_proof_audit_regression.py
new file mode 100644
index 00000000..662c0766
--- /dev/null
+++ b/625/experiments/full_proof_audit_regression.py
@@ -0,0 +1,367 @@
+#!/usr/bin/env python3
+"""Exact and high-precision regression checks for the Erdős 625 full audit.
+
+This script is deliberately standard-library only. It checks finite arithmetic
+claims used by the audit and prints diagnostic asymptotic scale comparisons.
+It does not claim to formalize the remaining global Section 8
+completion/decorations equivalence.
+"""
+
+from __future__ import annotations
+
+from decimal import Decimal, getcontext
+from fractions import Fraction
+from itertools import combinations, product
+from math import comb, factorial
+
+
+def require(condition: bool, message: str) -> None:
+    if not condition:
+        raise RuntimeError(message)
+
+
+def floor_fraction(x: Fraction) -> int:
+    return x.numerator // x.denominator
+
+
+def ceil_fraction(x: Fraction) -> int:
+    return -((-x.numerator) // x.denominator)
+
+
+def falling(n: int, k: int) -> int:
+    require(0 <= k <= n, f"invalid falling factorial ({n})_{{{k}}}")
+    value = 1
+    for offset in range(k):
+        value *= n - offset
+    return value
+
+
+def check_rounding_lemma() -> int:
+    """Exhaust a rational grid for the deterministic midpoint inequality."""
+
+    checked = 0
+    denominator = 12
+    values = [Fraction(i, denominator) for i in range(-24, 61)]
+    losses = [Fraction(i, denominator) for i in range(0, 37)]
+
+    for x in values:
+        for y in values:
+            if x <= y:
+                continue
+            for loss in losses:
+                lhs = (
+                    floor_fraction(x)
+                    - ceil_fraction(loss)
+                    - ceil_fraction((x + y) / 2)
+                )
+                rhs = (x - y) / 2 - loss - 3
+                require(
+                    Fraction(lhs, 1) > rhs,
+                    f"rounding lemma failed for x={x}, y={y}, L={loss}",
+                )
+                checked += 1
+    return checked
+
+
+def check_balanced_binomial_penalty(limit: int = 600) -> int:
+    """Check 2^k / C(k,floor(k/2)) <= k+1 exactly."""
+
+    for k in range(1, limit + 1):
+        central = comb(k, k // 2)
+        require(
+            central * (k + 1) >= 2**k,
+            f"central-binomial average bound failed at k={k}",
+        )
+    return limit
+
+
+def even_edge_sets(edges: list[tuple[int, int]], vertices: list[int]) -> list[int]:
+    result: list[int] = []
+    for mask in range(1 << len(edges)):
+        parity = {v: 0 for v in vertices}
+        for index, (u, v) in enumerate(edges):
+            if (mask >> index) & 1:
+                parity[u] ^= 1
+                parity[v] ^= 1
+        if all(value == 0 for value in parity.values()):
+            result.append(mask)
+    return result
+
+
+def check_matching_restriction() -> tuple[int, int]:
+    """Exhaust small complete bipartite graphs and matching restrictions."""
+
+    instances = 0
+    even_sets_checked = 0
+    for left_size, right_size in ((2, 2), (2, 3), (3, 3)):
+        left = list(range(left_size))
+        right = list(range(left_size, left_size + right_size))
+        vertices = left + right
+        edges = [(u, v) for u in left for v in right]
+        even_sets = even_edge_sets(edges, vertices)
+        edge_index = {edge: i for i, edge in enumerate(edges)}
+
+        matchings: list[tuple[tuple[int, int], ...]] = [tuple()]
+        for size in range(1, min(left_size, right_size) + 1):
+            for chosen in combinations(edges, size):
+                used_left = {u for u, _ in chosen}
+                used_right = {v for _, v in chosen}
+                if len(used_left) == size and len(used_right) == size:
+                    matchings.append(chosen)
+
+        for matching in matchings:
+            matching_mask = 0
+            for edge in matching:
+                matching_mask |= 1 << edge_index[edge]
+
+            images: dict[int, int] = {}
+            for mask in even_sets:
+                residual = mask & ~matching_mask
+                require(
+                    residual not in images,
+                    (
+                        "matching restriction is not injective: "
+                        f"K_{{{left_size},{right_size}}}, M={matching}"
+                    ),
+                )
+                images[residual] = mask
+                even_sets_checked += 1
+
+            # One exact weighted inequality with rational edge activities.
+            weights = [Fraction(i + 1, i + 3) for i in range(len(edges))]
+            lhs = Fraction(0, 1)
+            for mask in even_sets:
+                term = Fraction(1, 1)
+                residual = mask & ~matching_mask
+                for index, weight in enumerate(weights):
+                    if (residual >> index) & 1:
+                        term *= weight
+                lhs += term
+
+            rhs = Fraction(1, 1)
+            for index, weight in enumerate(weights):
+                if not ((matching_mask >> index) & 1):
+                    rhs *= 1 + weight
+            require(lhs <= rhs, "weighted matching-restriction product bound failed")
+            instances += 1
+
+    return instances, even_sets_checked
+
+
+def check_two_thirds_budget(max_m: int = 800) -> int:
+    checked = 0
+    for m in range(1, max_m + 1):
+        for h in range(1, m + 1):
+            if 2 * h >= m:
+                continue
+            lhs = h * ((2 * m) // 3)
+            rhs = h * m - (h * (h + 1)) // 2
+            require(lhs <= rhs, f"two-thirds exponent budget failed at m={m}, h={h}")
+            checked += 1
+    return checked
+
+
+def local_high_deficit_ratio(m: int, d: int, h: int) -> Fraction:
+    """Formula R_{m,d}(h) from the global decoration bridge."""
+
+    denominator = 1
+    for t in range(1, h + 1):
+        denominator *= d + t
+    binary_exponent = h * m - h * (h + 1) // 2
+    return Fraction(comb(m, h), denominator * 2**binary_exponent)
+
+
+def check_local_high_deficit_ratio(max_m: int = 80) -> int:
+    """Verify the exact local falling-factorial/reward ratio."""
+
+    checked = 0
+    for m in range(3, max_m + 1):
+        for d in range(4):
+            for h in range((m - 1) // 2 + 1):
+                j = m - h
+                decorated_local = Fraction(
+                    falling(m, j) * falling(m + d, j), factorial(j)
+                ) * Fraction(2 ** comb(j, 2), 2)
+                full_local = Fraction(
+                    falling(m, m) * falling(m + d, m), factorial(m)
+                ) * Fraction(2 ** comb(m, 2), 2)
+                exact_ratio = decorated_local / full_local
+                formula = local_high_deficit_ratio(m, d, h)
+                require(
+                    exact_ratio == formula,
+                    f"local ratio failed at m={m}, d={d}, h={h}",
+                )
+                checked += 1
+    return checked
+
+
+def check_global_falling_ratio(max_n: int = 100) -> int:
+    """Verify (n)_{J+H}/(n)_J=(n-J)_H<=n^H exactly."""
+
+    checked = 0
+    for n in range(max_n + 1):
+        for j in range(n + 1):
+            for h in range(n - j + 1):
+                ratio = Fraction(falling(n, j + h), falling(n, j))
+                require(
+                    ratio == falling(n - j, h),
+                    f"falling ratio identity failed at n={n}, J={j}, H={h}",
+                )
+                require(
+                    ratio <= n**h,
+                    f"falling ratio bound failed at n={n}, J={j}, H={h}",
+                )
+                checked += 1
+    return checked
+
+
+def check_global_decoration_product() -> int:
+    """Exhaust small matching fibres for the global product comparison."""
+
+    options = [
+        (m, d, h)
+        for m in range(3, 9)
+        for d in range(4)
+        for h in range((m - 1) // 2 + 1)
+    ]
+    checked = 0
+    for cell_count in (1, 2, 3):
+        for cells in product(options, repeat=cell_count):
+            j_total = sum(m - h for m, _d, h in cells)
+            full_total = sum(m for m, _d, _h in cells)
+            n = full_total + 3
+            h_total = full_total - j_total
+
+            denominator_ratio = Fraction(
+                falling(n, full_total), falling(n, j_total)
+            )
+            local_ratio = Fraction(1, 1)
+            charged_product = Fraction(1, 1)
+            for m, d, h in cells:
+                ratio = local_high_deficit_ratio(m, d, h)
+                local_ratio *= ratio
+                charged_product *= n**h * ratio
+
+            exact_global_ratio = denominator_ratio * local_ratio
+            require(
+                denominator_ratio == falling(n - j_total, h_total),
+                f"global denominator identity failed for cells={cells}",
+            )
+            require(
+                exact_global_ratio <= charged_product,
+                f"global decoration product bound failed for cells={cells}",
+            )
+            checked += 1
+    return checked
+
+
+def check_geometric_decoration_sum() -> int:
+    """Check finite deficit fibres against rho/(1-rho) and 2rho."""
+
+    checked = 0
+    for denominator in range(2, 31):
+        for numerator in range(1, denominator // 2 + 1):
+            rho = Fraction(numerator, denominator)
+            for max_h in range(1, 31):
+                finite_sum = sum((rho**h for h in range(1, max_h + 1)), Fraction())
+                require(finite_sum <= rho / (1 - rho), "geometric majorant failed")
+                require(finite_sum <= 2 * rho, "two-rho geometric bound failed")
+                checked += 1
+    return checked
+
+
+def coefficient_ledger() -> dict[str, Decimal]:
+    getcontext().prec = 80
+    q = Decimal(2).ln()
+    current = q * q * (Decimal(200) / Decimal(153)).ln() / Decimal(32)
+    propagated = q * q * (Decimal(200) / Decimal(153)).ln() / Decimal(8)
+    entropy_only = q * q * (Decimal(1000) / Decimal(639)).ln() / Decimal(32)
+    combined = q * q * (Decimal(1000) / Decimal(639)).ln() / Decimal(8)
+
+    require(propagated == current * 4, "factor-four coefficient identity failed")
+    require(combined == entropy_only * 4, "combined factor-four identity failed")
+    require(combined > propagated > entropy_only > current > 0, "coefficient ordering failed")
+
+    return {
+        "canonical": current,
+        "factor_four": propagated,
+        "entropy_only": entropy_only,
+        "combined": combined,
+        "combined_over_canonical": combined / current,
+    }
+
+
+def asymptotic_diagnostics() -> list[tuple[int, Decimal, Decimal, Decimal]]:
+    """Evaluate logarithms of three subcritical exponent ratios.
+
+    sharp all-high ratio prototype:
+      n^(2/3) N^(4/3) / (n/N^4) = exp(-N/3) N^(16/3).
+
+    current formal all-high ratio prototype (one extra factor N):
+      n^(2/3) N^(7/3) / (n/N^4) = exp(-N/3) N^(19/3).
+
+    intrinsic-small-power prototype after the midpoint log correction:
+      exp(-N/3) N^(13/3).
+
+    These values are diagnostics for the stated scale comparisons, not proofs
+    of the profile asymptotics that produce the prototypes.
+    """
+
+    getcontext().prec = 80
+    rows: list[tuple[int, Decimal, Decimal, Decimal]] = []
+    previous_sharp: Decimal | None = None
+    previous_formal: Decimal | None = None
+    previous_small: Decimal | None = None
+    for nlog in (120, 240, 480, 960, 1920):
+        x = Decimal(nlog)
+        log_sharp = -x / 3 + (Decimal(16) / 3) * x.ln()
+        log_formal = -x / 3 + (Decimal(19) / 3) * x.ln()
+        log_small = -x / 3 + (Decimal(13) / 3) * x.ln()
+        if previous_sharp is not None:
+            require(log_sharp < previous_sharp, "sharp all-high ratio is not decreasing")
+            require(log_formal < previous_formal, "formal all-high ratio is not decreasing")
+            require(log_small < previous_small, "small-power ratio is not decreasing")
+        previous_sharp = log_sharp
+        previous_formal = log_formal
+        previous_small = log_small
+        rows.append((nlog, log_sharp, log_formal, log_small))
+
+    require(rows[-1][1] < -100, "sharp all-high diagnostic is not strongly subcritical")
+    require(rows[-1][2] < -100, "formal all-high diagnostic is not strongly subcritical")
+    require(rows[-1][3] < -100, "small-power diagnostic is not strongly subcritical")
+    return rows
+
+
+def main() -> None:
+    rounding_cases = check_rounding_lemma()
+    binomial_cases = check_balanced_binomial_penalty()
+    matching_instances, even_sets = check_matching_restriction()
+    budget_cases = check_two_thirds_budget()
+    local_ratio_cases = check_local_high_deficit_ratio()
+    falling_ratio_cases = check_global_falling_ratio()
+    decoration_product_cases = check_global_decoration_product()
+    geometric_cases = check_geometric_decoration_sum()
+    coefficients = coefficient_ledger()
+    diagnostics = asymptotic_diagnostics()
+
+    print("ERDOS 625 FULL PROOF AUDIT REGRESSION: PASS")
+    print(f"  midpoint rounding cases: {rounding_cases}")
+    print(f"  balanced central-binomial cases: {binomial_cases}")
+    print(f"  matching-restriction instances: {matching_instances}")
+    print(f"  even edge sets inspected: {even_sets}")
+    print(f"  two-thirds exponent cases: {budget_cases}")
+    print(f"  exact local high-deficit ratios: {local_ratio_cases}")
+    print(f"  global falling-factorial ratios: {falling_ratio_cases}")
+    print(f"  global decoration product cases: {decoration_product_cases}")
+    print(f"  geometric decoration sums: {geometric_cases}")
+    print("  coefficient ledger:")
+    for name, value in coefficients.items():
+        print(f"    {name}: {value}")
+    print("  asymptotic diagnostic log-ratios (N, sharp all-high, formal all-high, small-power):")
+    for nlog, sharp, formal, small_power in diagnostics:
+        print(f"    {nlog}: {sharp}, {formal}, {small_power}")
+    print("  scope: exact finite arithmetic/regression; the global Section 8 equivalence remains a Lean obligation")
+
+
+if __name__ == "__main__":
+    main()
diff --git a/625/formalization/Erdos625/FiniteRestrictionProduct.lean b/625/formalization/Erdos625/FiniteRestrictionProduct.lean
new file mode 100644
index 00000000..30718bd0
--- /dev/null
+++ b/625/formalization/Erdos625/FiniteRestrictionProduct.lean
@@ -0,0 +1,59 @@
+import Mathlib.Data.ENNReal.BigOperators
+import Mathlib.Tactic
+
+/-!
+# A generic finite restriction-product inequality
+
+Suppose a finite family of finite subsets is uniquely determined by deleting a
+fixed set of coordinates.  For nonnegative multiplicative weights, its total
+restricted weight is then bounded by the full subset product on the remaining
+coordinates.
+
+The Section IX matching-restriction estimate is one instance.  The statement
+itself does not mention graphs, parity, or matchings.
+-/
+
+namespace Erdos625
+
+open scoped BigOperators ENNReal
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- If deletion of `frozen` is injective on `family`, the weighted family sum
+is bounded by the full subset product outside `frozen`. -/
+theorem weighted_finsetFamily_sdiff_le_subsetProduct
+    {E : Type*} [Fintype E] [DecidableEq E]
+    (family : Finset (Finset E))
+    (frozen : Finset E)
+    (q : E → ENNReal)
+    (hinj : ∀ F ∈ family, ∀ G ∈ family,
+      F \ frozen = G \ frozen → F = G) :
+    (∑ F ∈ family, ∏ e ∈ F \ frozen, q e) ≤
+      ∏ e ∈ (Finset.univ : Finset E) \ frozen, (1 + q e) := by
+  classical
+  calc
+    (∑ F ∈ family, ∏ e ∈ F \ frozen, q e) =
+        ∑ S ∈ Finset.image (fun F : Finset E => F \ frozen) family,
+          ∏ e ∈ S, q e := by
+      symm
+      rw [Finset.sum_image]
+      exact hinj
+    _ ≤ ∑ S ∈ Finset.powerset
+          ((Finset.univ : Finset E) \ frozen),
+          ∏ e ∈ S, q e := 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 E) \ frozen, (1 + q e) := by
+      simp +decide [Finset.prod_add, add_comm]
+
+#print axioms weighted_finsetFamily_sdiff_le_subsetProduct
+
+end
+
+end Erdos625
diff --git a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
index b5d93151..4f61b331 100644
--- a/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
+++ b/625/formalization/Erdos625/Section8AllHighDeficitCellWeight.lean
@@ -99,10 +99,12 @@ theorem nearCellTerm_le_allHighCellBase_pow
     _ ≤ ((n : ENNReal) ^ e * (m : ENNReal) ^ e) *
           ((2 : ENNReal) ^ (e * budget))⁻¹ :=
       mul_le_mul' hfirst hinv
-    _ = allHighCellBase n m ^ e := by
+    _ = ((n : ENNReal) ^ e * (m : ENNReal) ^ e) *
+          (((2 : ENNReal) ^ budget)⁻¹) ^ e := by
       have heb : e * budget = budget * e := Nat.mul_comm _ _
-      rw [heb, pow_mul, inv_pow]
-      simp [allHighCellBase, budget, div_eq_mul_inv, mul_pow, mul_assoc]
+      rw [heb, pow_mul, ENNReal.inv_pow]
+    _ = allHighCellBase n m ^ e := by
+      simp only [allHighCellBase, budget, div_eq_mul_inv, mul_pow]
 
 /-- Every allowed nonzero all-high deficit satisfies the hypothesis of the
 literal one-cell geometric bound. -/
diff --git a/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean b/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
index 80f4764e..7f726fb5 100644
--- a/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
+++ b/625/formalization/Erdos625/Section8AllHighDeficitProductBound.lean
@@ -56,7 +56,9 @@ theorem sum_nearSkeletonChoiceWeight_le_uniform_card_mul
         _ = ((allowed c).card : ENNReal) * rho := by
           simp
         _ ≤ (U : ENNReal) * rho := by
-          exact mul_le_mul_right (by exact_mod_cast hcard c) rho
+          have hcard' : ((allowed c).card : ENNReal) ≤ (U : ENNReal) := by
+            exact_mod_cast hcard c
+          simpa [mul_comm] using (mul_le_mul_right hcard' rho)
     _ = (1 + (U : ENNReal) * rho) ^ Fintype.card Cell := by
       simp
 
diff --git a/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean b/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
index d37067be..6a73f171 100644
--- a/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
+++ b/625/formalization/Erdos625/Section8EndpointAllHighDecoration.lean
@@ -114,44 +114,63 @@ theorem sum_fourEndpointAllHighChoiceWeight_le_uniform
         (fourEndpointAllHighWeight n alpha hAlpha P) choice) ≤
       (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^ P.1.edges.card := by
   classical
-  apply sum_nearSkeletonChoiceWeight_le_uniform_pow
-    (fourEndpointAllHighAllowed alpha hAlpha P)
-    (fourEndpointAllHighWeight n alpha hAlpha P)
-    (fun deficit => deficit.1) (alpha + 1) rho hrho
-  · intro cell
-    exact Finset.card_le_univ _
-  · intro cell deficit hdeficit
-    have hmem : deficit.1 ∈ Finset.Icc 1
-        (allHighDeficitCut (fourEndpointLargestSize alpha hAlpha)
-          (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1)) := by
-      simpa only [fourEndpointAllHighAllowed, Finset.mem_filter,
-        Finset.mem_univ, true_and] using hdeficit
-    exact (Finset.mem_Icc.mp hmem).1
-  · intro cell deficit hdeficit
-    let i : Fin 4 := cell.1.1.1
-    let j : Fin 4 := cell.1.2.1
-    let m := fourEndpointOverlapSize alpha hAlpha i j
-    have hmem : deficit.1 ∈ Finset.Icc 1
-        (allHighDeficitCut (fourEndpointLargestSize alpha hAlpha) m) := by
-      simpa only [fourEndpointAllHighAllowed, i, j, m,
-        Finset.mem_filter, Finset.mem_univ, true_and] using hdeficit
-    have hcut : deficit.1 ≤
-        allHighDeficitCut (fourEndpointLargestSize alpha hAlpha) m :=
-      (Finset.mem_Icc.mp hmem).2
-    have hm : m ≤ fourEndpointLargestSize alpha hAlpha :=
-      fourEndpointOverlapSize_le_largest alpha hAlpha i j
-    have hmHigh : fourEndpointLargestSize alpha hAlpha / 2 < m :=
-      fourEndpointOverlapSize_above_half_largest alpha hAlpha hHigh i j
-    have hjHigh := allHighDeficit_reconstructs_highMultiplicity
-      (fourEndpointLargestSize alpha hAlpha) m deficit.1 hmHigh hcut
-    have hhalf := highMultiplicity_deficit_twice_lt
-      (fourEndpointLargestSize alpha hAlpha) m (m - deficit.1)
-      hm hjHigh (Nat.sub_le _ _)
-    have hreconstruct : m - (m - deficit.1) = deficit.1 := by omega
-    rw [hreconstruct] at hhalf
-    have hlocal := nearCellTerm_le_allHighCellBase_pow n m
-      (Nat.dist i.val j.val) deficit.1 hhalf
-    exact hlocal.trans (ENNReal.pow_le_pow_left (hbase cell))
+  have hbound :
+      (∑ choice : NearSkeletonChoice (↥P.1.edges)
+          (FourEndpointDeficit alpha)
+          (fourEndpointAllHighAllowed alpha hAlpha P),
+        nearSkeletonChoiceWeight
+          (fourEndpointAllHighAllowed alpha hAlpha P)
+          (fourEndpointAllHighWeight n alpha hAlpha P) choice) ≤
+        (1 + ((alpha + 1 : Nat) : ENNReal) * rho) ^
+          Fintype.card (↥P.1.edges) := by
+    apply sum_nearSkeletonChoiceWeight_le_uniform_pow
+      (fourEndpointAllHighAllowed alpha hAlpha P)
+      (fourEndpointAllHighWeight n alpha hAlpha P)
+      (fun deficit => deficit.1) (alpha + 1) rho hrho
+    · intro cell
+      have hsubset :
+          fourEndpointAllHighAllowed alpha hAlpha P cell ⊆
+            (Finset.univ : Finset (FourEndpointDeficit alpha)) := by
+        intro deficit _
+        exact Finset.mem_univ deficit
+      calc
+        (fourEndpointAllHighAllowed alpha hAlpha P cell).card ≤
+            (Finset.univ : Finset (FourEndpointDeficit alpha)).card :=
+          Finset.card_le_card hsubset
+        _ = alpha + 1 := by simp [FourEndpointDeficit]
+    · intro cell deficit hdeficit
+      have hmem : deficit.1 ∈ Finset.Icc 1
+          (allHighDeficitCut (fourEndpointLargestSize alpha hAlpha)
+            (fourEndpointOverlapSize alpha hAlpha cell.1.1.1 cell.1.2.1)) := by
+        simpa only [fourEndpointAllHighAllowed, Finset.mem_filter,
+          Finset.mem_univ, true_and] using hdeficit
+      exact (Finset.mem_Icc.mp hmem).1
+    · intro cell deficit hdeficit
+      let i : Fin 4 := cell.1.1.1
+      let j : Fin 4 := cell.1.2.1
+      let m := fourEndpointOverlapSize alpha hAlpha i j
+      have hmem : deficit.1 ∈ Finset.Icc 1
+          (allHighDeficitCut (fourEndpointLargestSize alpha hAlpha) m) := by
+        simpa only [fourEndpointAllHighAllowed, i, j, m,
+          Finset.mem_filter, Finset.mem_univ, true_and] using hdeficit
+      have hcut : deficit.1 ≤
+          allHighDeficitCut (fourEndpointLargestSize alpha hAlpha) m :=
+        (Finset.mem_Icc.mp hmem).2
+      have hm : m ≤ fourEndpointLargestSize alpha hAlpha :=
+        fourEndpointOverlapSize_le_largest alpha hAlpha i j
+      have hmHigh : fourEndpointLargestSize alpha hAlpha / 2 < m :=
+        fourEndpointOverlapSize_above_half_largest alpha hAlpha hHigh i j
+      have hjHigh := allHighDeficit_reconstructs_highMultiplicity
+        (fourEndpointLargestSize alpha hAlpha) m deficit.1 hmHigh hcut
+      have hhalf := highMultiplicity_deficit_twice_lt
+        (fourEndpointLargestSize alpha hAlpha) m (m - deficit.1)
+        hm hjHigh (Nat.sub_le _ _)
+      have hreconstruct : m - (m - deficit.1) = deficit.1 := by omega
+      rw [hreconstruct] at hhalf
+      have hlocal := nearCellTerm_le_allHighCellBase_pow n m
+        (Nat.dist i.val j.val) deficit.1 hhalf
+      exact hlocal.trans (ENNReal.pow_le_pow_left (hbase cell))
+  simpa using hbound
 
 /-- Explicit common base: the sum of the sixteen endpoint-type bases. -/
 def fourEndpointAllHighRho
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..801fbab6
--- /dev/null
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionProduct.lean
@@ -0,0 +1,123 @@
+import Erdos625.Section9FixedFEvenAggregation
+import Erdos625.EvenMatchingRestriction
+import Erdos625.FiniteRestrictionProduct
+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`.  The generic finite restriction-product theorem
+then gives the required subset-product bound without a cycle/polymer
+decomposition.
+
+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
+the final random-graph statement.
+-/
+
+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
+  exact weighted_finsetFamily_sdiff_le_subsetProduct
+    (bipartiteEvenEdgeSets A B) M (fun e => q e.1 e.2)
+    (sdiff_matching_injective_on_bipartiteEvenEdgeSets M hM)
+
+/-- 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/Section9QOnlySecondMomentFrontier.lean b/625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean
new file mode 100644
index 00000000..803c9494
--- /dev/null
+++ b/625/formalization/Erdos625/Section9QOnlySecondMomentFrontier.lean
@@ -0,0 +1,86 @@
+import Erdos625.Section9QOnlyTwoRegimeAssembly
+import Erdos625.Section9MidpointSecondMomentSeed
+import Mathlib.Tactic
+
+/-!
+# Section IX: q-only normalized-second-moment frontier
+
+The repaired q-only route bounds the literal attained attachment sum by the
+Section VIII bare-skeleton sum times a vanishing exponential factor.  This
+module composes that theorem with the exact normalized-second-moment identity.
+
+Consequently the only analytic premise left visible here is a vanishing-scale
+bound on `canonicalBareSkeletonSum`.  No polymer surrogate, independent demand
+law, or additional residual adapter is introduced.
+-/
+
+namespace Erdos625
+
+open Filter
+open scoped ENNReal Topology
+
+noncomputable section
+
+set_option autoImplicit false
+
+/-- A Section VIII bare-skeleton estimate and the q-only literal attachment
+bound give the requested normalized signed-profile second-moment estimate.
+The resulting exponent coefficient is the sum of the two vanishing
+coefficients. -/
+theorem exists_normalizedSignedProfileSecondMoment_qOnly_error_of_bareSkeleton
+    (b U : Nat → Nat)
+    (k : (n : Nat) → ColoringProfile (b n))
+    (row0 : (n : Nat) → OrderedProfilePartition n (k n))
+    (epsilonSkeleton : Nat → Real)
+    (hUmin : ∀ᶠ n : Nat in atTop, 2 ≤ U n)
+    (hPhase : ∀ᶠ n : Nat in atTop, U n ≤ phaseNat n)
+    (hcap : ∀ᶠ n : Nat in atTop,
+      ∀ a : ProfileBlockIndex (k n), profileBlockMargin (k n) a ≤ U n)
+    (hSkeletonTendsto : Tendsto epsilonSkeleton atTop (nhds 0))
+    (hSkeletonNonneg : ∀ᶠ n : Nat in atTop, 0 ≤ epsilonSkeleton n)
+    (hSkeleton : ∀ᶠ n : Nat in atTop,
+      canonicalBareSkeletonSum (k n) (U n) ≤
+        ENNReal.ofReal
+          (Real.exp (epsilonSkeleton n * amplificationBase n))) :
+    ∃ epsilon : Nat → Real,
+      Tendsto epsilon atTop (nhds 0) ∧
+      (∀ᶠ n : Nat in atTop, 0 ≤ epsilon n) ∧
+      ∀ᶠ n : Nat in atTop,
+        signedProfileSecondMoment n (k n) /
+            signedProfileExpectation n (k n) ^ 2 ≤
+          ENNReal.ofReal
+            (Real.exp (epsilon n * amplificationBase n)) := by
+  obtain ⟨epsilonAttachment, hAttachmentTendsto,
+      hAttachmentNonneg, hAttachment⟩ :=
+    exists_midpointCanonicalAttachment_qOnly_twoRegime_error
+      b U k row0 hPhase hcap
+  let epsilon := fun n => epsilonSkeleton n + epsilonAttachment n
+  refine ⟨epsilon, ?_, ?_, ?_⟩
+  · simpa [epsilon] using hSkeletonTendsto.add hAttachmentTendsto
+  · filter_upwards [hSkeletonNonneg, hAttachmentNonneg] with n hs ha
+    exact add_nonneg hs ha
+  · filter_upwards [hUmin, hSkeleton, hAttachment] with n hUn hs ha
+    rw [normalizedSignedProfileSecondMoment_eq_midpointCanonicalAttachmentSum
+      (row0 n) (U n) hUn]
+    calc
+      midpointCanonicalAttachmentSum (row0 n) (U n) ≤
+          canonicalBareSkeletonSum (k n) (U n) *
+            ENNReal.ofReal
+              (Real.exp (epsilonAttachment n * amplificationBase n)) := ha
+      _ ≤ ENNReal.ofReal
+            (Real.exp (epsilonSkeleton n * amplificationBase n)) *
+          ENNReal.ofReal
+            (Real.exp (epsilonAttachment n * amplificationBase n)) := by
+        exact mul_le_mul_left hs _
+      _ = ENNReal.ofReal
+          (Real.exp (epsilon n * amplificationBase n)) := by
+        rw [← ENNReal.ofReal_mul (Real.exp_nonneg _), ← Real.exp_add]
+        congr 2
+        simp only [epsilon, add_mul]
+
+#print axioms
+  exists_normalizedSignedProfileSecondMoment_qOnly_error_of_bareSkeleton
+
+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.
diff --git a/625/proofs/RESTRICTION_PRODUCT_GENERALIZATION.md b/625/proofs/RESTRICTION_PRODUCT_GENERALIZATION.md
new file mode 100644
index 00000000..921b1a23
--- /dev/null
+++ b/625/proofs/RESTRICTION_PRODUCT_GENERALIZATION.md
@@ -0,0 +1,97 @@
+# A generic restriction-product theorem behind Section IX
+
+## 1. Finite theorem
+
+Let `E` be a finite coordinate set, let `C` be a finite family of subsets of
+`E`, and let `I subset E`. Assume that deletion of `I` is injective on `C`:
+
+\[
+  A\setminus I=B\setminus I,\quad A,B\in\mathcal C
+  \quad\Longrightarrow\quad A=B.
+\]
+
+For arbitrary nonnegative activities \((q_e)_{e\in E}\),
+
+\[
+ \boxed{
+ \sum_{A\in\mathcal C}\prod_{e\in A\setminus I}q_e
+ \le
+ \prod_{e\in E\setminus I}(1+q_e).}
+ \tag{1.1}
+\]
+
+Indeed, the restrictions `A \ I` form a subfamily of the full powerset of
+`E \ I`, with no repetitions. Summing over the larger powerset gives the
+product on the right.
+
+The theorem is kernel-checked in
+`Erdos625/FiniteRestrictionProduct.lean`. It is independent of graph parity,
+matchings, or the Erdős 625 profile.
+
+## 2. Section IX as a corollary
+
+Take `C` to be the even edge sets of the residual bipartite support and take
+`I=M`, where `M` is the exposed matching. If two even edge sets have the same
+restriction outside `M`, their symmetric difference is an even subset of a
+matching. Such a subset must be empty. Therefore deletion is injective, and
+(1.1) is exactly the matching-restriction product bound used in Section IX.
+
+This factorization is logically cleaner than a cycle/polymer enumeration: all
+model-specific work is confined to proving injectivity and bounding the total
+activities.
+
+## 3. Forest generalization
+
+The matching hypothesis is stronger than necessary. Let `T` be any forest in
+a finite graph. No nonempty edge subset of `T` is even: every nonempty forest
+has a leaf of degree one in its nontrivial edge-induced subgraph. Hence
+restriction outside `T` is injective on the graph's binary cycle space, and
+
+\[
+ \boxed{
+ \sum_{F\text{ even}}
+   \prod_{e\in F\setminus T}q_e
+ \le
+ \prod_{e\notin T}(1+q_e).}
+ \tag{3.1}
+\]
+
+For a spanning forest, this is the weighted subset-product form of the usual
+fact that cotree coordinates determine a binary cycle uniquely.
+
+The forest statement is an immediate mathematical corollary of (1.1), but its
+graph-theoretic injectivity proof has not yet been added to the Lean tree.
+
+## 4. Binary-matroid form
+
+The same statement is not intrinsically graphical. Let `C` be the cycle space
+of a binary matroid on ground set `E`, and let `I` be independent. A nonzero
+cycle vector cannot be supported inside `I`; consequently projection to
+`E \ I` is injective on `C`. Formula (1.1) gives
+
+\[
+ \sum_{x\in C}\prod_{e\in\operatorname{supp}(x)\setminus I}q_e
+ \le
+ \prod_{e\in E\setminus I}(1+q_e).
+ \tag{4.1}
+\]
+
+This is a useful abstract form for parity-constrained partition functions,
+configuration-model second moments, and high-temperature expansions. It should
+be treated as a reusable method lemma rather than claimed as a new matroid
+result without a separate literature review.
+
+## 5. Possible follow-up direction
+
+A substantive follow-up paper would need more than (1.1) alone. The promising
+program is to combine:
+
+1. injective restriction along forests or independent matroid sets;
+2. sharp activity estimates in a random combinatorial model;
+3. stability or near-equality analysis for the product bound;
+4. at least two applications where this removes a conventional polymer or
+   cycle enumeration.
+
+The Erdős 625 attachment problem supplies one application. Random regular
+partition models and parity-constrained configuration models are natural
+second targets.
diff --git a/625/proofs/SECTION8_GLOBAL_DECORATION_BRIDGE.md b/625/proofs/SECTION8_GLOBAL_DECORATION_BRIDGE.md
new file mode 100644
index 00000000..264f5b72
--- /dev/null
+++ b/625/proofs/SECTION8_GLOBAL_DECORATION_BRIDGE.md
@@ -0,0 +1,338 @@
+# Section VIII: exact global block-pairing and deficit bridge
+
+**Purpose.** This note supplies the paper-level bridge between the exact
+canonical high-skeleton sum and the shortened endpoint/all-deficit estimates.
+It also separates the mathematical statement from the remaining Lean
+implementation work.
+
+This is a finite argument. No independence between unlabelled skeletons is
+asserted. Factorization is used only after fixing a block-level matching
+support, whose selected cells have disjoint row and column endpoints.
+
+A crucial distinction is maintained throughout:
+
+- a **block pairing** records which row block is paired with which column block;
+- a **physical stub matching** records the actual matched vertices/stubs inside
+  each selected block pair.
+
+A partial physical stub matching generally has many full completions. The
+argument below does **not** choose a unique completion. Instead, it sums the
+physical stub-matching fibre exactly at each multiplicity and compares its
+aggregate weight with the aggregate full-containment weight on the same fixed
+block pairing.
+
+## 1. Setup
+
+Fix an ordered four-size profile. Its row and column block sizes lie in
+
+\[
+  \{U,U-1,U-2,U-3\},
+\]
+
+and put
+
+\[
+  R_0=\lfloor U/2\rfloor.
+\]
+
+The positive support of a canonical high skeleton is a block-level bipartite
+matching \(P\) between row and column blocks. For every selected block pair
+\(e\in P\), let
+
+\[
+  R_0<j_e\le m_e:=\min\{s_e,t_e\},
+\]
+
+where \(s_e,t_e\) are its endpoint block sizes. Write
+
+\[
+  d_e=|s_e-t_e|\in\{0,1,2,3\},\qquad
+  h_e=m_e-j_e,
+\]
+
+and
+
+\[
+  J=\sum_{e\in P}j_e,\qquad
+  J_*=\sum_{e\in P}m_e,\qquad
+  H=J_*-J=\sum_{e\in P}h_e.
+\]
+
+For a fixed block pairing \(P\) and fixed multiplicity vector \(j\), summing
+all physical stub matchings inside its selected cells gives the exact bare
+aggregate weight
+
+\[
+ w(P,j)
+ =
+ \frac{\displaystyle\prod_{e\in P}
+       (s_e)_{j_e}(t_e)_{j_e}}
+      {\displaystyle(n)_J\prod_{e\in P}j_e!}
+ \prod_{e\in P}g(j_e),
+ \tag{1.1}
+\]
+
+with \(g(x)=2^{\binom x2-1}\) for every high multiplicity in the
+present range. The factor
+
+\[
+  \frac{(s_e)_{j_e}(t_e)_{j_e}}{j_e!}
+\]
+
+is exactly the number of size-\(j_e\) physical matchings between the two
+endpoint blocks. Thus (1.1) already includes the complete physical fibre; it is
+not the weight of one arbitrarily selected stub matching.
+
+## 2. Exact finite parameterization
+
+Every physical canonical high skeleton determines, uniquely:
+
+1. its block-level matching support \(P\);
+2. its deficit vector \(h=(h_e)_{e\in P}\), with
+   \[
+     0\le h_e<m_e-R_0;
+   \]
+3. for each selected block pair \(e\), a size-\(m_e-h_e\) physical matching
+   between its endpoint stubs.
+
+Conversely, these three pieces of data reconstruct one physical canonical high
+skeleton. Hence the physical skeleton family is a disjoint union over block
+pairings and deficit choices, with a finite product of partial-stub-matching
+fibres inside each pair.
+
+After summing those inner physical fibres, the contribution of the parameter
+pair \((P,h)\) is precisely \(w(P,m-h)\) from (1.1).
+
+For comparison, define
+
+\[
+  w_{\mathrm{full}}(P):=w(P,m),
+\]
+
+where \(m=(m_e)_{e\in P}\). This is the **aggregate** weight of all
+full-containment physical stub matchings on the same block support \(P\). It is
+not obtained by assigning a unique full completion to each partial physical
+matching.
+
+The word “physical” remains essential: selected cells are distinguished first
+by their actual paired row and column blocks. Grouping block pairings by the
+sixteen endpoint types is performed only after this disjoint decomposition.
+Consequently there is no additional unlabelled multiplicity beyond the exact
+block-pairing fibre cardinality already present in the endpoint table formula.
+
+## 3. Exact one-cell aggregate ratio
+
+Assume without loss of generality that one selected block pair has endpoint
+sizes \(m\) and \(m+d\), with \(0\le d\le3\), and put \(j=m-h\). Dividing the
+aggregate local factor at multiplicity \(m-h\) by its aggregate
+full-containment value gives
+
+\[
+ \begin{aligned}
+ &\frac{(m)_{m-h}(m+d)_{m-h}}{(m-h)!}
+   \frac{m!}{(m)_m(m+d)_m}
+   \frac{g(m-h)}{g(m)} \\
+ &\qquad=
+ \frac{\binom mh}{(d+1)(d+2)\cdots(d+h)}
+  2^{-hm+h(h+1)/2}
+ =:R_{m,d}(h).
+ \end{aligned}
+ \tag{3.1}
+\]
+
+For \(h=0\), the empty product is one and \(R_{m,d}(0)=1\).
+
+The only nonlocal change is the falling-factorial denominator. Since
+\(J_*=J+H\),
+
+\[
+  \frac{(n)_{J_*}}{(n)_J}=(n-J)_H\le n^H.
+ \tag{3.2}
+\]
+
+Combining (3.1) and (3.2) yields the global aggregate comparison
+
+\[
+ \boxed{
+ \frac{w(P,m-h)}{w_{\mathrm{full}}(P)}
+ \le
+ \prod_{e\in P} n^{h_e}R_{m_e,d_e}(h_e).}
+ \tag{3.3}
+\]
+
+No product-law approximation occurs in (3.3). The local aggregate ratios
+factor because \(P\) is a block matching: each selected cell uses a distinct
+row block and a distinct column block. The single global denominator ratio is
+handled once, by (3.2).
+
+## 4. Uniform all-deficit charge
+
+The high condition gives \(2h<m\). The exact integer inequality
+
+\[
+ h\left\lfloor\frac{2m}{3}\right\rfloor
+ \le hm-\frac{h(h+1)}2
+ \tag{4.1}
+\]
+
+then implies
+
+\[
+ n^hR_{m,d}(h)
+ \le
+ \left(\frac{nm}{2^{\lfloor2m/3\rfloor}}\right)^h.
+ \tag{4.2}
+\]
+
+Let
+
+\[
+ \rho_n=
+ \max_{U-3\le m\le U}
+ \frac{nm}{2^{\lfloor2m/3\rfloor}}.
+ \tag{4.3}
+\]
+
+The phase relation \(2^U=\Theta(n^2/N^2)\), where \(N=\ln n\), gives
+
+\[
+ \rho_n=O\!\left(\frac{N^{7/3}}{n^{1/3}}\right)=o(1).
+ \tag{4.4}
+\]
+
+For all sufficiently large \(n\), \(\rho_n\le1/2\). Therefore, for each
+selected block pair,
+
+\[
+ \sum_{1\le h<m-R_0} n^hR_{m,d}(h)
+ \le\sum_{h\ge1}\rho_n^h
+ =\frac{\rho_n}{1-\rho_n}
+ \le2\rho_n.
+ \tag{4.5}
+\]
+
+This geometric estimate is the sharp interface needed for the exponent in the
+concise manuscript route. Merely bounding each term by \(\rho_n\) and
+multiplying by the number of allowed deficits introduces a harmless but
+unnecessary extra factor \(U\).
+
+## 5. Sum over one block-pairing fibre
+
+For a fixed block pairing \(P\), sum the aggregate weights (1.1) over every
+allowed deficit vector. Applying (3.3) and then (4.5),
+
+\[
+ \begin{aligned}
+ \sum_{h:\,m-h\text{ high}} w(P,m-h)
+ &\le
+ w_{\mathrm{full}}(P)
+ \prod_{e\in P}
+   \left(1+\sum_{1\le h<m_e-R_0}n^hR_{m_e,d_e}(h)\right)\\
+ &\le
+ w_{\mathrm{full}}(P)(1+2\rho_n)^{|P|}\\
+ &\le
+ w_{\mathrm{full}}(P)(1+2\rho_n)^{k_{\mathrm{co}}}.
+ \end{aligned}
+ \tag{5.1}
+\]
+
+Now sum over block pairings. Grouping them by their endpoint type table \(L\),
+the exact block-pairing factorial identity gives
+
+\[
+ \sum_{P}w_{\mathrm{full}}(P)=\sum_LW(L).
+ \tag{5.2}
+\]
+
+The square-free endpoint transportation and termwise AM--GM estimate give
+
+\[
+ \sum_LW(L)
+ \le
+ (1+C\eta_n)^{k_{\mathrm{co}}}\sum_rD(r),
+ \qquad
+ \eta_n=O\!\left(\frac{N^{3/2}}{\sqrt n}\right).
+ \tag{5.3}
+\]
+
+By the all-partial-diagonals estimate, \(\sum_rD(r)=1+o(1)\). Combining
+(5.1)--(5.3),
+
+\[
+ \begin{aligned}
+ \sum_{P}\sum_{h:\,m-h\text{ high}}w(P,m-h)
+ &\le
+ (1+2\rho_n)^{k_{\mathrm{co}}}
+ (1+C\eta_n)^{k_{\mathrm{co}}}(1+o(1)) \\
+ &\le
+ \exp\!\left\{
+ O(n^{2/3}N^{4/3})+O(\sqrt{nN})
+ \right\} \\
+ &=\exp\!\left\{o\!\left(\frac n{N^4}\right)\right\}.
+ \end{aligned}
+ \tag{5.4}
+\]
+
+The left side is the exact bare canonical high-skeleton sum because the
+parameterization in Section 2 is disjoint and (1.1) has already summed every
+partial physical stub-matching fibre.
+
+This is the Section VIII bare-skeleton estimate required by the repaired
+q-only Section IX attachment theorem.
+
+## 6. Formalization boundary
+
+The repository already contains kernel-checked finite components for:
+
+1. the exact prescribed-demand/typed-partial-matching correspondence;
+2. the exact labelled/unlabelled physical skeleton quotient;
+3. the endpoint block-pairing factorial identity;
+4. the squared endpoint transport inequality and square-free AM--GM bridge;
+5. the one-cell aggregate ratio bound (4.2);
+6. the optional-deficit product for a fixed endpoint block pairing.
+
+The remaining Lean work is to package one global finite reindexing and one
+aggregate weight comparison:
+
+- the equivalence between canonical high physical skeletons and triples
+  `(endpoint block pairing, allowed deficit choice, per-cell partial stub
+  matching)`;
+- the summation of the per-cell physical fibres to (1.1), followed by the
+  global comparison (3.3), including the single denominator ratio (3.2);
+- the identification of the full-reference block-pairing sum with
+  `sum_L fourEndpointW(L)`.
+
+There is deliberately no claimed equivalence between a partial physical
+matching and a unique full physical matching.
+
+The current generic Lean product endpoint bounds the sum by a factor of the
+form
+
+\[
+  \bigl(1+(\alpha+1)\rho_n\bigr)^{|P|},
+\]
+
+which gives the weaker exponent \(O(n^{2/3}N^{7/3})\). This is still
+\(o(n/N^4)\), so it is sufficient for Proposition 9.2. To match the sharper
+paper exponent in (5.4), add the finite geometric-series lemma (4.5) and use
+the fact that each positive deficit exponent occurs at most once in one
+cell's allowed set.
+
+## 7. Reusable abstract form
+
+The proof above is an instance of an aggregate matching-decoration transfer
+principle.
+
+> **Aggregate matching-decoration transfer.** Suppose objects decompose
+> disjointly by a block matching \(P\), one deficit \(h_e\) per selected cell,
+> and a finite local physical fibre. After summing each local physical fibre,
+> assume the aggregate deficit-\(h\) weight is at most \(\rho^h\) times the
+> corresponding aggregate full-cell reference weight, with one global
+> denominator loss distributed across the deficits. If \(|P|\le k\) and
+> \(\rho\le1/2\), then the total decorated weight is at most
+> \((1+2\rho)^k\) times the total aggregate reference weight.
+
+This formulation requires no unique completion map. It is potentially
+reusable in configuration-model and random-partition second moments whenever
+exceptional cells form a matching and their aggregate local deficits have a
+geometric charge.
diff --git a/625/proofs/TRANSFERABLE_RESULTS_AND_COROLLARIES_2026-07-25.md b/625/proofs/TRANSFERABLE_RESULTS_AND_COROLLARIES_2026-07-25.md
new file mode 100644
index 00000000..4dc09489
--- /dev/null
+++ b/625/proofs/TRANSFERABLE_RESULTS_AND_COROLLARIES_2026-07-25.md
@@ -0,0 +1,369 @@
+# Erdős 625: transferable results, stronger corollaries, and follow-up paper directions
+
+**Date:** 25 July 2026  
+**Purpose:** separate results that can strengthen the Erdős 625 manuscript from methods that may support independent papers  
+**Status convention:** every item is labelled as an immediate conditional corollary, a finite theorem already checked in the repository, or a research direction requiring new work
+
+## 1. Literature position after the public search
+
+The public literature located in this audit contains the following closest results.
+
+- Annika Heckel, *The difference between the chromatic and the cochromatic number of a random graph*, arXiv:2409.17614, proves a positive answer for roughly 95% of integers `n`.
+- Annika Heckel, *On a question of Erdős and Gimbel on the cochromatic number*, Electronic Journal of Combinatorics 31(4), P4.72 (2024), proves that a high-probability upper bound on the gap cannot stay below `n^(1/2-o(1))` along all large `n`.
+- Raphael Steiner, *On the Difference Between the Chromatic and Cochromatic Number*, SIAM Journal on Discrete Mathematics 39(4), 2268--2274 (2025), gives independent positive evidence and resolves related cochromatic questions.
+- Heckel--Panagiotou, *Colouring random graphs: Tame colourings*, arXiv:2306.07253, develops the delicate second-moment technology used in the admissible-phase coloring literature.
+- Gimbel--Kündgen--Molloy, *Fractional cocoloring of graphs*, arXiv:1906.05504, studies the fractional analogue but does not supply the all-phase random-graph result sought here.
+- The Erdős Problems page for #625 still lists the problem as open and records Heckel's roughly-95% result. Its discussion thread also records a different two-independent-random-graphs coupling direction; that direction should be credited to the people named there if pursued.
+
+The search found no public paper dated through 25 July 2026 that claims the same full-sequence `Omega(n/(log n)^3)` high-probability lower bound. This is a search result, not a guarantee that no unpublished or unindexed work exists.
+
+## 2. Results that should strengthen the main Erdős 625 paper
+
+### 2.1 Phase-resolved gap theorem
+
+**Status: immediate conditional corollary of the canonical root formula, Proposition 9.2, and Lemma 10.2.**
+
+Let
+
+\[
+ A_4(\delta)=\ln2-D_4(\delta).
+\]
+
+Equation (5.11), midpoint placement, integer rounding, and the `o(n/(ln n)^3)` amplification loss give
+
+\[
+ \boxed{
+ \chi(G_n)-\zeta(G_n)
+ \ge\left(\frac{(\ln2)^2}{8}A_4(\delta_n)-o(1)\right)
+       \frac{n}{(\ln n)^3}}
+\]
+
+with high probability, once the normalized second moment is established.
+
+This statement is stronger and more informative than a single uniform constant. It displays the residual phase oscillation instead of discarding it. A fixed-constant theorem should be presented as its corollary.
+
+**Required manuscript bridge:** state continuity of `D_4` and uniformity of the error in (5.11) explicitly.
+
+### 2.2 Stronger certified uniform constant
+
+**Status: immediate conditional corollary after integrating PRs #31 and #32.**
+
+PR #32 certifies
+
+\[
+ A_4(\delta)>\ln(1000/639)
+\]
+
+uniformly. PR #31 shows that the final fixed coefficient is divided by `8`, not `32`. Hence
+
+\[
+ \boxed{
+ \chi(G_n)-\zeta(G_n)
+ \ge \frac{(\ln2)^2}{8}\ln(1000/639)
+      \frac{n}{(\ln n)^3}}
+\]
+
+with high probability, conditional on the completed second-moment chain.
+
+The numerical coefficient is
+
+\[
+ 0.026896409808379\ldots,
+\]
+
+about `6.687` times the coefficient currently printed in the canonical manuscript.
+
+### 2.3 Simultaneous complement-symmetric corollary
+
+**Status: immediate conditional corollary; no new second moment.**
+
+Cochromatic number is complement-invariant:
+
+\[
+ \zeta(\overline G)=\zeta(G).
+\]
+
+Moreover, if `G_n~G(n,1/2)`, then `\overline G_n` has the same distribution. Apply the completed theorem once to `G_n` and once to `\overline G_n`, and take a union bound. For every certified coefficient `c` from the main theorem,
+
+\[
+ \boxed{
+ \min\{\chi(G_n),\chi(\overline G_n)\}-\zeta(G_n)
+ \ge c\frac{n}{(\ln n)^3}}
+\]
+
+with high probability.
+
+This says that a mixed clique/independent partition beats both pure orientations simultaneously by polynomial scale. It is a clean structural corollary worth stating in the introduction.
+
+### 2.4 Balanced-sign midpoint seed
+
+**Status: rigorous conditional seed corollary; the high-probability structural upgrade needs a modified amplifier.**
+
+Let `k=k_co`, and restrict the signed witness count to assignments having exactly
+
+\[
+ b=\lfloor k/2\rfloor
+\]
+
+clique declarations. Denote the restricted count by `Z_bal`. For each underlying partition,
+
+\[
+ \mathbb E Z_{\mathrm{bal}}
+ =\frac{\binom{k}{b}}{2^k}\mathbb E Z_{\mathrm{sgn}}.
+\]
+
+Since the largest binomial coefficient is at least the average coefficient,
+
+\[
+ \binom{k}{\lfloor k/2\rfloor}\ge\frac{2^k}{k+1}.
+\]
+
+Thus the first-moment logarithm loses at most `ln(k+1)`, negligible compared with the `Theta(k)` midpoint margin.
+
+Pointwise `Z_bal<=Z_sgn`, so
+
+\[
+ \frac{\mathbb E Z_{\mathrm{bal}}^2}
+      {(\mathbb E Z_{\mathrm{bal}})^2}
+ \le (k+1)^2
+ \frac{\mathbb E Z_{\mathrm{sgn}}^2}
+      {(\mathbb E Z_{\mathrm{sgn}})^2}.
+\]
+
+Consequently Proposition 9.2 would give the balanced seed
+
+\[
+ \Pr\{Z_{\mathrm{bal}}>0\}
+ \ge\exp\{-\Lambda_n-O(\ln k)\}.
+\]
+
+This is already a nontrivial structural result: the rare witness can be required to use asymptotically equal numbers of clique and independent classes.
+
+**High-probability upgrade.** A direct application of Lemma 10.2 forgets the balance information. To preserve it, introduce `k` labelled signed slots and the two-Lipschitz score
+
+\[
+ T=\max\{|W|+\#\text{nonempty slots}\},
+\]
+
+with exactly `b` clique-labelled slots. Deleting the altered vertex changes this score by at most two. The seed event has score `n+k`; bounded differences then shows that both the uncovered vertex count and the empty-slot count are `o(k)`. Coloring the leftover with independent classes produces, with high probability, a near-optimal cocoloring with
+
+\[
+ \#\text{clique parts}=(1/2+o(1))k,
+ \qquad
+ \#\text{independent parts}=(1/2+o(1))k.
+\]
+
+This modified amplifier should be written and audited before the structural statement is promoted to a theorem.
+
+### 2.5 Explicit upper-tail family for the cocoloring location
+
+**Status: already contained in Lemma 10.2; should be highlighted.**
+
+For any deterministic `r>0`, the seed exponent `Lambda_n` gives
+
+\[
+ \Pr\!\left(
+ \zeta(G_n)>k_n+C\left(
+ \frac{\sqrt{n\Lambda_n}+\sqrt{nr}}{\ln n}
+ +n^{1/3}+1\right)\right)
+ \le e^{-r}+o(1).
+\]
+
+This is stronger than the one chosen specialization in the final proof. It gives a tunable tail family and can be quoted independently in later work on random partition parameters.
+
+## 3. Finite results suitable for reuse outside Erdős 625
+
+### 3.1 Matching-restriction inequality for weighted even subgraphs
+
+**Status: finite theorem; kernel-checked in PR #34.**
+
+Let `H=(V,E)` be a finite graph, let `M` be a matching, and let `E_even` be the family of even edge sets. Restriction
+
+\[
+ \rho_M:F\mapsto F\setminus M
+\]
+
+is injective on `E_even`. Indeed, if two even sets have the same restriction, their symmetric difference is an even subset of a matching. A nonempty subset of a matching has degree one at each of its incident vertices, so it cannot be even.
+
+For arbitrary nonnegative edge weights `q_e`, injection into the full subset family gives
+
+\[
+ \boxed{
+ \sum_{F\in E_{\mathrm{even}}}
+   \prod_{e\in F\setminus M}q_e
+ \le\prod_{e\in E\setminus M}(1+q_e)
+ \le\exp\!\left(\sum_{e\in E\setminus M}q_e\right).}
+\]
+
+This removes cycle decompositions whenever a matching has already been exposed. Potential applications include configuration-model second moments, polymer expansions, parity-constrained subgraph sums, and high-temperature expansions with frozen matching edges.
+
+**Possible standalone note.** The theorem alone is short; a separate paper would require a broader family of applications or extensions, for example matroidal restrictions, `Z/qZ` flows, or sharpness/stability results.
+
+### 3.2 Exact cycle-space factor for two signed partitions
+
+**Status: finite theorem proved in manuscript Lemma 6.1; much of the algebra is formalized.**
+
+For two set partitions, build the bipartite support graph whose edges are overlap cells of size at least two. Compatible binary declarations are constant on connected components. The exact normalized factor is
+
+\[
+ 2^{W+c(H)-|V(H)|}
+ =\left(\prod_e g(r_e)\right)2^{\beta(H)}.
+\]
+
+The topological term is the size of the binary cycle space. This identity is a finite partition analogue of a high-temperature Ising expansion: local cell multiplicities contribute edge activities, while global sign compatibility contributes the cycle-space dimension.
+
+**Generalization direction.** Replace the two declarations by `q` templates. Compatibility would be governed by a `q`-state constraint system on the overlap support, leading to Potts/Tutte-type factors rather than a binary cycle space. This is not required for Erdős 625 but could form a separate combinatorial-statistical-mechanics project.
+
+### 3.3 All-high deficit calculus
+
+**Status: finite arithmetic largely checked in PR #38; physical global assembly still missing.**
+
+For an endpoint cell of size `m` and deficit `e` with `2e<m`, the exact local ratio has a uniform binary exponent budget
+
+\[
+ e\lfloor2m/3\rfloor
+ \le em-\frac{e(e+1)}2.
+\]
+
+This yields a geometric base independent of the individual deficit. The resulting one-product treatment replaces separate near and middle ranges.
+
+The reusable principle is:
+
+> If a high-overlap local ratio has a convex quadratic exponent and every admissible deficit lies below half the endpoint size, charge every deficit to one fixed linear fraction of the endpoint exponent and sum one geometric series.
+
+This pattern should be useful in second moments for bounded colorings and random set partitions. A standalone theorem would need an abstract hypothesis/result formulation rather than the current Erdős-625-specific type table.
+
+## 4. General method theorems that could support independent papers
+
+### 4.1 Rare-seed to typical-completion amplifier
+
+**Status: exact theorem in the manuscript for cochromatic number; abstract generalization requires writing.**
+
+The mechanism of Lemma 10.2 depends on four properties only:
+
+1. a random object is exposed in independent vertex blocks;
+2. `S_k`, the maximum size of an induced feasible subobject, is one-Lipschitz;
+3. the rare seed event is exactly `S_k=n`;
+4. an arbitrary leftover of size `s` can be completed at cost `g_n(s)` on one simultaneous high-probability event.
+
+Then
+
+\[
+ \Pr\{S_k=n\}\ge e^{-\Lambda}
+\]
+
+implies, except with probability `e^{-r}+o(1)`, a leftover of size at most
+
+\[
+ O(\sqrt{n\Lambda}+\sqrt{nr}),
+\]
+
+and hence total cost at most `k+g_n(O(sqrt(n Lambda)+sqrt(n r)))`.
+
+This abstract statement applies to many hereditary covering and partition parameters. A methods paper could develop variants with block Lipschitz constants, weighted scores, multiple resource types, and product-space measures beyond `G(n,1/2)`.
+
+### 4.2 Finite-support root-displacement theorem
+
+**Status: the required analysis is already implicit in Lemma 3.1 and Section 5; abstract formulation requires writing.**
+
+Let `S` be a fixed finite deficit support whose convex hull contains the complete phase target interval. Define the limiting support loss
+
+\[
+ D_S(\delta)=\mathcal F_{S_+}(T_0)-\mathcal F_S(T_0).
+\]
+
+If
+
+\[
+ \inf_{\delta\in[0,1]}\{\ln2-D_S(\delta)\}>0,
+\]
+
+then the signed root for support `S` satisfies
+
+\[
+ r_+-r_S^{\mathrm{co}}
+ =\left(\frac{(\ln2)^2}{4}
+   \{\ln2-D_S(\delta_n)\}+o(1)\right)
+   \frac{n}{(\ln n)^3}.
+\]
+
+Midpoint placement retains one half of this coefficient before the support-specific second moment is considered.
+
+This theorem cleanly separates two tasks:
+
+- **support design:** optimize the phase-uniform entropy advantage;
+- **admissibility:** prove a second moment for the chosen support.
+
+It provides a reusable optimization framework and explains why a numerically better support may still be a worse proof choice if it raises the transportation dimension.
+
+### 4.3 Support frontier and complexity/advantage trade-off
+
+**Status: diagnostic only.**
+
+PR #33 scans finite supports and reports that `{2,3,4,5,6}` improves the limiting minimum advantage by only about `1.017%` over `{2,3,4,5}`, while raising the dense endpoint table from `4x4` to `5x5`. This supports the four-size support as the current practical frontier.
+
+A publishable optimization result would require interval-certified global support comparisons, not grid scans. A useful theorem would characterize which fixed supports maximize the minimum advantage subject to cardinality or diameter constraints.
+
+## 5. Additional research directions
+
+### 5.1 Prove the exact phase minimum of the four-support advantage
+
+The numerical scans place the minimum of `A_4(delta)` near the phase endpoint `delta=1`. Proving monotonicity or a unique minimum would replace the conservative omitted-mass certificate by a substantially sharper exact constant and clarify the phase geometry.
+
+A possible route is to use
+
+\[
+ \frac{d}{dT}\mathcal F_S(T)=-\lambda_S(T)
+\]
+
+and compare the full- and four-support tilts with certified interval arithmetic. This remains a new analytic problem.
+
+### 5.2 Asymmetric edge density `p != 1/2`
+
+At `p=1/2`, clique and independent declarations have equal one-class weights, producing the exact `2^k` sign gain. For `p!=1/2`, declarations acquire an external field depending on class size. The overlap compatibility factor should become an inhomogeneous Ising partition function on the support graph.
+
+A systematic extension could study when a mixed partition still improves on ordinary coloring and how the optimal clique/independent proportion depends on `p`. This is a plausible separate paper, not a corollary of the present proof.
+
+### 5.3 Two-independent-graph coupling
+
+The current Erdős Problems discussion records a reduction using two independent `G(n,1/2)` graphs and a McDiarmid coupling. This approach is conceptually different from the signed-overlap proof and may yield cleaner concentration or comparison statements. It should be pursued only with explicit attribution to the collaborators named in that discussion and after obtaining the precise coupling statement from a primary source or direct communication.
+
+### 5.4 Fractional and LP relaxations
+
+The fractional cochromatic literature suggests comparing the integral random gap with the fractional cochromatic number. Possible questions include whether the signed four-size profile has an LP interpretation, whether the integral/fractional gap is smaller than `n/(ln n)^3`, and whether dual variables recover the limiting tilt calculation. No such result follows automatically from the present manuscript.
+
+## 6. Recommended paper strategy
+
+### Main Erdős 625 paper
+
+The strongest coherent version should contain:
+
+1. the full-sequence theorem;
+2. the phase-resolved coefficient;
+3. the stronger certified constant from PRs #31--#32;
+4. the simultaneous complement corollary;
+5. the matching-restriction simplification and all-high-deficit Section 8 route;
+6. the abstract rare-seed amplifier as a named method lemma.
+
+The balanced-core statement may be included if the weighted-slot amplifier is completed cleanly. Otherwise it belongs in a final “further consequences” section as a proved seed statement plus an explicit conjectural upgrade.
+
+### Best independent follow-up paper
+
+The most promising standalone direction is not another numerical support scan. It is a methods paper combining:
+
+- weighted even-subgraph restriction through an exposed matching;
+- exact signed-partition cycle-space factors;
+- a general rare-seed to typical-completion theorem;
+- applications to at least two random partition models.
+
+Without multiple applications, these ingredients are better presented as reusable propositions inside the main paper rather than split into several very short notes.
+
+## 7. Priority order
+
+1. Complete the Section 8 physical quotient/product theorem.
+2. Complete the Section 9 intrinsic two-regime phase adapter.
+3. Derive Proposition 9.2 on one integrated branch.
+4. Insert the phase-resolved theorem and improved constant.
+5. Add the simultaneous complement corollary.
+6. Write the balanced-sign seed formally; decide whether the weighted-slot amplifier is concise enough for the main paper.
+7. Only after the main theorem is closed, develop the abstract methods/general-`p` follow-up.