From 27c97b8375deb9f794d5e0774b396f6908730744 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 07:46:19 +0300
Subject: [PATCH 01/18] Add direct Section 9 attachment envelope

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

diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
new file mode 100644
index 00000000..559e23f1
--- /dev/null
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
@@ -0,0 +1,317 @@
+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
+      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 :
+          ENNReal) : EReal) ≤
+          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
+  calc
+    ((residualActualAttachmentNumerator M (U / 2) row col htotal :
+        ENNReal) : EReal) ≤
+      (((∏ a : A, ∏ b : B,
+          (1 + residualLambda M (U / 2) row col a b)) *
+        (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          (1 + residualQ M (U / 2) row col e.1 e.2)) : ENNReal) : EReal) := by
+      exact_mod_cast hbridge
+    _ ≤ EReal.exp
+        (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) +
+          kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) :=
+      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

From 74b0df099da71b3a12a9cb41287d92f556af3f2d Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 07:46:42 +0300
Subject: [PATCH 02/18] Document the direct attachment-envelope boundary

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

diff --git a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
new file mode 100644
index 00000000..e3405ecc
--- /dev/null
+++ b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
@@ -0,0 +1,91 @@
+# Audit: direct matching-restriction attachment envelope
+
+## Scope
+
+This audit accompanies `Erdos625/Section9MatchingRestrictionEnvelope.lean`.
+The branch is stacked on PR #34 and therefore assumes the finite
+matching-restriction product theorem from
+`Section9MatchingRestrictionProduct.lean`.
+
+## New checked targets
+
+The new 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).
+   \]
+
+This statement 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.
+
+## Trust gates
+
+The focused workflow:
+
+- rejects `sorry`, `admit`, `sorryAx`, project `axiom`/`constant`, and `unsafe`;
+- builds the pinned Lean 4.31/mathlib project with warnings fatal;
+- compiles the new module directly with `-DwarningAsError=true`;
+- prints the axioms of every new public theorem.
+
+The ordinary repository Lean workflow also runs because this PR changes the
+formalization tree.
+
+## Deliberate boundary
+
+This module still does not prove the complete Erdős 625 theorem. In particular
+it does not:
+
+- sum the Section VIII bare skeleton weights;
+- specialize the envelope to the midpoint profile and produce the eventual
+  `o(n/(log n)^4)` coefficient;
+- update the root aggregate or generated self-contained checkpoint;
+- prove the chromatic lower tail, rare seed, or final event intersection.
+
+The next integration step, after review, is a profile-level asymptotic adapter
+showing that the displayed exponent is `o(amplificationBase n)` uniformly over
+attained canonical demands.

From 957bba7aff9cf34c3c00c738d0ec1d751d444a5f Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 07:46:55 +0300
Subject: [PATCH 03/18] Add focused Lean gate for direct attachment envelope

---
 ...erdos625-matching-restriction-envelope.yml | 42 +++++++++++++++++++
 1 file changed, 42 insertions(+)
 create mode 100644 .github/workflows/erdos625-matching-restriction-envelope.yml

diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml
new file mode 100644
index 00000000..aadd804b
--- /dev/null
+++ b/.github/workflows/erdos625-matching-restriction-envelope.yml
@@ -0,0 +1,42 @@
+name: Erdős 625 matching-restriction envelope
+
+on:
+  pull_request:
+    paths:
+      - "625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean"
+      - "625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md"
+      - ".github/workflows/erdos625-matching-restriction-envelope.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  focused-lean-check:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
+      - name: Reject placeholders and project axioms in the new module
+        shell: bash
+        run: |
+          if grep -nE \
+            '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
+            625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean; then
+            exit 1
+          fi
+      - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
+        with:
+          lake-package-directory: 625/formalization
+          auto-config: false
+          build: true
+          build-args: --wfail
+          use-mathlib-cache: true
+          use-github-cache: false
+          nanoda: false
+      - name: Compile the module warning-fatally
+        working-directory: 625/formalization
+        shell: bash
+        run: |
+          lake env lean -DwarningAsError=true \
+            Erdos625/Section9MatchingRestrictionEnvelope.lean \
+            -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionEnvelope.olean

