diff --git a/LeanFrontier/Analysis/Nesbitt.lean b/LeanFrontier/Analysis/Nesbitt.lean
index 40333645..90f9060d 100644
--- a/LeanFrontier/Analysis/Nesbitt.lean
+++ b/LeanFrontier/Analysis/Nesbitt.lean
@@ -1,4 +1,4 @@
-import Mathlib.Data.Real.Basic
+import Mathlib.Basic.Real.Basic
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Positivity
diff --git a/LeanFrontier/Analysis/SlopeMinorant.lean b/LeanFrontier/Analysis/SlopeMinorant.lean
index f3543c01..9dd89bc7 100644
--- a/LeanFrontier/Analysis/SlopeMinorant.lean
+++ b/LeanFrontier/Analysis/SlopeMinorant.lean
@@ -1,5 +1,5 @@
 import Mathlib.Data.Finset.Lattice.Fold
-import Mathlib.Data.Real.Basic
+import Mathlib.Basic.Real.Basic
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Ring
 
diff --git a/LeanFrontier/Combinatorics/CircularDominoTilings.lean b/LeanFrontier/Combinatorics/CircularDominoTilings.lean
index 64a46e5e..fe7bd506 100644
--- a/LeanFrontier/Combinatorics/CircularDominoTilings.lean
+++ b/LeanFrontier/Combinatorics/CircularDominoTilings.lean
@@ -56,7 +56,7 @@ theorem card_circularOneTwoTilings_add_two (n : ℕ) :
     obtain ⟨l, -, rfl⟩ := Finset.mem_image.mp hxFalse
     obtain ⟨r, -, h⟩ := Finset.mem_image.mp hxTrue
     simp at h
