diff --git a/proof/formalization/R3Cert/BGSCLCeil.lean b/proof/formalization/R3Cert/BGSCLCeil.lean
new file mode 100644
index 00000000..153429d3
--- /dev/null
+++ b/proof/formalization/R3Cert/BGSCLCeil.lean
@@ -0,0 +1,312 @@
+/-
+  The per-hub branch-ceiling step `CeilStep` (BGSCLHub), degree ≤ 6.
+
+  For a hub of root-degree `d ≤ 6`, the concave-log tangent at the EXACT all-cherry slope `μ* = 3/(4d-1)` (which
+  lies in the invariant price interval `I` for `d ≤ 6`) makes the child `S`-terms cancel exactly against the child
+  SCL bound, giving `bell (node cs) ≤ A_d := (d-1)(log(3/2) − 2F*) + log((4d-1)/(3d)) − F*`.  `A_d ≤ 0` is a clean
+  rational log inequality — strict for `d ≤ 5`, and EXACTLY `0` at `d = 6` (the arithmetic tie
+  `(3/2)^5·(23/18) = 621/64`, i.e. the `n = 11` degree-6 near-broom).  This closes the ceiling step for `d ≤ 6`.
+  (The `d ≥ 7` tail is the reachable-`y` envelope, gated in Telperion by `HighDegreeTailCertificate`.)
+
+  conjecture1_proved = False.
+-/
+import Mathlib
+import R3Cert.BGSCLInduction
+import R3Cert.BGSCLStep
+import R3Cert.BGSCLHub
+
+namespace R3Cert
+namespace BGSCL
+
+/-- All-cherry ceiling, d=2: `A_2 = log(3/2) + log(7/6) − 3F* ≤ 0`. -/
+theorem acl_d2 : Real.log (3/2) + Real.log (7/6) - 3*FSTAR ≤ 0 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(Real.log (3/2) + Real.log (7/6) - 3*(Real.log (621/64)/11))
+      = Real.log ((3/2)^11 * (7/6)^11 * (64/621)^3) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^11 * (7/6)^11 * (64/621)^3) ≤ 0 :=
+    Real.log_nonpos (by positivity) (by norm_num)
+  nlinarith [hcomb, hX]
+
+/-- All-cherry ceiling, d=3: `A_3 = 2 log(3/2) + log(11/9) − 5F* ≤ 0`. -/
+theorem acl_d3 : 2*Real.log (3/2) + Real.log (11/9) - 5*FSTAR ≤ 0 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(2*Real.log (3/2) + Real.log (11/9) - 5*(Real.log (621/64)/11))
+      = Real.log ((3/2)^22 * (11/9)^11 * (64/621)^5) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^22 * (11/9)^11 * (64/621)^5) ≤ 0 :=
+    Real.log_nonpos (by positivity) (by norm_num)
+  nlinarith [hcomb, hX]
+
+/-- All-cherry ceiling, d=4: `A_4 = 3 log(3/2) + log(5/4) − 7F* ≤ 0`. -/
+theorem acl_d4 : 3*Real.log (3/2) + Real.log (5/4) - 7*FSTAR ≤ 0 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(3*Real.log (3/2) + Real.log (5/4) - 7*(Real.log (621/64)/11))
+      = Real.log ((3/2)^33 * (5/4)^11 * (64/621)^7) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^33 * (5/4)^11 * (64/621)^7) ≤ 0 :=
+    Real.log_nonpos (by positivity) (by norm_num)
+  nlinarith [hcomb, hX]
+
+/-- All-cherry ceiling, d=5: `A_5 = 4 log(3/2) + log(19/15) − 9F* ≤ 0`. -/
+theorem acl_d5 : 4*Real.log (3/2) + Real.log (19/15) - 9*FSTAR ≤ 0 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(4*Real.log (3/2) + Real.log (19/15) - 9*(Real.log (621/64)/11))
+      = Real.log ((3/2)^44 * (19/15)^11 * (64/621)^9) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^44 * (19/15)^11 * (64/621)^9) ≤ 0 :=
+    Real.log_nonpos (by positivity) (by norm_num)
+  nlinarith [hcomb, hX]
+
+/-- All-cherry ceiling, d=6: `A_6 = 5 log(3/2) + log(23/18) − 11F* ≤ 0` — EXACTLY `0` (the tie
+    `(3/2)^5·(23/18) = 621/64`). -/
+theorem acl_d6 : 5*Real.log (3/2) + Real.log (23/18) - 11*FSTAR ≤ 0 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(5*Real.log (3/2) + Real.log (23/18) - 11*(Real.log (621/64)/11))
+      = Real.log ((3/2)^55 * (23/18)^11 * (64/621)^11) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^55 * (23/18)^11 * (64/621)^11) ≤ 0 :=
+    Real.log_nonpos (by positivity) (by norm_num)
+  nlinarith [hcomb, hX]
+
+/-- `bell cherry ≤ 0` (`log(3/2) − 2F* ≤ 0`). -/
+theorem bell_cherry_nonpos : bell cherry ≤ 0 := by
+  rw [bell_cherry]
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(Real.log (3/2) - 2*(Real.log (621/64)/11))
+      = Real.log ((3/2)^11 * (64/621)^2) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^11 * (64/621)^2) ≤ 0 := Real.log_nonpos (by positivity) (by norm_num)
+  nlinarith [hcomb, hX]
+
+/-- **Ceiling step, d=2** (`cs.length = 1`).  Leaf child ⟹ hub `= cherry` (`bell cherry ≤ 0`); non-leaf ⟹
+    the all-cherry decouple at `μ* = 3/7` gives `bell (node cs) ≤ A_2 = log(3/2) + log(7/6) − 3F* ≤ 0`. -/
+theorem ceil_hub_d2 {cs : List Branch} (hlen : cs.length = 1)
+    (hchild : ∀ c ∈ cs, PSCLne c) : bell (Branch.node cs) ≤ 0 := by
+  obtain ⟨c, rfl⟩ : ∃ c, cs = [c] := by
+    cases cs with
+    | nil => simp at hlen
+    | cons c t => cases t with
+      | nil => exact ⟨c, rfl⟩
+      | cons _ _ => simp at hlen
+  have hc1 : PSCLne c := hchild c (List.mem_cons.mpr (Or.inl rfl))
+  by_cases hc : c = Branch.node []
+  · subst hc
+    show bell (Branch.node [Branch.node []]) ≤ 0
+    have hch : Branch.node [Branch.node []] = cherry := rfl
+    rw [hch]; exact bell_cherry_nonpos
+  · set S := (([c] : List Branch).map bY).sum with hSdef
+    have hSnn : 0 ≤ S := by
+      rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+      obtain ⟨z, _, rfl⟩ := hx; exact bY_nonneg z
+    have hlenR : (([c] : List Branch).length : ℝ) = 1 := by norm_num
+    have hchild2 : ∀ x ∈ ([c] : List Branch), bV (3/7) x ≤ bV (3/7) cherry := by
+      intro x hx; rw [List.mem_singleton] at hx; subst hx
+      exact hc1 hc (3/7) (by constructor <;> norm_num)
+    have hsum : (([c] : List Branch).map bell).sum
+        ≤ (([c] : List Branch).length : ℝ) * bV (3/7) cherry - (3/7) * (([c] : List Branch).map bY).sum :=
+      child_bell_sum_le (3/7) [c] hchild2
+    rw [hlenR, ← hSdef] at hsum
+    have htan := bell_node_tangent [c] (s0 := 1/3) (by norm_num)
+    rw [hlenR, ← hSdef] at htan
+    have hlogeq : Real.log (1 + 1/3/((1:ℝ)+1)) = Real.log (7/6) := by norm_num
+    have hden : ((1:ℝ)+1)+1/3 = 7/3 := by norm_num
+    rw [hlogeq, hden] at htan
+    have hRHS : bell (Branch.node [c])
+        ≤ (1 * bV (3/7) cherry - (3/7) * S) + (Real.log (7/6) + (S - 1/3)/(7/3) - FSTAR) := by
+      linarith [htan, hsum]
+    have hbridge : (1 * bV (3/7) cherry - (3/7) * S) + (Real.log (7/6) + (S - 1/3)/(7/3) - FSTAR)
+        = Real.log (3/2) + Real.log (7/6) - 3*FSTAR := by
+      rw [bV, bell_cherry, bY_cherry]; ring
+    linarith [hRHS, hbridge, acl_d2]
+
+/-- **Ceiling step, d=3** (`cs.length = 2`).  `μ* = 3/11 ∈ I`, `s0 = 2/3` ⟹ `bell (node cs) ≤ A_3 ≤ 0`. -/
+theorem ceil_hub_d3 {cs : List Branch} (hlen : cs.length = 2)
+    (hchild : ∀ c ∈ cs, PSCLne c) : bell (Branch.node cs) ≤ 0 := by
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨z, _, rfl⟩ := hx; exact bY_nonneg z
+  have hlenR : (cs.length : ℝ) = 2 := by exact_mod_cast hlen
+  have hchild2 : ∀ c ∈ cs, bV (3/11) c ≤ bV (3/11) cherry := by
+    intro c hc
+    by_cases hleaf : c = Branch.node []
+    · subst hleaf; exact leaf_le_cherry (by norm_num)
+    · exact hchild c hc hleaf (3/11) (by constructor <;> norm_num)
+  have hsum : (cs.map bell).sum ≤ (cs.length : ℝ) * bV (3/11) cherry - (3/11) * (cs.map bY).sum :=
+    child_bell_sum_le (3/11) cs hchild2
+  rw [hlenR, ← hSdef] at hsum
+  have htan := bell_node_tangent cs (s0 := 2/3) (by norm_num)
+  rw [hlenR, ← hSdef] at htan
+  have hlogeq : Real.log (1 + 2/3/((2:ℝ)+1)) = Real.log (11/9) := by norm_num
+  have hden : ((2:ℝ)+1)+2/3 = 11/3 := by norm_num
+  rw [hlogeq, hden] at htan
+  have hRHS : bell (Branch.node cs)
+      ≤ (2 * bV (3/11) cherry - (3/11) * S) + (Real.log (11/9) + (S - 2/3)/(11/3) - FSTAR) := by
+    linarith [htan, hsum]
+  have hbridge : (2 * bV (3/11) cherry - (3/11) * S) + (Real.log (11/9) + (S - 2/3)/(11/3) - FSTAR)
+      = 2*Real.log (3/2) + Real.log (11/9) - 5*FSTAR := by
+    rw [bV, bell_cherry, bY_cherry]; ring
+  linarith [hRHS, hbridge, acl_d3]
+
+/-- **Ceiling step, d=4** (`cs.length = 3`).  `μ* = 1/5 ∈ I`, `s0 = 1` ⟹ `bell (node cs) ≤ A_4 ≤ 0`. -/
+theorem ceil_hub_d4 {cs : List Branch} (hlen : cs.length = 3)
+    (hchild : ∀ c ∈ cs, PSCLne c) : bell (Branch.node cs) ≤ 0 := by
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨z, _, rfl⟩ := hx; exact bY_nonneg z
+  have hlenR : (cs.length : ℝ) = 3 := by exact_mod_cast hlen
+  have hchild2 : ∀ c ∈ cs, bV (1/5) c ≤ bV (1/5) cherry := by
+    intro c hc
+    by_cases hleaf : c = Branch.node []
+    · subst hleaf; exact leaf_le_cherry (by norm_num)
+    · exact hchild c hc hleaf (1/5) (by constructor <;> norm_num)
+  have hsum : (cs.map bell).sum ≤ (cs.length : ℝ) * bV (1/5) cherry - (1/5) * (cs.map bY).sum :=
+    child_bell_sum_le (1/5) cs hchild2
+  rw [hlenR, ← hSdef] at hsum
+  have htan := bell_node_tangent cs (s0 := 1) (by norm_num)
+  rw [hlenR, ← hSdef] at htan
+  have hlogeq : Real.log (1 + 1/((3:ℝ)+1)) = Real.log (5/4) := by norm_num
+  have hden : ((3:ℝ)+1)+1 = 5 := by norm_num
+  rw [hlogeq, hden] at htan
+  have hRHS : bell (Branch.node cs)
+      ≤ (3 * bV (1/5) cherry - (1/5) * S) + (Real.log (5/4) + (S - 1)/5 - FSTAR) := by
+    linarith [htan, hsum]
+  have hbridge : (3 * bV (1/5) cherry - (1/5) * S) + (Real.log (5/4) + (S - 1)/5 - FSTAR)
+      = 3*Real.log (3/2) + Real.log (5/4) - 7*FSTAR := by
+    rw [bV, bell_cherry, bY_cherry]; ring
+  linarith [hRHS, hbridge, acl_d4]
+
+/-- **Ceiling step, d=5** (`cs.length = 4`).  `μ* = 3/19 ∈ I`, `s0 = 4/3` ⟹ `bell (node cs) ≤ A_5 ≤ 0`. -/
+theorem ceil_hub_d5 {cs : List Branch} (hlen : cs.length = 4)
+    (hchild : ∀ c ∈ cs, PSCLne c) : bell (Branch.node cs) ≤ 0 := by
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨z, _, rfl⟩ := hx; exact bY_nonneg z
+  have hlenR : (cs.length : ℝ) = 4 := by exact_mod_cast hlen
+  have hchild2 : ∀ c ∈ cs, bV (3/19) c ≤ bV (3/19) cherry := by
+    intro c hc
+    by_cases hleaf : c = Branch.node []
+    · subst hleaf; exact leaf_le_cherry (by norm_num)
+    · exact hchild c hc hleaf (3/19) (by constructor <;> norm_num)
+  have hsum : (cs.map bell).sum ≤ (cs.length : ℝ) * bV (3/19) cherry - (3/19) * (cs.map bY).sum :=
+    child_bell_sum_le (3/19) cs hchild2
+  rw [hlenR, ← hSdef] at hsum
+  have htan := bell_node_tangent cs (s0 := 4/3) (by norm_num)
+  rw [hlenR, ← hSdef] at htan
+  have hlogeq : Real.log (1 + 4/3/((4:ℝ)+1)) = Real.log (19/15) := by norm_num
+  have hden : ((4:ℝ)+1)+4/3 = 19/3 := by norm_num
+  rw [hlogeq, hden] at htan
+  have hRHS : bell (Branch.node cs)
+      ≤ (4 * bV (3/19) cherry - (3/19) * S) + (Real.log (19/15) + (S - 4/3)/(19/3) - FSTAR) := by
+    linarith [htan, hsum]
+  have hbridge : (4 * bV (3/19) cherry - (3/19) * S) + (Real.log (19/15) + (S - 4/3)/(19/3) - FSTAR)
+      = 4*Real.log (3/2) + Real.log (19/15) - 9*FSTAR := by
+    rw [bV, bell_cherry, bY_cherry]; ring
+  linarith [hRHS, hbridge, acl_d5]
+
+/-- **Ceiling step, d=6** (`cs.length = 5`).  `μ* = 3/23 ∈ I`, `s0 = 5/3` ⟹ `bell (node cs) ≤ A_6 = 0`
+    (the exact `n=11` degree-6 tie). -/
+theorem ceil_hub_d6 {cs : List Branch} (hlen : cs.length = 5)
+    (hchild : ∀ c ∈ cs, PSCLne c) : bell (Branch.node cs) ≤ 0 := by
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨z, _, rfl⟩ := hx; exact bY_nonneg z
+  have hlenR : (cs.length : ℝ) = 5 := by exact_mod_cast hlen
+  have hchild2 : ∀ c ∈ cs, bV (3/23) c ≤ bV (3/23) cherry := by
+    intro c hc
+    by_cases hleaf : c = Branch.node []
+    · subst hleaf; exact leaf_le_cherry (by norm_num)
+    · exact hchild c hc hleaf (3/23) (by constructor <;> norm_num)
+  have hsum : (cs.map bell).sum ≤ (cs.length : ℝ) * bV (3/23) cherry - (3/23) * (cs.map bY).sum :=
+    child_bell_sum_le (3/23) cs hchild2
+  rw [hlenR, ← hSdef] at hsum
+  have htan := bell_node_tangent cs (s0 := 5/3) (by norm_num)
+  rw [hlenR, ← hSdef] at htan
+  have hlogeq : Real.log (1 + 5/3/((5:ℝ)+1)) = Real.log (23/18) := by norm_num
+  have hden : ((5:ℝ)+1)+5/3 = 23/3 := by norm_num
+  rw [hlogeq, hden] at htan
+  have hRHS : bell (Branch.node cs)
+      ≤ (5 * bV (3/23) cherry - (3/23) * S) + (Real.log (23/18) + (S - 5/3)/(23/3) - FSTAR) := by
+    linarith [htan, hsum]
+  have hbridge : (5 * bV (3/23) cherry - (3/23) * S) + (Real.log (23/18) + (S - 5/3)/(23/3) - FSTAR)
+      = 5*Real.log (3/2) + Real.log (23/18) - 11*FSTAR := by
+    rw [bV, bell_cherry, bY_cherry]; ring
+  linarith [hRHS, hbridge, acl_d6]
+
+/-- `0 ≤ F*` (`621/64 ≥ 1`). -/
+theorem fstar_nonneg : (0:ℝ) ≤ FSTAR := by
+  rw [FSTAR]; exact div_nonneg (Real.log_nonneg (by norm_num)) (by norm_num)
+
+/-- **The d≥7 hub-ceiling residual.**  For a hub of root-degree `d ≥ 7`, `bell (node cs) ≤ 0` given the child
+    ceilings AND child SCL.  This is the ONLY residual of the whole branch-ceiling + SCL after the `d ≤ 6`
+    ceilings are proven (numeric margin `+0.0015`, worst at the all-cherry hub).  It is the high-degree tail of
+    the `M_d` frontier: the all-cherry price `μ* = 3/(4d-1)` falls BELOW the invariant interval `I` for `d ≥ 7`,
+    so the `d ≤ 6` all-cherry decouple does not apply, and the SCL-on-`I` bound alone overshoots by `~0.004`
+    (the min-`y` regime needs the reachable-`y` structure).  Gated in Telperion (`HighDegreeTailCertificate` +
+    the near-broom certificates).  `conjecture1_proved = False`. -/
+def CeilStepHi : Prop :=
+  ∀ cs : List Branch, 6 ≤ cs.length →
+    (∀ c ∈ cs, bell c ≤ 0) → (∀ c ∈ cs, PSCLne c) → bell (Branch.node cs) ≤ 0
+
+/-- **The full per-hub ceiling step, from the d≥7 residual.**  `d ≤ 6` is PROVEN (the all-cherry decouple,
+    including the exact `d = 6` arithmetic tie `acl_d6`); `d ≥ 7` is `CeilStepHi`.  Note the `d ≤ 6` ceilings
+    need only the child SCL (not the child ceilings) — the child ceilings are consumed only by the tail. -/
+theorem ceilStep_of_hi (hhi : CeilStepHi) : CeilStep := by
+  intro cs hcc hcs
+  rcases cs with _ | ⟨a, t⟩
+  · rw [bell_leaf]; linarith [fstar_nonneg]
+  · have h1 : 1 ≤ (a :: t).length := by simp
+    rcases Nat.lt_or_ge (a :: t).length 6 with hlo | hge
+    · rcases (by omega : (a :: t).length = 1 ∨ (a :: t).length = 2 ∨ (a :: t).length = 3
+          ∨ (a :: t).length = 4 ∨ (a :: t).length = 5) with h | h | h | h | h
+      · exact ceil_hub_d2 h hcs
+      · exact ceil_hub_d3 h hcs
+      · exact ceil_hub_d4 h hcs
+      · exact ceil_hub_d5 h hcs
+      · exact ceil_hub_d6 h hcs
+    · exact hhi (a :: t) hge hcc hcs
+
+/-- **Joint ceiling + SCL for every branch, from the d≥7 residual.**  The `d ≤ 6` ceiling — including the tight
+    `n = 11` degree-6 arithmetic tie — is now PROVEN in Lean; the ENTIRE branch ceiling `∀ b, bell b ≤ 0` and the
+    leaf-excluding SCL `∀ b, PSCLne b` reduce to the single high-degree-tail residual `CeilStepHi` (margin
+    `+0.0015`).  `conjecture1_proved = False`. -/
+theorem ceil_and_scl_of_ceilStepHi (hhi : CeilStepHi) : ∀ b, bell b ≤ 0 ∧ PSCLne b :=
+  ceil_and_scl_of_ceilStep (ceilStep_of_hi hhi)
+
+/-- The branch ceiling `∀ b, bell b ≤ 0` from the d≥7 residual. -/
+theorem bell_ceiling_of_ceilStepHi (hhi : CeilStepHi) : ∀ b, bell b ≤ 0 :=
+  fun b => (ceil_and_scl_of_ceilStepHi hhi b).1
+
+/-- The SCL `∀ b, PSCLne b` from the d≥7 residual. -/
+theorem scl_of_ceilStepHi (hhi : CeilStepHi) : ∀ b, PSCLne b :=
+  fun b => (ceil_and_scl_of_ceilStepHi hhi b).2
+
+end BGSCL
+end R3Cert
diff --git a/proof/formalization/R3Cert/BGSCLCeilHi.lean b/proof/formalization/R3Cert/BGSCLCeilHi.lean
new file mode 100644
index 00000000..dd56275b
--- /dev/null
+++ b/proof/formalization/R3Cert/BGSCLCeilHi.lean
@@ -0,0 +1,138 @@
+/-
+  Per-child-degree BUDGET lemmas toward the d≥7 hub-ceiling residual `CeilStepHi` (BGSCLCeil).
+
+  The natural attack on `CeilStepHi` (`bell(node cs) ≤ 0` for a hub of degree `d ≥ 7`) is the all-cherry
+  concave-log tangent at slope `μ* = 3/(4d-1)`, using the SHARP per-degree ceiling `bell(c) ≤ cbound(deg c)`
+  (`= A_k` for `3 ≤ k ≤ 6`, `= log(3/2) − 2F*` for `k = 2` [the cherry, NOT `A_2`], `= −F*` for a leaf, `= 0`
+  for `k ≥ 7`) with `deg-2` children handled by SCL extend-below-`I` (their `y ≥ 1/3`).  This closes EXACTLY for
+  `7 ≤ d ≤ 15`; for `d ≥ 16` the price `μ*` drops below the crossover and the incompatible (bell-max, y-max) of
+  low-degree children breaks the per-child inequality — the genuine `TieSlack` regime (matching the BG ledger's
+  step 2a, `k ≥ 16`), which needs a separate slack argument.  So these lemmas are NECESSARY infrastructure but
+  do NOT on their own discharge `CeilStepHi`; the `d ≥ 16` tail remains open.
+
+  The `key_dk` lemmas (`7·A_k + 1/k ≤ F*`, the `d = 7` per-child budget; `d ≥ 7` follows by `A_k ≤ 0`
+  monotonicity) reduce (11×-clear) to `log(W_k) ≤ −11/k`, discharged by bounding `exp(11/k) ≤ r_k` (small
+  integer, via `(exp(11/k))^k = (exp 1)^11 < 2.7182818286^11 ≤ r_k^k`) then `W_k · r_k ≤ 1` (`norm_num`, no
+  large powers).  `k = 5, 6` instead use `A_k ≤ 0` + `1/k ≤ F*` (avoids the huge `norm_num`).
+  conjecture1_proved = False.
+-/
+import Mathlib
+import R3Cert.BGSCLInduction
+import R3Cert.BGSCLStep
+import R3Cert.BGSCLHub
+import R3Cert.BGSCLCeil
+
+namespace R3Cert
+namespace BGSCL
+
+/-- Per-child budget, k=2: `7·A_2 + 1/2 ≤ F*`, `A_2 = log(3/2) + log(7/6) − 3F*`. -/
+theorem key_d2 : 7*(Real.log (3/2) + Real.log (7/6) - 3*FSTAR) + 1/2 ≤ FSTAR := by
+  have e1 : (Real.exp (11/2))^2 = Real.exp 11 := by rw [← Real.exp_nat_mul]; congr 1; norm_num
+  have e2 : (Real.exp 1)^11 = Real.exp 11 := by rw [← Real.exp_nat_mul]; congr 1; norm_num
+  have hb : (Real.exp 1)^11 ≤ (2.7182818286:ℝ)^11 :=
+    pow_le_pow_left₀ (Real.exp_nonneg 1) (le_of_lt Real.exp_one_lt_d9) 11
+  have hexp : Real.exp (11/2) ≤ (300:ℝ) := by
+    have hpk : (Real.exp (11/2))^2 ≤ (300:ℝ)^2 := by
+      rw [e1, ← e2]; have : (2.7182818286:ℝ)^11 ≤ (300:ℝ)^2 := by norm_num
+      linarith
+    exact le_of_pow_le_pow_left₀ (by norm_num) (by norm_num) hpk
+  have hWK : (0:ℝ) < (3/2:ℝ)^77*(7/6)^77*(64/621)^22 := by positivity
+  have h1 : ((3/2:ℝ)^77*(7/6)^77*(64/621)^22) * Real.exp (11/2) ≤ 1 := by
+    have hm := mul_le_mul_of_nonneg_left hexp (le_of_lt hWK)
+    have hWr : ((3/2:ℝ)^77*(7/6)^77*(64/621)^22) * (300:ℝ) ≤ 1 := by norm_num
+    linarith
+  have hlogW : Real.log ((3/2:ℝ)^77*(7/6)^77*(64/621)^22) ≤ -(11/2) := by
+    have h3 : Real.log (((3/2:ℝ)^77*(7/6)^77*(64/621)^22) * Real.exp (11/2)) ≤ 0 := by
+      rw [Real.log_le_iff_le_exp (by positivity), Real.exp_zero]; exact h1
+    rw [Real.log_mul (ne_of_gt hWK) (ne_of_gt (Real.exp_pos _)), Real.log_exp] at h3; linarith
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  have hcomb : (11:ℝ)*(7*(Real.log (3/2) + Real.log (7/6) - 3*FSTAR) + 1/2 - FSTAR)
+      = Real.log ((3/2:ℝ)^77*(7/6)^77*(64/621)^22) + 11/2 := by
+    rw [hF, Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow, show (64:ℝ)/621=(621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  linarith [hcomb, hlogW]
+
+/-- Per-child budget, k=3: `7·A_3 + 1/3 ≤ F*`, `A_3 = 2 log(3/2) + log(11/9) − 5F*`. -/
+theorem key_d3 : 7*(2*Real.log (3/2) + Real.log (11/9) - 5*FSTAR) + 1/3 ≤ FSTAR := by
+  have e1 : (Real.exp (11/3))^3 = Real.exp 11 := by rw [← Real.exp_nat_mul]; congr 1; norm_num
+  have e2 : (Real.exp 1)^11 = Real.exp 11 := by rw [← Real.exp_nat_mul]; congr 1; norm_num
+  have hb : (Real.exp 1)^11 ≤ (2.7182818286:ℝ)^11 :=
+    pow_le_pow_left₀ (Real.exp_nonneg 1) (le_of_lt Real.exp_one_lt_d9) 11
+  have hexp : Real.exp (11/3) ≤ (45:ℝ) := by
+    have hpk : (Real.exp (11/3))^3 ≤ (45:ℝ)^3 := by
+      rw [e1, ← e2]; have : (2.7182818286:ℝ)^11 ≤ (45:ℝ)^3 := by norm_num
+      linarith
+    exact le_of_pow_le_pow_left₀ (by norm_num) (by norm_num) hpk
+  have hWK : (0:ℝ) < (3/2:ℝ)^154*(11/9)^77*(64/621)^36 := by positivity
+  have h1 : ((3/2:ℝ)^154*(11/9)^77*(64/621)^36) * Real.exp (11/3) ≤ 1 := by
+    have hm := mul_le_mul_of_nonneg_left hexp (le_of_lt hWK)
+    have hWr : ((3/2:ℝ)^154*(11/9)^77*(64/621)^36) * (45:ℝ) ≤ 1 := by norm_num
+    linarith
+  have hlogW : Real.log ((3/2:ℝ)^154*(11/9)^77*(64/621)^36) ≤ -(11/3) := by
+    have h3 : Real.log (((3/2:ℝ)^154*(11/9)^77*(64/621)^36) * Real.exp (11/3)) ≤ 0 := by
+      rw [Real.log_le_iff_le_exp (by positivity), Real.exp_zero]; exact h1
+    rw [Real.log_mul (ne_of_gt hWK) (ne_of_gt (Real.exp_pos _)), Real.log_exp] at h3; linarith
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  have hcomb : (11:ℝ)*(7*(2*Real.log (3/2) + Real.log (11/9) - 5*FSTAR) + 1/3 - FSTAR)
+      = Real.log ((3/2:ℝ)^154*(11/9)^77*(64/621)^36) + 11/3 := by
+    rw [hF, Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow, show (64:ℝ)/621=(621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  linarith [hcomb, hlogW]
+
+/-- Per-child budget, k=4 (binding): `7·A_4 + 1/4 ≤ F*`, `A_4 = 3 log(3/2) + log(5/4) − 7F*`. -/
+theorem key_d4 : 7*(3*Real.log (3/2) + Real.log (5/4) - 7*FSTAR) + 1/4 ≤ FSTAR := by
+  have e1 : (Real.exp (11/4))^4 = Real.exp 11 := by rw [← Real.exp_nat_mul]; congr 1; norm_num
+  have e2 : (Real.exp 1)^11 = Real.exp 11 := by rw [← Real.exp_nat_mul]; congr 1; norm_num
+  have hb : (Real.exp 1)^11 ≤ (2.7182818286:ℝ)^11 :=
+    pow_le_pow_left₀ (Real.exp_nonneg 1) (le_of_lt Real.exp_one_lt_d9) 11
+  have hexp : Real.exp (11/4) ≤ (16:ℝ) := by
+    have hpk : (Real.exp (11/4))^4 ≤ (16:ℝ)^4 := by
+      rw [e1, ← e2]; have : (2.7182818286:ℝ)^11 ≤ (16:ℝ)^4 := by norm_num
+      linarith
+    exact le_of_pow_le_pow_left₀ (by norm_num) (by norm_num) hpk
+  have hWK : (0:ℝ) < (3/2:ℝ)^231*(5/4)^77*(64/621)^50 := by positivity
+  have h1 : ((3/2:ℝ)^231*(5/4)^77*(64/621)^50) * Real.exp (11/4) ≤ 1 := by
+    have hm := mul_le_mul_of_nonneg_left hexp (le_of_lt hWK)
+    have hWr : ((3/2:ℝ)^231*(5/4)^77*(64/621)^50) * (16:ℝ) ≤ 1 := by norm_num
+    linarith
+  have hlogW : Real.log ((3/2:ℝ)^231*(5/4)^77*(64/621)^50) ≤ -(11/4) := by
+    have h3 : Real.log (((3/2:ℝ)^231*(5/4)^77*(64/621)^50) * Real.exp (11/4)) ≤ 0 := by
+      rw [Real.log_le_iff_le_exp (by positivity), Real.exp_zero]; exact h1
+    rw [Real.log_mul (ne_of_gt hWK) (ne_of_gt (Real.exp_pos _)), Real.log_exp] at h3; linarith
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  have hcomb : (11:ℝ)*(7*(3*Real.log (3/2) + Real.log (5/4) - 7*FSTAR) + 1/4 - FSTAR)
+      = Real.log ((3/2:ℝ)^231*(5/4)^77*(64/621)^50) + 11/4 := by
+    rw [hF, Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow, show (64:ℝ)/621=(621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  linarith [hcomb, hlogW]
+
+/-- `1/5 ≤ F*` (`11/5 ≤ log(621/64)`, via `exp(11/5) ≤ 9.5 ≤ 621/64`). -/
+theorem recip5_le_fstar : (1:ℝ)/5 ≤ FSTAR := by
+  have e1 : (Real.exp (11/5))^5 = Real.exp 11 := by rw [← Real.exp_nat_mul]; congr 1; norm_num
+  have e2 : (Real.exp 1)^11 = Real.exp 11 := by rw [← Real.exp_nat_mul]; congr 1; norm_num
+  have hb : (Real.exp 1)^11 ≤ (2.7182818286:ℝ)^11 :=
+    pow_le_pow_left₀ (Real.exp_nonneg 1) (le_of_lt Real.exp_one_lt_d9) 11
+  have hexp : Real.exp (11/5) ≤ (9.5:ℝ) := by
+    have hpk : (Real.exp (11/5))^5 ≤ (9.5:ℝ)^5 := by
+      rw [e1, ← e2]; have : (2.7182818286:ℝ)^11 ≤ (9.5:ℝ)^5 := by norm_num
+      linarith
+    exact le_of_pow_le_pow_left₀ (by norm_num) (by norm_num) hpk
+  have hlog : (11:ℝ)/5 ≤ Real.log (621/64) := by
+    rw [Real.le_log_iff_exp_le (by norm_num)]; exact le_trans hexp (by norm_num)
+  rw [FSTAR]; linarith
+
+/-- Per-child budget, k=5: `7·A_5 + 1/5 ≤ F*` — since `A_5 ≤ 0` (`acl_d5`) and `1/5 ≤ F*`. -/
+theorem key_d5 : 7*(4*Real.log (3/2) + Real.log (19/15) - 9*FSTAR) + 1/5 ≤ FSTAR := by
+  have hA5 : 4*Real.log (3/2) + Real.log (19/15) - 9*FSTAR ≤ 0 := acl_d5
+  linarith [hA5, recip5_le_fstar]
+
+/-- Per-child budget, k=6: `7·A_6 + 1/6 ≤ F*` — since `A_6 ≤ 0` (`acl_d6`) and `1/6 ≤ 1/5 ≤ F*`. -/
+theorem key_d6 : 7*(5*Real.log (3/2) + Real.log (23/18) - 11*FSTAR) + 1/6 ≤ FSTAR := by
+  have hA6 : 5*Real.log (3/2) + Real.log (23/18) - 11*FSTAR ≤ 0 := acl_d6
+  linarith [hA6, recip5_le_fstar]
+
+end BGSCL
+end R3Cert
diff --git a/proof/formalization/R3Cert/BGSCLDecouple.lean b/proof/formalization/R3Cert/BGSCLDecouple.lean
new file mode 100644
index 00000000..c00fdfd5
--- /dev/null
+++ b/proof/formalization/R3Cert/BGSCLDecouple.lean
@@ -0,0 +1,178 @@
+/-
+  SCL per-hub decouple residual — the `nlinarith` core of `FlowedHubStep` (the d≤6 tangent decouple).
+  This discharges the Telperion `PerHubDecoupleResidualCertificate` in Lean.  The d=2 residual `R(S) ≤ 0`
+  is PROVEN here (no `sorry`, axiom-clean); d=3..6 follow by the SAME template (`log((4d-1)/(3d))` combined via
+  `×11` into `log(rational)`, bounded by a clean `exp` power, then `μ/(d+S)` cleared and `nlinarith` on the
+  upward parabola in `S`).  Verified against the Telperion cert (20 endpoint atoms, margin ≥ +0.007).
+  conjecture1_proved = False.
+-/
+import Mathlib
+import R3Cert.BGSCLInduction
+import R3Cert.BGSCLStep
+
+namespace R3Cert
+namespace BGSCL
+
+/-- The keystone log bound for the d=2 decouple: `g := log(7/6) − F* ≤ −1/22`.  Via `11·g =
+    log((7/6)^11 · 64/621)` and the clean half-integer bound `exp(1/2) = √(exp 1) < 1.6489`. -/
+theorem log76_gap : Real.log (7/6) - FSTAR ≤ -(1/22) := by
+  have hF : FSTAR = Real.log (621 / 64) / 11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ) * (Real.log (7/6) - Real.log (621/64)/11)
+      = Real.log ((7/6)^11 * (64/621)) := by
+    rw [Real.log_mul (by positivity) (by norm_num), Real.log_pow,
+      show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]; ring
+  have hval : Real.log ((7/6)^11 * (64/621)) ≤ -(1/2) := by
+    rw [Real.log_le_iff_le_exp (by positivity), Real.exp_neg]
+    have hehalf : Real.exp (1/2) * Real.exp (1/2) = Real.exp 1 := by rw [← Real.exp_add]; norm_num
+    have h1 : Real.exp 1 < 2.7182818286 := Real.exp_one_lt_d9
+    have hexp12 : Real.exp (1/2) < 1.6489 := by nlinarith [hehalf, h1, Real.exp_pos (1/2 : ℝ)]
+    have hpos : (0:ℝ) < Real.exp (1/2) := Real.exp_pos _
+    have hinvcancel : (Real.exp (1/2))⁻¹ * Real.exp (1/2) = 1 := inv_mul_cancel₀ (ne_of_gt hpos)
+    have hinvpos : (0:ℝ) < (Real.exp (1/2))⁻¹ := inv_pos.mpr hpos
+    nlinarith [hexp12, hpos, hinvcancel, hinvpos]
+  nlinarith [hcomb, hval]
+
+/-- d=2 decouple residual `R(S) ≤ 0` on `S ∈ [0, 1/2]`, `μ ∈ I`.  `μ'' = muPP 2 μ = 3(7−3μ)/49`;
+    `R(S) = μ''/3 − μ/3 − 1/7 + log(7/6) − F* + 9μS/49 + μ/(2+S)`.  The log part `≤ −1/22` (`log76_gap`);
+    the rational part `≤ 1/22` after clearing `(2+S) > 0` (upward parabola, margin `+0.0002`). -/
+theorem decouple_d2 (μ S : ℝ) (hμ : inI μ) (hS0 : 0 ≤ S) (hSmax : S ≤ 1/2) :
+    (muPP 2 μ)/3 - μ/3 - 1/7 + Real.log (7/6) - FSTAR + 9*μ*S/49 + μ/(2+S) ≤ 0 := by
+  obtain ⟨hμlo, hμhi⟩ := hμ
+  have hmuPP : muPP 2 μ = 3*(7 - 3*μ)/49 := by rw [muPP]; norm_num
+  have hg := log76_gap
+  have h2S : (0:ℝ) < 2 + S := by linarith
+  have hμpos : 0 ≤ μ := by linarith
+  rw [hmuPP, div_eq_mul_inv μ (2+S)]
+  have hinv : (2+S)⁻¹ * (2+S) = 1 := inv_mul_cancel₀ (ne_of_gt h2S)
+  have hinvpos : 0 < (2+S)⁻¹ := inv_pos.mpr h2S
+  nlinarith [hg, hμlo, hμhi, hS0, hSmax, h2S, hinv, hinvpos, mul_nonneg hμpos (le_of_lt hinvpos),
+    mul_nonneg hμpos hS0, mul_nonneg (mul_nonneg hμpos hS0) (le_of_lt hinvpos),
+    mul_nonneg (mul_nonneg hμpos (le_of_lt hinvpos)) hS0]
+
+/-- d=3 log gap: `log(3/2) + log(11/9) - 3 F* ≤ 0` (the combined `log(X_3)` with `X_3 = (3/2)^11·(11/9)^11·(64/621)^3 < 1`). -/
+theorem log_gap_d3 : Real.log (3/2) + Real.log (11/9) - 3*FSTAR ≤ 0 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(Real.log (3/2) + Real.log (11/9) - 3*(Real.log (621/64)/11))
+      = Real.log ((3/2)^11 * (11/9)^11 * (64/621)^3) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^11 * (11/9)^11 * (64/621)^3) ≤ 0 :=
+    Real.log_nonpos (by positivity) (by norm_num)
+  nlinarith [hcomb, hX]
+
+/-- d=3 decouple residual `R(S) ≤ 0` on `S ∈ [0,2]`, `μ ∈ I`.  `μ'' = muPP 3 μ = 3(11−3μ)/121`. -/
+theorem decouple_d3 (μ S : ℝ) (hμ : inI μ) (hS0 : 0 ≤ S) (hSmax : S ≤ 2) :
+    2*(muPP 3 μ)/3 - μ/3 + 9*μ*S/121 - 2/11 + (Real.log (3/2) + Real.log (11/9) - 3*FSTAR) + μ/(3+S) ≤ 0 := by
+  obtain ⟨hμlo, hμhi⟩ := hμ
+  have hmuPP : muPP 3 μ = 3*(11 - 3*μ)/121 := by rw [muPP]; norm_num
+  have hg := log_gap_d3
+  have h3S : (0:ℝ) < 3 + S := by linarith
+  have hμpos : 0 ≤ μ := by linarith
+  rw [hmuPP, div_eq_mul_inv μ (3+S)]
+  have hinv : (3+S)⁻¹ * (3+S) = 1 := inv_mul_cancel₀ (ne_of_gt h3S)
+  have hinvpos : 0 < (3+S)⁻¹ := inv_pos.mpr h3S
+  nlinarith [hg, hμlo, hμhi, hS0, hSmax, h3S, hinv, hinvpos, mul_nonneg hμpos (le_of_lt hinvpos),
+    mul_nonneg hμpos hS0, mul_nonneg (mul_nonneg hμpos hS0) (le_of_lt hinvpos),
+    mul_nonneg (mul_nonneg hμpos (le_of_lt hinvpos)) hS0]
+
+/-- d=4 log gap: `2·log(3/2) + log(5/4) - 5 F* ≤ 1334065663/1159983480832`. -/
+theorem log_gap_d4 : 2*Real.log (3/2) + Real.log (5/4) - 5*FSTAR ≤ 1334065663/1159983480832 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(2*Real.log (3/2) + Real.log (5/4) - 5*(Real.log (621/64)/11))
+      = Real.log ((3/2)^22 * (5/4)^11 * (64/621)^5) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^22 * (5/4)^11 * (64/621)^5)
+      ≤ (3/2)^22 * (5/4)^11 * (64/621)^5 - 1 :=
+    Real.log_le_sub_one_of_pos (by positivity)
+  have hXval : (3/2)^22 * (5/4)^11 * (64/621)^5 - 1 = 1334065663/105453043712 := by norm_num
+  nlinarith [hcomb, hX, hXval]
+
+/-- d=4 decouple residual `R(S) ≤ 0` on `S ∈ [0,3]`, `μ ∈ I`.  `μ'' = muPP 4 μ = 3(15−3μ)/225`. -/
+theorem decouple_d4 (μ S : ℝ) (hμ : inI μ) (hS0 : 0 ≤ S) (hSmax : S ≤ 3) :
+    (1*(muPP 4 μ)/1) - μ/3 + 1*μ*S/16 - (1/4) + (2*Real.log (3/2) + Real.log (5/4) - 5*FSTAR) + μ/(4+S) ≤ 0 := by
+  obtain ⟨hμlo, hμhi⟩ := hμ
+  have hmuPP : muPP 4 μ = 3*(15 - 3*μ)/225 := by rw [muPP]; norm_num
+  have hg := log_gap_d4
+  have hdS : (0:ℝ) < 4 + S := by linarith
+  have hμpos : 0 ≤ μ := by linarith
+  rw [hmuPP, div_eq_mul_inv μ (4+S)]
+  have hinv : (4+S)⁻¹ * (4+S) = 1 := inv_mul_cancel₀ (ne_of_gt hdS)
+  have hinvpos : 0 < (4+S)⁻¹ := inv_pos.mpr hdS
+  nlinarith [hg, hμlo, hμhi, hS0, hSmax, hdS, hinv, hinvpos, mul_nonneg hμpos (le_of_lt hinvpos),
+    mul_nonneg hμpos hS0, mul_nonneg (mul_nonneg hμpos hS0) (le_of_lt hinvpos),
+    mul_nonneg (mul_nonneg hμpos (le_of_lt hinvpos)) hS0]
+
+
+/-- d=5 log gap: `3·log(3/2) + log(19/15) - 7 F* ≤ 12677795138367509/1828763667822265625`. -/
+theorem log_gap_d5 : 3*Real.log (3/2) + Real.log (19/15) - 7*FSTAR ≤ 12677795138367509/1828763667822265625 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(3*Real.log (3/2) + Real.log (19/15) - 7*(Real.log (621/64)/11))
+      = Real.log ((3/2)^33 * (19/15)^11 * (64/621)^7) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^33 * (19/15)^11 * (64/621)^7)
+      ≤ (3/2)^33 * (19/15)^11 * (64/621)^7 - 1 :=
+    Real.log_le_sub_one_of_pos (by positivity)
+  have hXval : (3/2)^33 * (19/15)^11 * (64/621)^7 - 1 = 12677795138367509/166251242529296875 := by norm_num
+  nlinarith [hcomb, hX, hXval]
+
+/-- d=5 decouple residual `R(S) ≤ 0` on `S ∈ [0,4]`, `μ ∈ I`.  `μ'' = muPP 5 μ = 3(19−3μ)/361`. -/
+theorem decouple_d5 (μ S : ℝ) (hμ : inI μ) (hS0 : 0 ≤ S) (hSmax : S ≤ 4) :
+    (4*(muPP 5 μ)/3) - μ/3 + 9*μ*S/361 - (4/19) + (3*Real.log (3/2) + Real.log (19/15) - 7*FSTAR) + μ/(5+S) ≤ 0 := by
+  obtain ⟨hμlo, hμhi⟩ := hμ
+  have hmuPP : muPP 5 μ = 3*(19 - 3*μ)/361 := by rw [muPP]; norm_num
+  have hg := log_gap_d5
+  have hdS : (0:ℝ) < 5 + S := by linarith
+  have hμpos : 0 ≤ μ := by linarith
+  rw [hmuPP, div_eq_mul_inv μ (5+S)]
+  have hinv : (5+S)⁻¹ * (5+S) = 1 := inv_mul_cancel₀ (ne_of_gt hdS)
+  have hinvpos : 0 < (5+S)⁻¹ := inv_pos.mpr hdS
+  nlinarith [hg, hμlo, hμhi, hS0, hSmax, hdS, hinv, hinvpos, mul_nonneg hμpos (le_of_lt hinvpos),
+    mul_nonneg hμpos hS0, mul_nonneg (mul_nonneg hμpos hS0) (le_of_lt hinvpos),
+    mul_nonneg (mul_nonneg hμpos (le_of_lt hinvpos)) hS0]
+
+
+/-- d=6 log gap: `4·log(3/2) + log(23/18) - 9 F* ≤ 43/5346`. -/
+theorem log_gap_d6 : 4*Real.log (3/2) + Real.log (23/18) - 9*FSTAR ≤ 43/5346 := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(4*Real.log (3/2) + Real.log (23/18) - 9*(Real.log (621/64)/11))
+      = Real.log ((3/2)^44 * (23/18)^11 * (64/621)^9) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_mul (by positivity) (by positivity),
+        Real.log_pow, Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hX : Real.log ((3/2)^44 * (23/18)^11 * (64/621)^9)
+      ≤ (3/2)^44 * (23/18)^11 * (64/621)^9 - 1 :=
+    Real.log_le_sub_one_of_pos (by positivity)
+  have hXval : (3/2)^44 * (23/18)^11 * (64/621)^9 - 1 = 43/486 := by norm_num
+  nlinarith [hcomb, hX, hXval]
+
+/-- d=6 decouple residual `R(S) ≤ 0` on `S ∈ [0,5]`, `μ ∈ I`.  `μ'' = muPP 6 μ = 3(23−3μ)/529`. -/
+theorem decouple_d6 (μ S : ℝ) (hμ : inI μ) (hS0 : 0 ≤ S) (hSmax : S ≤ 5) :
+    (5*(muPP 6 μ)/3) - μ/3 + 9*μ*S/529 - (5/23) + (4*Real.log (3/2) + Real.log (23/18) - 9*FSTAR) + μ/(6+S) ≤ 0 := by
+  obtain ⟨hμlo, hμhi⟩ := hμ
+  have hmuPP : muPP 6 μ = 3*(23 - 3*μ)/529 := by rw [muPP]; norm_num
+  have hg := log_gap_d6
+  have hdS : (0:ℝ) < 6 + S := by linarith
+  have hμpos : 0 ≤ μ := by linarith
+  rw [hmuPP, div_eq_mul_inv μ (6+S)]
+  have hinv : (6+S)⁻¹ * (6+S) = 1 := inv_mul_cancel₀ (ne_of_gt hdS)
+  have hinvpos : 0 < (6+S)⁻¹ := inv_pos.mpr hdS
+  nlinarith [hg, hμlo, hμhi, hS0, hSmax, hdS, hinv, hinvpos, mul_nonneg hμpos (le_of_lt hinvpos),
+    mul_nonneg hμpos hS0, mul_nonneg (mul_nonneg hμpos hS0) (le_of_lt hinvpos),
+    mul_nonneg (mul_nonneg hμpos (le_of_lt hinvpos)) hS0]
+
+end BGSCL
+end R3Cert
diff --git a/proof/formalization/R3Cert/BGSCLHub.lean b/proof/formalization/R3Cert/BGSCLHub.lean
new file mode 100644
index 00000000..ed56dce3
--- /dev/null
+++ b/proof/formalization/R3Cert/BGSCLHub.lean
@@ -0,0 +1,448 @@
+/-
+  SCL FlowedHubStep assembly — the list machinery + tangent connection tying the per-degree decouple
+  residuals (`BGSCLDecouple`) to the actual hub `node cs`.
+  `child_bell_sum_le`: from the per-child SCL at a price `ν`, the sum bound `Σ bell(c) ≤ |cs|·bV_ν(cherry) − ν·S`.
+  This feeds `bell_node_tangent` + `bY_node` + `decouple_d` to give `bV μ (node cs) ≤ bV μ cherry` for d≤6.
+  (d≥7 needs the branch ceiling `bell (node cs) ≤ 0`, a separate result not yet in the SCL Lean.)
+  conjecture1_proved = False.
+-/
+import Mathlib
+import R3Cert.BGSCLInduction
+import R3Cert.BGSCLStep
+import R3Cert.BGSCLDecouple
+import R3Cert.BGSCLFlowed
+
+namespace R3Cert
+namespace BGSCL
+
+/-- **The child-sum bound.**  If every child `c ∈ cs` satisfies the SCL at price `ν`
+    (`bV ν c ≤ bV ν cherry`), then `Σ_c bell(c) ≤ |cs|·bV_ν(cherry) − ν·Σ_c bY(c)`.  (Since
+    `bell c = bV ν c − ν·bY c ≤ bV ν cherry − ν·bY c`, summed.)  This is the list-machinery half of the
+    per-hub decouple: it converts the per-child hypotheses into the single scalar `Σ bell` bound the
+    tangent needs. -/
+theorem child_bell_sum_le (ν : ℝ) (cs : List Branch) (h : ∀ c ∈ cs, bV ν c ≤ bV ν cherry) :
+    (cs.map bell).sum ≤ (cs.length : ℝ) * bV ν cherry - ν * (cs.map bY).sum := by
+  induction cs with
+  | nil => simp
+  | cons a t ih =>
+    have ha : bell a + ν * bY a ≤ bell cherry + ν * bY cherry := by
+      have h1 : bV ν a = bell a + ν * bY a := rfl
+      have h2 : bV ν cherry = bell cherry + ν * bY cherry := rfl
+      have := h a (List.mem_cons.mpr (Or.inl rfl)); rw [h1, h2] at this; exact this
+    have iht : (t.map bell).sum ≤ (t.length : ℝ) * bV ν cherry - ν * (t.map bY).sum :=
+      ih (fun c hc => h c (List.mem_cons.mpr (Or.inr hc)))
+    have hVc : bV ν cherry = bell cherry + ν * bY cherry := rfl
+    simp only [List.map_cons, List.sum_cons, List.length_cons, Nat.cast_add, Nat.cast_one]
+    rw [hVc] at iht ⊢
+    nlinarith [ha, iht]
+
+/-- `bY b ≤ 1` for every branch (`h ≤ 1`, `bcc ≥ 0`). -/
+theorem bY_le_one (b : Branch) : bY b ≤ 1 := by
+  cases b with
+  | node cs =>
+    rw [bY_node]
+    have hS : 0 ≤ (cs.map bY).sum := by
+      apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+      obtain ⟨c, _, rfl⟩ := hx; exact bY_nonneg c
+    have hlen : (0:ℝ) ≤ (cs.length:ℝ) := Nat.cast_nonneg _
+    rw [div_le_one (by linarith)]; linarith
+
+/-- A non-leaf branch `node (a :: rest)` has `bY ≤ 1/2` (denominator `≥ 2`). -/
+theorem bY_nonleaf_le_half (a : Branch) (rest : List Branch) :
+    bY (Branch.node (a :: rest)) ≤ 1/2 := by
+  rw [bY_node]
+  have hS : 0 ≤ ((a :: rest).map bY).sum := by
+    apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨c, _, rfl⟩ := hx; exact bY_nonneg c
+  have h1 : (1:ℝ) ≤ ((a :: rest).length : ℝ) := by
+    have : (0:ℝ) ≤ (rest.length : ℝ) := Nat.cast_nonneg _
+    rw [List.length_cons]; push_cast; linarith
+  rw [div_le_iff₀ (by linarith)]
+  linarith
+
+/-- **Uniform child SCL at the flowed price** (`d ∈ {3..6}`): every child satisfies `bV_{μ''} c ≤ bV_{μ''} cherry`
+    — leaf children via `leaf_le_cherry` (`μ'' ≤ 3/11`), non-leaf via `PSCLne` at `μ'' ∈ I`. -/
+theorem child_scl_muPP {d : ℝ} (hd3 : 3 ≤ d) (hd6 : d ≤ 6) {μ : ℝ} (hμ : inI μ)
+    {cs : List Branch} (hchild : ∀ c ∈ cs, PSCLne c) :
+    ∀ c ∈ cs, bV (muPP d μ) c ≤ bV (muPP d μ) cherry := by
+  intro c hc
+  have hμ0 : (0:ℝ) ≤ μ := le_trans (by norm_num) hμ.1
+  by_cases hleaf : c = Branch.node []
+  · subst hleaf
+    exact leaf_le_cherry (muPP_le_three_eleven hd3 hμ0)
+  · exact hchild c hc hleaf (muPP d μ) (muPP_mem_I (by linarith) hd6 hμ)
+
+/-- `Σ_c bY(c) ≤ |cs|` (each `bY ≤ 1`). -/
+theorem sum_bY_le_length (cs : List Branch) : (cs.map bY).sum ≤ (cs.length : ℝ) := by
+  induction cs with
+  | nil => simp
+  | cons a t ih =>
+    simp only [List.map_cons, List.sum_cons, List.length_cons, Nat.cast_add, Nat.cast_one]
+    have := bY_le_one a
+    linarith [ih]
+
+/-- **Hub connection, d=3** (`cs.length = 2`). -/
+theorem hub_le_d3 {mu : ℝ} (hmu : inI mu) {cs : List Branch} (hlen : cs.length = 2)
+    (hchild : ∀ c ∈ cs, PSCLne c) :
+    bV mu (Branch.node cs) ≤ bV mu cherry := by
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨c, _, rfl⟩ := hx; exact bY_nonneg c
+  have hlenR : (cs.length : ℝ) = 2 := by exact_mod_cast hlen
+  have hSle : S ≤ 2 := by
+    have := sum_bY_le_length cs; rw [hlenR] at this; rw [hSdef]; exact this
+  have hmpp : muPP 3 mu = (33 - 9*mu)/121 := by rw [muPP]; ring
+  have hchild2 := child_scl_muPP (d:=3) (by norm_num) (by norm_num) hmu hchild
+  have hsum : (cs.map bell).sum ≤ (cs.length : ℝ) * bV (muPP 3 mu) cherry - muPP 3 mu * (cs.map bY).sum :=
+    child_bell_sum_le (muPP 3 mu) cs hchild2
+  rw [hlenR, ← hSdef] at hsum
+  have htan := bell_node_tangent cs (s0 := 2/3) (by norm_num)
+  rw [hlenR, ← hSdef] at htan
+  have hlogeq : Real.log (1 + 2/3/((2:ℝ)+1)) = Real.log (11/9) := by norm_num
+  have hden : ((2:ℝ)+1)+2/3 = 11/3 := by norm_num
+  rw [hlogeq, hden] at htan
+  have hbY : bY (Branch.node cs) = 1 / (3 + S) := by
+    have hden' : ((cs.length : ℝ) + 1) + (cs.map bY).sum = 3 + S := by rw [hlenR, ← hSdef]; ring
+    rw [bY_node, hden']
+  have hdec := decouple_d3 mu S hmu hSnn hSle
+  have hVpp : bV (muPP 3 mu) cherry = Real.log (3/2) - 2*FSTAR + muPP 3 mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  have hVc : bV mu cherry = Real.log (3/2) - 2*FSTAR + mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  -- the RHS bound on bV mu (node cs)
+  have hbV : bV mu (Branch.node cs) = bell (Branch.node cs) + mu * (1/(3+S)) := by rw [bV, hbY]
+  have hRHS : bV mu (Branch.node cs)
+      ≤ (2 * bV (muPP 3 mu) cherry - muPP 3 mu * S
+          + (Real.log (11/9) + (S - 2/3)/(11/3) - FSTAR)) + mu * (1/(3+S)) := by
+    rw [hbV]; linarith [htan, hsum]
+  -- the algebraic identity: RHS - bV mu cherry = decouple_d3 LHS  (μ'' expanded, μ/(3+S) shared atom)
+  have hbridge : (2 * bV (muPP 3 mu) cherry - muPP 3 mu * S
+        + (Real.log (11/9) + (S - 2/3)/(11/3) - FSTAR)) + mu * (1/(3+S)) - bV mu cherry
+      = (2*(muPP 3 mu)/3 - mu/3 + 9*mu*S/121 - 2/11
+          + (Real.log (3/2) + Real.log (11/9) - 3*FSTAR) + mu/(3+S)) := by
+    rw [hVpp, hVc, hmpp]; ring
+  linarith [hRHS, hbridge, hdec]
+
+/-- **Hub connection, d=4** (`cs.length = 3`). -/
+theorem hub_le_d4 {mu : ℝ} (hmu : inI mu) {cs : List Branch} (hlen : cs.length = 3)
+    (hchild : ∀ c ∈ cs, PSCLne c) :
+    bV mu (Branch.node cs) ≤ bV mu cherry := by
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨c, _, rfl⟩ := hx; exact bY_nonneg c
+  have hlenR : (cs.length : ℝ) = 3 := by exact_mod_cast hlen
+  have hSle : S ≤ 3 := by
+    have := sum_bY_le_length cs; rw [hlenR] at this; rw [hSdef]; exact this
+  have hmpp : muPP 4 mu = 3*(15 - 3*mu)/225 := by rw [muPP]; norm_num
+  have hchild2 := child_scl_muPP (d:=4) (by norm_num) (by norm_num) hmu hchild
+  have hsum : (cs.map bell).sum ≤ (cs.length : ℝ) * bV (muPP 4 mu) cherry - muPP 4 mu * (cs.map bY).sum :=
+    child_bell_sum_le (muPP 4 mu) cs hchild2
+  rw [hlenR, ← hSdef] at hsum
+  have htan := bell_node_tangent cs (s0 := 1) (by norm_num)
+  rw [hlenR, ← hSdef] at htan
+  have hlogeq : Real.log (1 + 1/((3:ℝ)+1)) = Real.log (5/4) := by norm_num
+  have hden : ((3:ℝ)+1)+1 = 5 := by norm_num
+  rw [hlogeq, hden] at htan
+  have hbY : bY (Branch.node cs) = 1 / (4 + S) := by
+    have hden' : ((cs.length : ℝ) + 1) + (cs.map bY).sum = 4 + S := by rw [hlenR, ← hSdef]; ring
+    rw [bY_node, hden']
+  -- d=4's pre-existing decouple lemma uses a non-uniform normalization; prove the UNIFORM
+  -- residual (matching the clean tangent) inline via the same log gap.
+  have hdS : (0:ℝ) < 4 + S := by linarith
+  have hμpos : (0:ℝ) ≤ mu := le_trans (by norm_num) hmu.1
+  have hdec : (muPP 4 mu) - mu/3 + 9*mu*S/225 - (3/15)
+      + (2*Real.log (3/2) + Real.log (5/4) - 5*FSTAR) + mu/(4+S) ≤ 0 := by
+    obtain ⟨hμlo, hμhi⟩ := hmu
+    have hg := log_gap_d4
+    rw [hmpp, div_eq_mul_inv mu (4+S)]
+    have hinv : (4+S)⁻¹ * (4+S) = 1 := inv_mul_cancel₀ (ne_of_gt hdS)
+    have hinvpos : 0 < (4+S)⁻¹ := inv_pos.mpr hdS
+    nlinarith [hg, hμlo, hμhi, hSnn, hSle, hdS, hinv, hinvpos, mul_nonneg hμpos (le_of_lt hinvpos),
+      mul_nonneg hμpos hSnn, mul_nonneg (mul_nonneg hμpos hSnn) (le_of_lt hinvpos),
+      mul_nonneg (mul_nonneg hμpos (le_of_lt hinvpos)) hSnn]
+  have hVpp : bV (muPP 4 mu) cherry = Real.log (3/2) - 2*FSTAR + muPP 4 mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  have hVc : bV mu cherry = Real.log (3/2) - 2*FSTAR + mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  have hbV : bV mu (Branch.node cs) = bell (Branch.node cs) + mu * (1/(4+S)) := by rw [bV, hbY]
+  have hRHS : bV mu (Branch.node cs)
+      ≤ ((3:ℝ) * bV (muPP 4 mu) cherry - muPP 4 mu * S
+          + (Real.log (5/4) + (S - 1)/5 - FSTAR)) + mu * (1/(4+S)) := by
+    rw [hbV]; linarith [htan, hsum]
+  have hbridge : ((3:ℝ) * bV (muPP 4 mu) cherry - muPP 4 mu * S
+        + (Real.log (5/4) + (S - 1)/5 - FSTAR)) + mu * (1/(4+S)) - bV mu cherry
+      = ((muPP 4 mu) - mu/3 + 9*mu*S/225 - (3/15)
+          + (2*Real.log (3/2) + Real.log (5/4) - 5*FSTAR) + mu/(4+S)) := by
+    rw [hVpp, hVc, hmpp]; ring
+  linarith [hRHS, hbridge, hdec]
+
+/-- **Hub connection, d=5** (`cs.length = 4`). -/
+theorem hub_le_d5 {mu : ℝ} (hmu : inI mu) {cs : List Branch} (hlen : cs.length = 4)
+    (hchild : ∀ c ∈ cs, PSCLne c) :
+    bV mu (Branch.node cs) ≤ bV mu cherry := by
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨c, _, rfl⟩ := hx; exact bY_nonneg c
+  have hlenR : (cs.length : ℝ) = 4 := by exact_mod_cast hlen
+  have hSle : S ≤ 4 := by
+    have := sum_bY_le_length cs; rw [hlenR] at this; rw [hSdef]; exact this
+  have hmpp : muPP 5 mu = 3*(19 - 3*mu)/361 := by rw [muPP]; norm_num
+  have hchild2 := child_scl_muPP (d:=5) (by norm_num) (by norm_num) hmu hchild
+  have hsum : (cs.map bell).sum ≤ (cs.length : ℝ) * bV (muPP 5 mu) cherry - muPP 5 mu * (cs.map bY).sum :=
+    child_bell_sum_le (muPP 5 mu) cs hchild2
+  rw [hlenR, ← hSdef] at hsum
+  have htan := bell_node_tangent cs (s0 := 4/3) (by norm_num)
+  rw [hlenR, ← hSdef] at htan
+  have hlogeq : Real.log (1 + 4/3/((4:ℝ)+1)) = Real.log (19/15) := by norm_num
+  have hden : ((4:ℝ)+1)+4/3 = 19/3 := by norm_num
+  rw [hlogeq, hden] at htan
+  have hbY : bY (Branch.node cs) = 1 / (5 + S) := by
+    have hden' : ((cs.length : ℝ) + 1) + (cs.map bY).sum = 5 + S := by rw [hlenR, ← hSdef]; ring
+    rw [bY_node, hden']
+  have hdec := decouple_d5 mu S hmu hSnn hSle
+  have hVpp : bV (muPP 5 mu) cherry = Real.log (3/2) - 2*FSTAR + muPP 5 mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  have hVc : bV mu cherry = Real.log (3/2) - 2*FSTAR + mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  have hbV : bV mu (Branch.node cs) = bell (Branch.node cs) + mu * (1/(5+S)) := by rw [bV, hbY]
+  have hRHS : bV mu (Branch.node cs)
+      ≤ ((4:ℝ) * bV (muPP 5 mu) cherry - muPP 5 mu * S
+          + (Real.log (19/15) + (S - 4/3)/(19/3) - FSTAR)) + mu * (1/(5+S)) := by
+    rw [hbV]; linarith [htan, hsum]
+  have hbridge : ((4:ℝ) * bV (muPP 5 mu) cherry - muPP 5 mu * S
+        + (Real.log (19/15) + (S - 4/3)/(19/3) - FSTAR)) + mu * (1/(5+S)) - bV mu cherry
+      = ((4*(muPP 5 mu)/3) - mu/3 + 9*mu*S/361 - (4/19)
+          + (3*Real.log (3/2) + Real.log (19/15) - 7*FSTAR) + mu/(5+S)) := by
+    rw [hVpp, hVc, hmpp]; ring
+  linarith [hRHS, hbridge, hdec]
+
+/-- **Hub connection, d=6** (`cs.length = 5`). -/
+theorem hub_le_d6 {mu : ℝ} (hmu : inI mu) {cs : List Branch} (hlen : cs.length = 5)
+    (hchild : ∀ c ∈ cs, PSCLne c) :
+    bV mu (Branch.node cs) ≤ bV mu cherry := by
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨c, _, rfl⟩ := hx; exact bY_nonneg c
+  have hlenR : (cs.length : ℝ) = 5 := by exact_mod_cast hlen
+  have hSle : S ≤ 5 := by
+    have := sum_bY_le_length cs; rw [hlenR] at this; rw [hSdef]; exact this
+  have hmpp : muPP 6 mu = 3*(23 - 3*mu)/529 := by rw [muPP]; norm_num
+  have hchild2 := child_scl_muPP (d:=6) (by norm_num) (by norm_num) hmu hchild
+  have hsum : (cs.map bell).sum ≤ (cs.length : ℝ) * bV (muPP 6 mu) cherry - muPP 6 mu * (cs.map bY).sum :=
+    child_bell_sum_le (muPP 6 mu) cs hchild2
+  rw [hlenR, ← hSdef] at hsum
+  have htan := bell_node_tangent cs (s0 := 5/3) (by norm_num)
+  rw [hlenR, ← hSdef] at htan
+  have hlogeq : Real.log (1 + 5/3/((5:ℝ)+1)) = Real.log (23/18) := by norm_num
+  have hden : ((5:ℝ)+1)+5/3 = 23/3 := by norm_num
+  rw [hlogeq, hden] at htan
+  have hbY : bY (Branch.node cs) = 1 / (6 + S) := by
+    have hden' : ((cs.length : ℝ) + 1) + (cs.map bY).sum = 6 + S := by rw [hlenR, ← hSdef]; ring
+    rw [bY_node, hden']
+  have hdec := decouple_d6 mu S hmu hSnn hSle
+  have hVpp : bV (muPP 6 mu) cherry = Real.log (3/2) - 2*FSTAR + muPP 6 mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  have hVc : bV mu cherry = Real.log (3/2) - 2*FSTAR + mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  have hbV : bV mu (Branch.node cs) = bell (Branch.node cs) + mu * (1/(6+S)) := by rw [bV, hbY]
+  have hRHS : bV mu (Branch.node cs)
+      ≤ ((5:ℝ) * bV (muPP 6 mu) cherry - muPP 6 mu * S
+          + (Real.log (23/18) + (S - 5/3)/(23/3) - FSTAR)) + mu * (1/(6+S)) := by
+    rw [hbV]; linarith [htan, hsum]
+  have hbridge : ((5:ℝ) * bV (muPP 6 mu) cherry - muPP 6 mu * S
+        + (Real.log (23/18) + (S - 5/3)/(23/3) - FSTAR)) + mu * (1/(6+S)) - bV mu cherry
+      = ((5*(muPP 6 mu)/3) - mu/3 + 9*mu*S/529 - (5/23)
+          + (4*Real.log (3/2) + Real.log (23/18) - 9*FSTAR) + mu/(6+S)) := by
+    rw [hVpp, hVc, hmpp]; ring
+  linarith [hRHS, hbridge, hdec]
+
+/-- **Hub connection, d=2** (`cs.length = 1`, single child).  Special: a LEAF child makes the hub
+    `node [node []] = cherry` exactly (trivial equality); a NON-leaf child has `bY ≤ 1/2` (`S ≤ 1/2`),
+    so `decouple_d2` applies with the child IH at `μ'' = muPP 2 μ ∈ I`. -/
+theorem hub_le_d2 {mu : ℝ} (hmu : inI mu) {cs : List Branch} (hlen : cs.length = 1)
+    (hchild : ∀ c ∈ cs, PSCLne c) :
+    bV mu (Branch.node cs) ≤ bV mu cherry := by
+  obtain ⟨c, rfl⟩ : ∃ c, cs = [c] := by
+    cases cs with
+    | nil => simp at hlen
+    | cons c t => cases t with
+      | nil => exact ⟨c, rfl⟩
+      | cons _ _ => simp at hlen
+  have hc1 : PSCLne c := hchild c (List.mem_cons.mpr (Or.inl rfl))
+  by_cases hc : c = Branch.node []
+  · subst hc; exact le_of_eq rfl
+  · set S := (([c] : List Branch).map bY).sum with hSdef
+    have hSnn : 0 ≤ S := by
+      rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+      obtain ⟨z, _, rfl⟩ := hx; exact bY_nonneg z
+    have hScc : S = bY c := by rw [hSdef]; simp
+    have hSle : S ≤ 1/2 := by
+      rw [hScc]
+      cases c with
+      | node cs' => cases cs' with
+        | nil => exact absurd rfl hc
+        | cons a rest => exact bY_nonleaf_le_half a rest
+    have hlenR : (([c] : List Branch).length : ℝ) = 1 := by norm_num
+    have hmpp : muPP 2 mu = 3*(7 - 3*mu)/49 := by rw [muPP]; norm_num
+    have hchild2 : ∀ x ∈ ([c] : List Branch), bV (muPP 2 mu) x ≤ bV (muPP 2 mu) cherry := by
+      intro x hx
+      rw [List.mem_singleton] at hx; subst hx
+      exact hc1 hc (muPP 2 mu) (muPP_mem_I (by norm_num) (by norm_num) hmu)
+    have hsum : (([c] : List Branch).map bell).sum
+        ≤ (([c] : List Branch).length : ℝ) * bV (muPP 2 mu) cherry - muPP 2 mu * (([c] : List Branch).map bY).sum :=
+      child_bell_sum_le (muPP 2 mu) [c] hchild2
+    rw [hlenR, ← hSdef] at hsum
+    have htan := bell_node_tangent [c] (s0 := 1/3) (by norm_num)
+    rw [hlenR, ← hSdef] at htan
+    have hlogeq : Real.log (1 + 1/3/((1:ℝ)+1)) = Real.log (7/6) := by norm_num
+    have hden : ((1:ℝ)+1)+1/3 = 7/3 := by norm_num
+    rw [hlogeq, hden] at htan
+    have hbY : bY (Branch.node [c]) = 1 / (2 + S) := by
+      have hden' : (([c] : List Branch).length : ℝ) + 1 + (([c] : List Branch).map bY).sum = 2 + S := by
+        rw [hlenR, ← hSdef]; ring
+      rw [bY_node, hden']
+    have hdec := decouple_d2 mu S hmu hSnn hSle
+    have hVpp : bV (muPP 2 mu) cherry = Real.log (3/2) - 2*FSTAR + muPP 2 mu * (1/3) := by
+      rw [bV, bell_cherry, bY_cherry]
+    have hVc : bV mu cherry = Real.log (3/2) - 2*FSTAR + mu * (1/3) := by
+      rw [bV, bell_cherry, bY_cherry]
+    have hbV : bV mu (Branch.node [c]) = bell (Branch.node [c]) + mu * (1/(2+S)) := by rw [bV, hbY]
+    have hRHS : bV mu (Branch.node [c])
+        ≤ ((1:ℝ) * bV (muPP 2 mu) cherry - muPP 2 mu * S
+            + (Real.log (7/6) + (S - 1/3)/(7/3) - FSTAR)) + mu * (1/(2+S)) := by
+      rw [hbV]; linarith [htan, hsum]
+    have hbridge : ((1:ℝ) * bV (muPP 2 mu) cherry - muPP 2 mu * S
+          + (Real.log (7/6) + (S - 1/3)/(7/3) - FSTAR)) + mu * (1/(2+S)) - bV mu cherry
+        = ((muPP 2 mu)/3 - mu/3 - 1/7 + Real.log (7/6) - FSTAR + 9*mu*S/49 + mu/(2+S)) := by
+      rw [hVpp, hVc, hmpp]; ring
+    linarith [hRHS, hbridge, hdec]
+
+/-- **The cherry ceiling gap** `log(3/2) − 2 F* ≥ −1/50`.  (True value `≈ −0.00768`; margin `+0.012`.)
+    `two_le_log_gap` is too loose here (`≥ −0.0248`), so combine `11·(log(3/2) − 2F*) = log(354294/385641)`
+    and lower-bound via `log x ≥ 1 − 1/x` (`Real.log_le_sub_one_of_pos` on the inverse). -/
+theorem cherry_ceiling_gap : (-1/50 : ℝ) ≤ Real.log (3/2) - 2*FSTAR := by
+  have hF : FSTAR = Real.log (621/64)/11 := rfl
+  rw [hF]
+  have hcomb : (11:ℝ)*(Real.log (3/2) - 2*(Real.log (621/64)/11))
+      = Real.log ((3/2)^11 * (64/621)^2) := by
+    rw [Real.log_mul (by positivity) (by positivity), Real.log_pow, Real.log_pow,
+        show (64:ℝ)/621 = (621/64)⁻¹ by norm_num, Real.log_inv]
+    ring
+  have hXval : ((3/2:ℝ))^11 * (64/621)^2 = 354294/385641 := by norm_num
+  have hXpos : (0:ℝ) < ((3/2:ℝ))^11 * (64/621)^2 := by positivity
+  have hle := Real.log_le_sub_one_of_pos (inv_pos.mpr hXpos)
+  rw [Real.log_inv] at hle
+  rw [hXval] at hcomb hle
+  have hinvval : ((354294:ℝ)/385641)⁻¹ = 385641/354294 := by norm_num
+  rw [hinvval] at hle
+  linarith [hcomb, hle]
+
+/-- **Hub connection, d≥7 ceiling** (`cs.length ≥ 6`).  For a high-degree hub the tangent decouple is loose;
+    instead `bV μ (node cs) = bell(node cs) + μ·bY ≤ 0 + μ/7 ≤ bV μ cherry`, using the branch ceiling
+    `bell (node cs) ≤ 0` (hypothesis; the separate not-yet-formalized result) and `bY ≤ 1/7`.  The cherry
+    lower bound `μ/7 ≤ bV μ cherry` follows from `cherry_ceiling_gap` + `μ ≥ 456/3703` (`4μ/21 ≥ 1/50`). -/
+theorem hub_le_highdeg {mu : ℝ} (hmu : inI mu) {cs : List Branch} (hd7 : 6 ≤ cs.length)
+    (hceil : bell (Branch.node cs) ≤ 0) :
+    bV mu (Branch.node cs) ≤ bV mu cherry := by
+  have hμpos : (0:ℝ) ≤ mu := le_trans (by norm_num) hmu.1
+  obtain ⟨hμlo, hμhi⟩ := hmu
+  set S := (cs.map bY).sum with hSdef
+  have hSnn : 0 ≤ S := by
+    rw [hSdef]; apply List.sum_nonneg; intro x hx; rw [List.mem_map] at hx
+    obtain ⟨z, _, rfl⟩ := hx; exact bY_nonneg z
+  have hlenR : (6:ℝ) ≤ (cs.length : ℝ) := by exact_mod_cast hd7
+  have hden : (7:ℝ) ≤ ((cs.length : ℝ) + 1) + S := by linarith
+  have hbY : bY (Branch.node cs) = 1 / (((cs.length : ℝ) + 1) + S) := by rw [bY_node, ← hSdef]
+  have hbYle : bY (Branch.node cs) ≤ 1/7 := by
+    rw [hbY]; exact one_div_le_one_div_of_le (by norm_num) (by linarith)
+  have hbVnode : bV mu (Branch.node cs) ≤ mu * (1/7) := by
+    have hb : bV mu (Branch.node cs) = bell (Branch.node cs) + mu * bY (Branch.node cs) := rfl
+    rw [hb]; nlinarith [hceil, mul_le_mul_of_nonneg_left hbYle hμpos]
+  have hVc : bV mu cherry = Real.log (3/2) - 2*FSTAR + mu * (1/3) := by
+    rw [bV, bell_cherry, bY_cherry]
+  have h4μ : mu * (1/7) ≤ bV mu cherry := by
+    rw [hVc]; nlinarith [cherry_ceiling_gap, hμlo]
+  linarith [hbVnode, h4μ]
+
+/-- **The flowed per-hub step, from the branch ceiling.**  Case split on `cs.length`: `{1..5}` route through
+    `hub_le_d2..d6` (tangent decouple), `≥6` through `hub_le_highdeg` (needs `bell (node cs) ≤ 0`).  Reduces
+    `FlowedHubStep` — and hence the SCL for every non-leaf branch — to the single global obligation
+    `∀ b, bell b ≤ 0` (the branch ceiling).  `conjecture1_proved = False`. -/
+theorem flowed_hub_step_of_ceiling (hceil : ∀ b, bell b ≤ 0) : FlowedHubStep := by
+  intro cs hcs hchild mu hmu
+  have hlen1 : 1 ≤ cs.length := by
+    rcases cs with _ | ⟨a, t⟩
+    · exact absurd rfl hcs
+    · simp
+  rcases Nat.lt_or_ge cs.length 6 with hlo | hhi
+  · rcases (by omega : cs.length = 1 ∨ cs.length = 2 ∨ cs.length = 3 ∨ cs.length = 4 ∨ cs.length = 5)
+      with h | h | h | h | h
+    · exact hub_le_d2 hmu h hchild
+    · exact hub_le_d3 hmu h hchild
+    · exact hub_le_d4 hmu h hchild
+    · exact hub_le_d5 hmu h hchild
+    · exact hub_le_d6 hmu h hchild
+  · exact hub_le_highdeg hmu hhi (hceil (Branch.node cs))
+
+/-- **The SCL for every non-leaf branch, from the branch ceiling.**  Chains `flowed_hub_step_of_ceiling`
+    into `scl_of_flowed_step`.  This is the full reduction of the leaf-excluding single-child lemma to the
+    single global obligation `∀ b, bell b ≤ 0`.  `conjecture1_proved = False`. -/
+theorem scl_of_ceiling (hceil : ∀ b, bell b ≤ 0) : ∀ b, PSCLne b :=
+  scl_of_flowed_step (flowed_hub_step_of_ceiling hceil)
+
+/-- **The per-hub ceiling step** — the SINGLE remaining obligation.  A hub `node cs` whose children each
+    satisfy BOTH the branch ceiling `bell c ≤ 0` AND the leaf-excluding SCL `PSCLne c` has `bell (node cs) ≤ 0`.
+    This is exactly step `1b` / `2b-lo` of the BG upper-bound ledger (the `M_d` frontier: `ell(hub) ≤ ell(B(k)) ≤ 0`),
+    whose arithmetic is GATED in Telperion (`MdStepCertificate`, `NearBroomUnimodalityCertificate`,
+    `HighDegreeTailCertificate`, `BroomOptimumCertificate` — all `.check()` pass).  Its shape — child ceilings +
+    child SCL ⟹ hub ceiling — is precisely what those certificates consume.  `conjecture1_proved = False`. -/
+def CeilStep : Prop :=
+  ∀ cs : List Branch, (∀ c ∈ cs, bell c ≤ 0) → (∀ c ∈ cs, PSCLne c) → bell (Branch.node cs) ≤ 0
+
+/-- **The joint ceiling+SCL induction.**  ONE well-founded strong induction on `|b|` proves BOTH the branch
+    ceiling `bell b ≤ 0` AND the leaf-excluding SCL `PSCLne b` for every branch, reduced to the single per-hub
+    ceiling step `CeilStep`.  At a hub `node cs`: the child IH supplies BOTH properties on the (smaller) children;
+    `CeilStep` gives the hub ceiling `bell (node cs) ≤ 0`; then the SCL follows — `hub_le_d2..d6` (tangent
+    decouple, using child SCL) for degree `≤ 6`, and `hub_le_highdeg` (using the just-proved hub ceiling) for
+    degree `≥ 7`.  This ELIMINATES the free-floating `∀ b, bell b ≤ 0` hypothesis of `scl_of_ceiling`: the SCL's
+    d≥7 leg now draws the ceiling from the JOINT induction hypothesis, so the sole residual is `CeilStep` itself
+    — the `M_d` frontier, matching the BG ledger's single open piece exactly.  `conjecture1_proved = False`. -/
+theorem ceil_and_scl_of_ceilStep (hceil : CeilStep) : ∀ b, bell b ≤ 0 ∧ PSCLne b := by
+  refine scl_of_child_step bsize bchildren (fun b => bell b ≤ 0 ∧ PSCLne b) bchildren_bsize_lt
+    (fun a hIH => ?_)
+  cases a with
+  | node cs =>
+    have hcc : ∀ c ∈ cs, bell c ≤ 0 := fun c hc => (hIH c (by simpa only [bchildren] using hc)).1
+    have hcs : ∀ c ∈ cs, PSCLne c := fun c hc => (hIH c (by simpa only [bchildren] using hc)).2
+    have hb : bell (Branch.node cs) ≤ 0 := hceil cs hcc hcs
+    refine ⟨hb, ?_⟩
+    intro hne μ hμ
+    have hne' : cs ≠ [] := fun h => hne (by rw [h])
+    have hlen1 : 1 ≤ cs.length := by
+      rcases cs with _ | ⟨a, t⟩
+      · exact absurd rfl hne'
+      · simp
+    rcases Nat.lt_or_ge cs.length 6 with hlo | hhi
+    · rcases (by omega : cs.length = 1 ∨ cs.length = 2 ∨ cs.length = 3 ∨ cs.length = 4 ∨ cs.length = 5)
+        with h | h | h | h | h
+      · exact hub_le_d2 hμ h hcs
+      · exact hub_le_d3 hμ h hcs
+      · exact hub_le_d4 hμ h hcs
+      · exact hub_le_d5 hμ h hcs
+      · exact hub_le_d6 hμ h hcs
+    · exact hub_le_highdeg hμ hhi hb
+
+/-- The branch ceiling `∀ b, bell b ≤ 0` from the per-hub ceiling step. -/
+theorem bell_ceiling_of_ceilStep (hceil : CeilStep) : ∀ b, bell b ≤ 0 :=
+  fun b => (ceil_and_scl_of_ceilStep hceil b).1
+
+/-- The SCL `∀ b, PSCLne b` from the per-hub ceiling step (no free-floating ceiling hypothesis). -/
+theorem scl_of_ceilStep (hceil : CeilStep) : ∀ b, PSCLne b :=
+  fun b => (ceil_and_scl_of_ceilStep hceil b).2
+
+end BGSCL
+end R3Cert