From 75bec86ce179a37b2bd252a0744edbe7a1637807 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:00:27 +0300
Subject: [PATCH 04/18] Expose focused Lean compiler tail

---
 .../workflows/erdos625-matching-restriction-envelope.yml   | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml
index aadd804b..f105f67e 100644
--- a/.github/workflows/erdos625-matching-restriction-envelope.yml
+++ b/.github/workflows/erdos625-matching-restriction-envelope.yml
@@ -37,6 +37,11 @@ jobs:
         working-directory: 625/formalization
         shell: bash
         run: |
+          set +e
           lake env lean -DwarningAsError=true \
             Erdos625/Section9MatchingRestrictionEnvelope.lean \
-            -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionEnvelope.olean
+            -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionEnvelope.olean \
+            > /tmp/section9-envelope-lean.log 2>&1
+          status=$?
+          tail -n 240 /tmp/section9-envelope-lean.log
+          exit $status

From 4df65ce74095b9d3276cd8d5b57ee88f5738953c Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:01:44 +0300
Subject: [PATCH 05/18] Use targeted Lean dependency closure

---
 .../workflows/erdos625-matching-restriction-envelope.yml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml
index f105f67e..dbf15d37 100644
--- a/.github/workflows/erdos625-matching-restriction-envelope.yml
+++ b/.github/workflows/erdos625-matching-restriction-envelope.yml
@@ -28,19 +28,16 @@ jobs:
         with:
           lake-package-directory: 625/formalization
           auto-config: false
-          build: true
-          build-args: --wfail
+          build: false
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Compile the module warning-fatally
+      - name: Build the module and dependency closure warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
           set +e
-          lake env lean -DwarningAsError=true \
-            Erdos625/Section9MatchingRestrictionEnvelope.lean \
-            -o .lake/build/lib/lean/Erdos625/Section9MatchingRestrictionEnvelope.olean \
+          lake build Erdos625.Section9MatchingRestrictionEnvelope --wfail \
             > /tmp/section9-envelope-lean.log 2>&1
           status=$?
           tail -n 240 /tmp/section9-envelope-lean.log

From 425fe67e91e28f5ebced2c44b7e98028fc134d7a Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:07:05 +0300
Subject: [PATCH 06/18] Upload the focused Section 9 compiler log

---
 .../workflows/erdos625-matching-restriction-envelope.yml   | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml
index dbf15d37..5869a4d4 100644
--- a/.github/workflows/erdos625-matching-restriction-envelope.yml
+++ b/.github/workflows/erdos625-matching-restriction-envelope.yml
@@ -42,3 +42,10 @@ jobs:
           status=$?
           tail -n 240 /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

From 0c5c0228a02c0978d9a2e6fde0715f011fabad2b Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:15:49 +0300
Subject: [PATCH 07/18] Repair the direct attachment-envelope transport

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

diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
index 559e23f1..8d92d8bd 100644
--- a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
@@ -53,6 +53,7 @@ theorem sum_configurationCellTheta_sq_global
     _ = ((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) *
@@ -295,10 +296,10 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope :
   calc
     ((residualActualAttachmentNumerator M (U / 2) row col htotal :
         ENNReal) : EReal) ≤
-      (((∏ a : A, ∏ b : B,
-          (1 + residualLambda M (U / 2) row col a b)) *
-        (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
-          (1 + residualQ M (U / 2) row col e.1 e.2)) : ENNReal) : EReal) := by
+      ((∏ a : A, ∏ b : B,
+          (1 + residualLambda M (U / 2) row col a b)) : EReal) *
+        ((∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+          (1 + residualQ M (U / 2) row col e.1 e.2)) : EReal) := by
       exact_mod_cast hbridge
     _ ≤ EReal.exp
         (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) +

From 32750462cc5fc8b568e0a3b97dee29c0e6f33bc1 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:24:04 +0300
Subject: [PATCH 08/18] Use the exact ENNReal-to-EReal order bridge

---
 .../Section9MatchingRestrictionEnvelope.lean  | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
index 8d92d8bd..141895a8 100644
--- a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
@@ -293,18 +293,15 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope :
       (residualQ M (U / 2) row col) M
       (kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal))
       (kappaQ * (U : ENNReal) ^ 2) hlambda hqOutside