-  rw [circularOneTwoTilings, if_pos htwo, hsub,
+  rw [circularOneTwoTilings, ite_eq_left htwo, hsub,
     Finset.card_union_of_disjoint hdisj,
     Finset.card_image_of_injective _ (by
       intro a b h
diff --git a/LeanFrontier/Dynamics/LogisticMap.lean b/LeanFrontier/Dynamics/LogisticMap.lean
index 1a9ea555..d66e7d7c 100644
--- a/LeanFrontier/Dynamics/LogisticMap.lean
+++ b/LeanFrontier/Dynamics/LogisticMap.lean
@@ -58,10 +58,10 @@ noncomputable def tentMap (x : ℝ) : ℝ := if x ≤ 1 / 2 then 2 * x else 2 *
 /-- The logistic map at parameter four, `x ↦ 4 * x * (1 - x)`, extended to all of `ℝ`. -/
 def logisticMap (x : ℝ) : ℝ := 4 * x * (1 - x)
 
-theorem tentMap_of_le {x : ℝ} (h : x ≤ 1 / 2) : tentMap x = 2 * x := if_pos h
+theorem tentMap_of_le {x : ℝ} (h : x ≤ 1 / 2) : tentMap x = 2 * x := ite_eq_left h
 
 theorem tentMap_of_half_lt {x : ℝ} (h : 1 / 2 < x) : tentMap x = 2 * (1 - x) :=
-  if_neg (not_le.mpr h)
+  ite_eq_right (not_le.mpr h)
 
 /-- The identity behind both branches of the semiconjugacy: doubling the angle inside
 `sin ^ 2` is applying the logistic map outside. -/
diff --git a/LeanFrontier/Geometry/InversiveGeometry.lean b/LeanFrontier/Geometry/InversiveGeometry.lean
index c3a466f2..935c7dc4 100644
--- a/LeanFrontier/Geometry/InversiveGeometry.lean
+++ b/LeanFrontier/Geometry/InversiveGeometry.lean
@@ -1,4 +1,4 @@
-import Mathlib.Data.Complex.Basic
+import Mathlib.Basic.Complex.Basic
 import Mathlib.Tactic.LinearCombination
 
 /-!
diff --git a/LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean b/LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean
index aed0a999..5137bcaf 100644
--- a/LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean
+++ b/LeanFrontier/NumberTheory/SternBrocot/NodeInterval.lean
@@ -53,12 +53,12 @@ theorem mediant_bounds_eq_pair (path : List Bool) :
   | cons dir path ih =>
       rw [bounds_cons]
       cases dir
-      · simp only [mapBounds, mapPair, Bool.false_eq_true, if_false, Prod.fst, Prod.snd, pair]
+      · simp only [mapBounds, mapPair, Bool.false_eq_true, ite_false, Prod.fst, Prod.snd, pair]
         constructor
         · exact ih.1
         · rw [Nat.cast_add]
           omega
-      · simp only [mapBounds, mapPair, if_true, Prod.fst, Prod.snd, pair]
+      · simp only [mapBounds, mapPair, ite_true, Prod.fst, Prod.snd, pair]
         constructor
         · rw [Nat.cast_add]
           omega
diff --git a/LeanFrontier/NumberTheory/SternDiatomic.lean b/LeanFrontier/NumberTheory/SternDiatomic.lean
index 8a6dcab5..3e07c66b 100644
--- a/LeanFrontier/NumberTheory/SternDiatomic.lean
+++ b/LeanFrontier/NumberTheory/SternDiatomic.lean
@@ -65,7 +65,7 @@ theorem fusc_two_mul (n : ℕ) : fusc (2 * n) = fusc n := by
   · have hm : 2 * (k + 1) = 2 * k + 2 := by ring
     have heven : (2 * k + 2) % 2 = 0 := by omega
     have hdiv : (2 * k + 2) / 2 = k + 1 := by omega
-    rw [hm, fusc, if_pos heven, hdiv]
+    rw [hm, fusc, ite_eq_left heven, hdiv]
 
 /-- An odd index splits into the two neighbouring values at half the index. -/
 theorem fusc_two_mul_add_one (n : ℕ) : fusc (2 * n + 1) = fusc n + fusc (n + 1) := by
@@ -74,7 +74,7 @@ theorem fusc_two_mul_add_one (n : ℕ) : fusc (2 * n + 1) = fusc n + fusc (n + 1
   · have hm : 2 * (k + 1) + 1 = (2 * k + 1) + 2 := by ring
     have hodd : ¬ ((2 * k + 1 + 2) % 2 = 0) := by omega
     have hdiv : (2 * k + 1 + 2) / 2 = k + 1 := by omega
-    rw [hm, fusc, if_neg hodd, hdiv]
+    rw [hm, fusc, ite_eq_right hodd, hdiv]
 
 /-- Consecutive values of Stern's diatomic sequence are coprime, so the fraction
 `fusc n / fusc (n + 1)` is always in lowest terms. -/
diff --git a/LeanFrontier/NumberTheory/ThueMorse.lean b/LeanFrontier/NumberTheory/ThueMorse.lean
index 129ad886..f5933901 100644
--- a/LeanFrontier/NumberTheory/ThueMorse.lean
+++ b/LeanFrontier/NumberTheory/ThueMorse.lean
@@ -82,9 +82,9 @@ theorem thueMorse_two_mul_add_one (n : ℕ) : thueMorse (2 * n + 1) = !thueMorse
 theorem thueMorseSign_eq_ite (n : ℕ) :
     thueMorseSign n = if thueMorse n then -1 else 1 := by
   rcases Nat.even_or_odd (Nat.digits 2 n).sum with h | h
-  · rw [thueMorseSign, h.neg_one_pow, if_neg]
+  · rw [thueMorseSign, h.neg_one_pow, ite_eq_right]
     simp [thueMorse, Nat.not_odd_iff_even, h]
-  · rw [thueMorseSign, h.neg_one_pow, if_pos]
+  · rw [thueMorseSign, h.neg_one_pow, ite_eq_left]
     simp [thueMorse, h]
 
 private theorem thueMorseSign_two_mul (n : ℕ) : thueMorseSign (2 * n) = thueMorseSign n := by
diff --git a/LeanFrontier/Topology/Furstenberg.lean b/LeanFrontier/Topology/Furstenberg.lean
index bf056890..32306276 100644
--- a/LeanFrontier/Topology/Furstenberg.lean
+++ b/LeanFrontier/Topology/Furstenberg.lean
@@ -76,7 +76,7 @@ topology. -/
 theorem isTopologicalBasis_arithProgression :
     @IsTopologicalBasis ℤ furstenbergTopology
       {S : Set ℤ | ∃ a b, b ≠ 0 ∧ S = arithProgression a b} := by
-  letI := furstenbergTopology
+  let := furstenbergTopology
   refine ⟨?_, ?_, rfl⟩
   · rintro t₁ ⟨a₁, b₁, hb₁, rfl⟩ t₂ ⟨a₂, b₂, hb₂, rfl⟩ x ⟨hx₁, hx₂⟩
     refine ⟨arithProgression x (b₁ * b₂), ⟨x, b₁ * b₂, mul_ne_zero hb₁ hb₂, rfl⟩,
@@ -94,7 +94,7 @@ theorem isTopologicalBasis_arithProgression :
 /-- Arithmetic progressions with nonzero step are open. -/
 theorem isOpen_arithProgression (a b : ℤ) (hb : b ≠ 0) :
     IsOpen[furstenbergTopology] (arithProgression a b) := by
-  letI := furstenbergTopology
+  let := furstenbergTopology
   exact isTopologicalBasis_arithProgression.isOpen ⟨a, b, hb, rfl⟩
 
 /-- Arithmetic progressions with nonzero step are closed: after reducing to a positive
@@ -103,7 +103,7 @@ residues. Together with `isOpen_arithProgression`, the basic sets of the Fursten
 topology are clopen. -/
 theorem isClosed_arithProgression (a : ℤ) {b : ℤ} (hb : b ≠ 0) :
     IsClosed[furstenbergTopology] (arithProgression a b) := by
-  letI := furstenbergTopology
+  let := furstenbergTopology
   have habs : arithProgression a b = arithProgression a |b| :=
     Set.ext fun x => (abs_dvd b (x - a)).symm
   have hpos : 0 < |b| := abs_pos.mpr hb
@@ -148,7 +148,7 @@ theorem infinite_arithProgression (a : ℤ) {b : ℤ} (hb : b ≠ 0) :
 arithmetic progression around each of its points. -/
 theorem infinite_of_isOpen {U : Set ℤ} (hU : IsOpen[furstenbergTopology] U)
     (hne : U.Nonempty) : U.Infinite := by
-  letI := furstenbergTopology
+  let := furstenbergTopology
   obtain ⟨x, hx⟩ := hne
   obtain ⟨V, ⟨a, b, hb, rfl⟩, -, hVU⟩ :=
     isTopologicalBasis_arithProgression.exists_subset_of_mem_open hx hU
@@ -159,7 +159,7 @@ the integers other than `1` and `-1`. -/
 theorem iUnion_prime_arithProgression :
     ⋃ p ∈ {p : ℕ | p.Prime}, arithProgression 0 (p : ℤ) = ({1, -1} : Set ℤ)ᶜ := by
   ext x
-  simp only [mem_iUnion, mem_setOf_eq, mem_arithProgression, sub_zero, mem_compl_iff,
+  simp only [mem_iUnion, mem_ofPred_eq, mem_arithProgression, sub_zero, mem_compl_iff,
     mem_insert_iff, mem_singleton_iff, exists_prop]
   constructor
   · rintro ⟨p, hp, hdvd⟩ h
@@ -190,7 +190,7 @@ theorem infinite_of_iUnion_eq_compl {S : Set ℕ} (h0 : 0 ∉ S)
   by_contra hinf
   rw [Set.not_infinite] at hinf
   have hfin : S.Finite := hinf
-  letI := furstenbergTopology
+  let := furstenbergTopology
   have hclosed : IsClosed (⋃ p ∈ S, arithProgression 0 (p : ℤ)) :=
     hfin.isClosed_biUnion fun p hp =>
       isClosed_arithProgression 0 (Int.natCast_ne_zero.mpr (fun h => h0 (h ▸ hp)))
diff --git a/docs/CONTRIBUTION-DIRECTIONS.md b/docs/CONTRIBUTION-DIRECTIONS.md
index 431e1613..981901ef 100644
--- a/docs/CONTRIBUTION-DIRECTIONS.md
+++ b/docs/CONTRIBUTION-DIRECTIONS.md
@@ -90,7 +90,8 @@ crossing the Markov uniqueness-conjecture boundary.
 
 ### A. Largest Ford circle between Farey neighbours
 
-**Current corpus fit:** ready to investigate.
+**Status:** landed as `LeanFrontier.FordCircle.mediant_is_unique_largest_in_farey_gap`
+(`LeanFrontier/Geometry/FareyFordCircle.lean`). Build on it rather than restating it.
 
 **Primary parents:**
 
@@ -133,7 +134,8 @@ gap."
 
 ### B. Ford–Farey–Descartes configuration
 
-**Current corpus fit:** ready to investigate.
+**Status:** landed as `LeanFrontier.FordCircle.farey_mediant_descartes_configuration`
+(`LeanFrontier/Geometry/FordCircleDescartes.lean`). Build on it rather than restating it.
 
 **Primary parents:**
 
@@ -176,7 +178,10 @@ gives `DescartesCircle` a genuine geometric interpretation.
 
 ### C. Lucas numbers as characteristic-polynomial data of Fibonacci Q-matrix powers
 
-**Current corpus fit:** ready to investigate.
+**Status:** partly covered by D. `LeanFrontier.Horadam.trace_fibMatrix_pow_succ_eq_lucas`
+proves the trace form, and the general companion-matrix power characteristic polynomial has
+landed, so the statement below may now be a short corollary. Check the catalogue before
+submitting it.
 
 **Primary parents:**
 
@@ -219,8 +224,10 @@ recurrence, determinant, and Binet-style work.
 
 ### D. General Horadam companion matrix
 
-**Current corpus fit:** high-value infrastructure; verify the live catalogue before
-implementation.
+**Status:** landed in `LeanFrontier/LinearAlgebra/HoradamCompanionMatrix.lean` and
+`HoradamCompanionMatrixSpecializations.lean`, including the explicit power formula, trace,
+determinant and characteristic-polynomial identities, and the Fibonacci/Lucas specialization.
+Build on it rather than restating it.
 
 **Primary parents:**
 
@@ -272,6 +279,9 @@ specializations, and later Binet-style results.
 
 ### E. Circular square/domino tilings counted by Lucas numbers
 
+**Status:** landed as `LeanFrontier.Nat.card_circularOneTwoTilings_add_two`
+(`LeanFrontier/Combinatorics/CircularDominoTilings.lean`).
+
 **Primary parents:** `FibonacciComposition` + `LucasNumber`.
 
 Classically, linear square/domino tilings are Fibonacci-counted while circular tilings are
@@ -303,6 +313,10 @@ modest.
 
 ### G. Maximum Stern-row value is Fibonacci
 
+**Status:** landed as `LeanFrontier.SternDiatomic.fib_is_max_on_dyadic_row`
+(`LeanFrontier/NumberTheory/SternDiatomic/RowMaximum.lean`), with attainment in both Fibonacci
+orientations.
+
 **Primary parent:** `SternDiatomic`; Fibonacci support would mainly come from Mathlib.
 
 The classical extremal theorem says the maximum of Stern's sequence on an appropriate dyadic
@@ -320,7 +334,13 @@ Treat it as a good independent Stern extension, not as a top corpus-synthesis ta
 
 ### H. Stern diatomic / Calkin–Wilf to Stern–Brocot representation bridge
 
-**Status:** reformulated; high effort.
+**Status:** landed. Both path enumerations
+(`LeanFrontier.CalkinWilf.exists_code_eq`, `LeanFrontier.SternBrocot.existsUnique_pair_of_coprime`),
+the Stern–Brocot interval invariants (`LeanFrontier/NumberTheory/SternBrocot/Intervals.lean`),
+and the bridge itself: `LeanFrontier.CalkinWilf.pair_reverse_eq_sternBrocot` and
+`pair_eq_sternBrocot_iff_reverse` (`LeanFrontier/NumberTheory/CalkinWilfSternBrocot.lean`)
+show that a Calkin–Wilf path and a Stern–Brocot path reach the same pair exactly when they are
+reverses. Traversal orders are not identified; that remains open.
 
 **Critical correction:**