-  calc
-    ((residualActualAttachmentNumerator M (U / 2) row col htotal :
+  have hbridgeE :
+      ((residualActualAttachmentNumerator M (U / 2) row col htotal :
         ENNReal) : EReal) ≤
-      ((∏ a : A, ∏ b : B,
-          (1 + residualLambda M (U / 2) row col a b)) : EReal) *
-        ((∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
-          (1 + residualQ M (U / 2) row col e.1 e.2)) : EReal) := by
-      exact_mod_cast hbridge
-    _ ≤ EReal.exp
-        (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) +
-          kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) :=
-      hproduct
+        (((∏ a : A, ∏ b : B,
+            (1 + residualLambda M (U / 2) row col a b)) *
+          (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
+            (1 + residualQ M (U / 2) row col e.1 e.2)) : ENNReal) : EReal) :=
+    EReal.coe_ennreal_le_coe_ennreal_iff.mpr hbridge
+  exact hbridgeE.trans hproduct
 
 #print axioms sum_configurationCellTheta_sq_global
 #print axioms sum_configurationCellTheta_sq_le_euler_sq_cap_sq

From 0d627c270424cf12f04da30f31ccf60c9a595f1b Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:29:42 +0300
Subject: [PATCH 09/18] State the direct endpoint in its native ENNReal
 codomain

---
 .../Section9MatchingRestrictionEnvelope.lean        | 13 ++-----------
 1 file changed, 2 insertions(+), 11 deletions(-)

diff --git a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
index 141895a8..3e588e6d 100644
--- a/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
+++ b/625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean
@@ -250,8 +250,7 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope :
         (∀ a, row a ≤ U) →
         (∀ b, col b ≤ U) →
         2 ^ U ≤ m ^ 3 →
-        ((residualActualAttachmentNumerator M (U / 2) row col htotal :
-          ENNReal) : EReal) ≤
+        residualActualAttachmentNumerator M (U / 2) row col htotal ≤
           EReal.exp
             (((kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal) +
               kappaQ * (U : ENNReal) ^ 2 : ENNReal) : EReal)) := by
@@ -293,15 +292,7 @@ theorem exists_absolute_residualActualAttachmentNumerator_le_matchingEnvelope :
       (residualQ M (U / 2) row col) M
       (kappaLambda * (U : ENNReal) ^ 4 / (m : ENNReal))
       (kappaQ * (U : ENNReal) ^ 2) hlambda hqOutside
-  have hbridgeE :
-      ((residualActualAttachmentNumerator M (U / 2) row col htotal :
-        ENNReal) : EReal) ≤
-        (((∏ a : A, ∏ b : B,
-            (1 + residualLambda M (U / 2) row col a b)) *
-          (∏ e ∈ (Finset.univ : Finset (A × B)) \ M,
-            (1 + residualQ M (U / 2) row col e.1 e.2)) : ENNReal) : EReal) :=
-    EReal.coe_ennreal_le_coe_ennreal_iff.mpr hbridge
-  exact hbridgeE.trans hproduct
+  exact hbridge.trans hproduct
 
 #print axioms sum_configurationCellTheta_sq_global
 #print axioms sum_configurationCellTheta_sq_le_euler_sq_cap_sq

From 115006007ffde2c55f1ea8a25d3be7ba4ccb2e3b Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:32:47 +0300
Subject: [PATCH 10/18] Specialize the direct envelope to attained profile
 skeletons

---
 ...ion9ProfileAttachmentMatchingEnvelope.lean | 68 +++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean
new file mode 100644
index 00000000..d414c389
--- /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

From 388c1ac558691179b42da13369215c705b2c878b Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:33:12 +0300
Subject: [PATCH 11/18] Validate the attained-profile envelope endpoint

---
 .../erdos625-matching-restriction-envelope.yml       | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml
index 5869a4d4..6e4752fd 100644
--- a/.github/workflows/erdos625-matching-restriction-envelope.yml
+++ b/.github/workflows/erdos625-matching-restriction-envelope.yml
@@ -4,6 +4,7 @@ on:
   pull_request:
     paths:
       - "625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean"
+      - "625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean"
       - "625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md"
       - ".github/workflows/erdos625-matching-restriction-envelope.yml"
   workflow_dispatch:
@@ -16,12 +17,13 @@ jobs:
     runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@93cb6efe18208431cddfb8368fd83d5badbf9bfd # v5
-      - name: Reject placeholders and project axioms in the new module
+      - 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; then
+            625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean; then
             exit 1
           fi
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
@@ -32,15 +34,15 @@ jobs:
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Build the module and dependency closure warning-fatally
+      - name: Build the profile endpoint and dependency closure warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
           set +e
-          lake build Erdos625.Section9MatchingRestrictionEnvelope --wfail \
+          lake build Erdos625.Section9ProfileAttachmentMatchingEnvelope --wfail \
             > /tmp/section9-envelope-lean.log 2>&1
           status=$?
-          tail -n 240 /tmp/section9-envelope-lean.log
+          tail -n 260 /tmp/section9-envelope-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()

From d5949794a5b80912fca8329fbf4570c87ecd993d Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:33:45 +0300
Subject: [PATCH 12/18] Extend the audit through the attained-profile bridge

---
 .../MATCHING_RESTRICTION_ENVELOPE_AUDIT.md    | 34 +++++++++++++------
 1 file changed, 23 insertions(+), 11 deletions(-)

diff --git a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
index e3405ecc..8afd59ba 100644
--- a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
+++ b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
@@ -2,14 +2,18 @@
 
 ## Scope
 
-This audit accompanies `Erdos625/Section9MatchingRestrictionEnvelope.lean`.
+This audit accompanies:
+
+- `Erdos625/Section9MatchingRestrictionEnvelope.lean`;
+- `Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean`.
+
 The branch is stacked on PR #34 and therefore assumes the finite
 matching-restriction product theorem from
 `Section9MatchingRestrictionProduct.lean`.
 
 ## New checked targets
 
-The new module is intended to prove the following finite statements.
+The first module is intended to prove the following finite statements.
 
 1. The complete square mass of the configuration-cell parameters factorizes as
 
@@ -49,8 +53,14 @@ The new module is intended to prove the following finite statements.
    \right).
    \]
 
-This statement has no traversal parameter, no factor depending on the number
-of profile blocks, and no factor depending on the number of matching edges.
+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 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
 
@@ -61,15 +71,17 @@ of profile blocks, and no factor depending on the number of matching edges.
 - `existsAbsoluteResidualLambdaTotalBound`;
 - exact degree-square and configuration-theta identities from
   `ConfigurationThetaMoments.lean`;
-- `ennreal_polymer_product_le_ereal_exp_sum` for finite products.
+- `ennreal_polymer_product_le_ereal_exp_sum` for finite products;
+- `canonicalReference_residual_parameters` and
+  `profileBlockMargin_total_eq_self` for the attained-profile specialization.
 
 ## Trust gates
 
 The focused workflow:
 
 - rejects `sorry`, `admit`, `sorryAx`, project `axiom`/`constant`, and `unsafe`;
-- builds the pinned Lean 4.31/mathlib project with warnings fatal;
-- compiles the new module directly with `-DwarningAsError=true`;
+- prepares the pinned Lean 4.31/mathlib project;
+- builds the profile endpoint and its dependency closure with `--wfail`;
 - prints the axioms of every new public theorem.
 
 The ordinary repository Lean workflow also runs because this PR changes the
@@ -77,12 +89,12 @@ formalization tree.
 
 ## Deliberate boundary
 
-This module still does not prove the complete Erdős 625 theorem. In particular
-it does not:
+These modules still do not prove the complete Erdős 625 theorem. In particular
+they do not:
 
 - sum the Section VIII bare skeleton weights;
-- specialize the envelope to the midpoint profile and produce the eventual
-  `o(n/(log n)^4)` coefficient;
+- specialize the exponent to the midpoint phase and prove the eventual
+  `O((log n)^2)` or `o(n/(log n)^4)` scale;
 - update the root aggregate or generated self-contained checkpoint;
 - prove the chromatic lower tail, rare seed, or final event intersection.
 

From 64bde7cb2d6c06686c77fa9a97a25df97ac6da35 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:36:57 +0300
Subject: [PATCH 13/18] Add the direct profile log-square adapter

---
 ...ion9ProfileAttachmentMatchingLogScale.lean | 198 ++++++++++++++++++
 1 file changed, 198 insertions(+)
 create mode 100644 625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean
new file mode 100644
index 00000000..64ffd228
--- /dev/null
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean
@@ -0,0 +1,198 @@
+import Erdos625.Section9ProfileAttachmentMatchingEnvelope
+import Erdos625.Section9PhaseTwoPowerCorridor
+import Erdos625.Section9ResidualRegimeScaleAdapters
+
+/-!
+# 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 [exponent, 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

From b78e0ba610e9e4a6ff7413e3178e0dd2fd10f04c Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:37:27 +0300
Subject: [PATCH 14/18] Validate the direct log-square profile endpoint

---
 .../erdos625-matching-restriction-envelope.yml         | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml
index 6e4752fd..6fed9bcb 100644
--- a/.github/workflows/erdos625-matching-restriction-envelope.yml
+++ b/.github/workflows/erdos625-matching-restriction-envelope.yml
@@ -5,6 +5,7 @@ on:
     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:
@@ -23,7 +24,8 @@ jobs:
           if grep -nE \
             '(^|[[:space:]])(sorry|admit|sorryAx)([[:space:][:punct:]]|$)|^[[:space:]]*(axiom|constant|unsafe)[[:space:]]' \
             625/formalization/Erdos625/Section9MatchingRestrictionEnvelope.lean \
-            625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean; then
+            625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean \
+            625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean; then
             exit 1
           fi
       - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1
@@ -34,15 +36,15 @@ jobs:
           use-mathlib-cache: true
           use-github-cache: false
           nanoda: false
-      - name: Build the profile endpoint and dependency closure warning-fatally
+      - name: Build the log-square endpoint and dependency closure warning-fatally
         working-directory: 625/formalization
         shell: bash
         run: |
           set +e
-          lake build Erdos625.Section9ProfileAttachmentMatchingEnvelope --wfail \
+          lake build Erdos625.Section9ProfileAttachmentMatchingLogScale --wfail \
             > /tmp/section9-envelope-lean.log 2>&1
           status=$?
-          tail -n 260 /tmp/section9-envelope-lean.log
+          tail -n 300 /tmp/section9-envelope-lean.log
           exit $status
       - name: Upload focused compiler log
         if: always()

From a3aa2560e5525ce48ff694e14688979b0a6be015 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:38:13 +0300
Subject: [PATCH 15/18] Record the direct log-square specialization

---
 .../MATCHING_RESTRICTION_ENVELOPE_AUDIT.md    | 40 ++++++++++++++-----
 1 file changed, 31 insertions(+), 9 deletions(-)

diff --git a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
index 8afd59ba..7c412a2b 100644
--- a/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
+++ b/625/formalization/MATCHING_RESTRICTION_ENVELOPE_AUDIT.md
@@ -5,7 +5,8 @@
 This audit accompanies:
 
 - `Erdos625/Section9MatchingRestrictionEnvelope.lean`;
-- `Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean`.
+- `Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean`;
+- `Erdos625/Section9ProfileAttachmentMatchingLogScale.lean`.
 
 The branch is stacked on PR #34 and therefore assumes the finite
 matching-restriction product theorem from
@@ -58,6 +59,25 @@ 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.
@@ -73,7 +93,9 @@ matching edges.
   `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.
+  `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
 
@@ -81,7 +103,8 @@ The focused workflow:
 
 - rejects `sorry`, `admit`, `sorryAx`, project `axiom`/`constant`, and `unsafe`;
 - prepares the pinned Lean 4.31/mathlib project;
-- builds the profile endpoint and its dependency closure with `--wfail`;
+- 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
@@ -93,11 +116,10 @@ These modules still do not prove the complete Erdős 625 theorem. In particular
 they do not:
 
 - sum the Section VIII bare skeleton weights;
-- specialize the exponent to the midpoint phase and prove the eventual
-  `O((log n)^2)` or `o(n/(log n)^4)` scale;
 - update the root aggregate or generated self-contained checkpoint;
-- prove the chromatic lower tail, rare seed, or final event intersection.
+- 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 a profile-level asymptotic adapter
-showing that the displayed exponent is `o(amplificationBase n)` uniformly over
-attained canonical demands.
+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.

From fed5811617ab39b9d25f9e18b9cc0ee623912ee0 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:39:24 +0300
Subject: [PATCH 16/18] Cancel superseded focused envelope runs

---
 .github/workflows/erdos625-matching-restriction-envelope.yml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/.github/workflows/erdos625-matching-restriction-envelope.yml b/.github/workflows/erdos625-matching-restriction-envelope.yml
index 6fed9bcb..3c8b30a7 100644
--- a/.github/workflows/erdos625-matching-restriction-envelope.yml
+++ b/.github/workflows/erdos625-matching-restriction-envelope.yml
@@ -10,6 +10,10 @@ on:
       - ".github/workflows/erdos625-matching-restriction-envelope.yml"
   workflow_dispatch:
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 permissions:
   contents: read
 

From 4a981d43a510497cb3bf1d98dce8186eb9d55d31 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:55:58 +0300
Subject: [PATCH 17/18] Silence the attained-profile cap linter

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

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean
index d414c389..b95852c7 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingEnvelope.lean
@@ -30,7 +30,7 @@ theorem exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope :
       0 < kappaQ ∧ kappaQ ≠ ∞ ∧
       ∀ {b n : ℕ} {k : ColoringProfile b}
           (row0 : OrderedProfilePartition n k) (U m : ℕ)
-          (hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
+          (_hcap : ∀ a : ProfileBlockIndex k, profileBlockMargin k a ≤ U)
           (demand : ProfileCanonicalHighSkeleton k U),
         m = canonicalDemandResidualTotal
           (profileBlockMargin k) (profileBlockMargin k) U demand →
@@ -43,12 +43,12 @@ theorem exists_absolute_profileHighSkeletonAttachment_le_matchingEnvelope :
   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
+  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
+    (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

From 628f0c2ba92ef5bc17cd93a6ff14f830962b5f77 Mon Sep 17 00:00:00 2001
From: Samuil Petkov <57594550+SamPetkov@users.noreply.github.com>
Date: Sat, 25 Jul 2026 08:56:48 +0300
Subject: [PATCH 18/18] Fix the log-square imports and warning-fatal lints

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

diff --git a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean
index 64ffd228..97c5a1e1 100644
--- a/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean
+++ b/625/formalization/Erdos625/Section9ProfileAttachmentMatchingLogScale.lean
@@ -1,6 +1,7 @@
 import Erdos625.Section9ProfileAttachmentMatchingEnvelope
 import Erdos625.Section9PhaseTwoPowerCorridor
 import Erdos625.Section9ResidualRegimeScaleAdapters
+import Erdos625.Section9ERealENNRealExpTransport
 
 /-!
 # Section IX: direct matching-restriction profile log scale
@@ -36,7 +37,7 @@ theorem matchingRestrictionEnvelope_bound
     (hm0 : 0 < m)
     (hkappaLambda0 : 0 ≤ kappaLambda)
     (hkappaQ0 : 0 ≤ kappaQ)
-    (hCU0 : 0 ≤ C_U)
+    (_hCU0 : 0 ≤ C_U)
     (hm : n / L ^ 6 ≤ m)
     (hU : U ≤ C_U * L)
     (hL8 : L ^ 8 ≤ n) :
@@ -180,7 +181,7 @@ theorem eventually_profileHighSkeletonAttachment_le_matching_logScale :
     hm hUreal hlog8
   have hparts := ENNReal.add_ne_top.mp hexponent
   rw [ENNReal.toReal_add hparts.1 hparts.2]
-  simp only [exponent, ENNReal.toReal_mul, ENNReal.toReal_div,
+  simp only [ENNReal.toReal_mul, ENNReal.toReal_div,
     ENNReal.toReal_pow, ENNReal.toReal_natCast]
   change
     kappaLambda.toReal * (U : ℝ) ^ 4 / (m : ℝ) +