diff --git a/HighDimProb/Analysis/OpenJensen.lean b/HighDimProb/Analysis/OpenJensen.lean
new file mode 100644
index 0000000..bcdccde
--- /dev/null
+++ b/HighDimProb/Analysis/OpenJensen.lean
@@ -0,0 +1,89 @@
+import Mathlib.Analysis.Convex.Continuous
+import Mathlib.Analysis.Convex.Integral
+
+/-!
+# Open-domain Jensen
+
+This module upgrades Mathlib's closed-domain integral Jensen inequality to the
+case of a concave function on an open convex set, provided the Bochner mean is
+known to stay in the domain.
+-/
+
+noncomputable section
+
+open MeasureTheory Set
+open scoped Topology
+
+section ClosureHypograph
+
+variable {E : Type*} [TopologicalSpace E]
+variable {s : Set E} {g : E → Real}
+
+private theorem le_of_mem_closure_hypograph_of_isOpen
+    (hgc : ContinuousOn g s) (hsOpen : IsOpen s)
+    {x : E} (hx : x ∈ s) {r : Real}
+    (hr : (x, r) ∈ closure {p : E × Real | p.1 ∈ s ∧ p.2 ≤ g p.1}) :
+    r ≤ g x := by
+  let hypograph : Set (E × Real) := {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
+  let strictEpigraph : Set (E × Real) := {p | p.1 ∈ s ∧ g p.1 < p.2}
+  by_contra hle
+  have hxr : (x, r) ∈ strictEpigraph := by
+    exact ⟨hx, lt_of_not_ge hle⟩
+  have hmap :
+      ContinuousOn (fun p : E × Real => (g p.1, p.2)) (s ×ˢ (Set.univ : Set Real)) :=
+    hgc.prodMap continuousOn_id
+  have hOpenStrict : IsOpen strictEpigraph := by
+    have :
+        IsOpen
+          ((s ×ˢ (Set.univ : Set Real)) ∩
+            (fun p : E × Real => (g p.1, p.2)) ⁻¹'
+              {q : Real × Real | q.1 < q.2}) :=
+      hmap.isOpen_inter_preimage (hsOpen.prod isOpen_univ)
+        (isOpen_lt continuous_fst continuous_snd)
+    simpa [strictEpigraph, Set.prod_eq] using this
+  rcases mem_closure_iff_nhds.mp hr strictEpigraph (hOpenStrict.mem_nhds hxr) with
+    ⟨p, hpStrict, hpHypo⟩
+  exact (not_lt_of_ge hpHypo.2) hpStrict.2
+
+end ClosureHypograph
+
+variable {α E : Type*}
+variable [MeasurableSpace α]
+variable [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+variable [FiniteDimensional ℝ E]
+variable {μ : Measure α} [IsProbabilityMeasure μ]
+variable {s : Set E} {f : α → E} {g : E → Real}
+
+namespace ConcaveOn
+
+/-- Integral Jensen for a concave function on a convex open domain.
+
+Mathlib already provides `ConcaveOn.le_map_integral` for convex closed domains.
+This wrapper uses the convex hypograph together with continuity on open convex
+sets to remove the closedness assumption, replacing it with an explicit
+hypothesis that the Bochner mean stays in the domain.
+-/
+theorem le_map_integral_of_mem_open
+    (hg : ConcaveOn ℝ s g) (hsOpen : IsOpen s)
+    (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (hgi : Integrable (g ∘ f) μ)
+    (hmean : ∫ x, f x ∂μ ∈ s) :
+    ∫ x, g (f x) ∂μ ≤ g (∫ x, f x ∂μ) := by
+  let hypograph : Set (E × Real) := {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
+  have hmem :
+      ∀ᵐ x ∂μ, (f x, g (f x)) ∈ hypograph := by
+    filter_upwards [hfs] with x hx
+    exact ⟨hx, le_rfl⟩
+  have hpairInt : Integrable (fun x => (f x, g (f x))) μ :=
+    hfi.prodMk <| by simpa [Function.comp] using hgi
+  have hpairClosure :
+      ∫ x, (f x, g (f x)) ∂μ ∈ closure hypograph := by
+    exact hg.convex_hypograph.closure.integral_mem isClosed_closure
+      (hmem.mono fun _ hx => subset_closure hx) hpairInt
+  have hpair :
+      (∫ x, f x ∂μ, ∫ x, g (f x) ∂μ) ∈ closure hypograph := by
+    rw [integral_pair hfi (by simpa [Function.comp] using hgi)] at hpairClosure
+    exact hpairClosure
+  exact le_of_mem_closure_hypograph_of_isOpen
+    (s := s) (g := g) (hg.continuousOn hsOpen) hsOpen hmean hpair
+
+end ConcaveOn
diff --git a/HighDimProb/Analysis/SelfAdjointCarrier.lean b/HighDimProb/Analysis/SelfAdjointCarrier.lean
new file mode 100644
index 0000000..28e4647
--- /dev/null
+++ b/HighDimProb/Analysis/SelfAdjointCarrier.lean
@@ -0,0 +1,142 @@
+import Mathlib
+import Mathlib.Topology.Algebra.Module.Star
+
+/-!
+# Self-adjoint carrier bridge
+
+This module bridges the two Mathlib carriers used for real self-adjoint elements:
+`selfAdjoint A` and the subtype carrier of `selfAdjoint.submodule Real A`.
+-/
+
+noncomputable section
+
+namespace selfAdjoint
+
+section Carrier
+
+variable {A : Type*}
+variable [NormedAddCommGroup A] [NormedSpace Real A]
+variable [StarAddMonoid A] [StarModule Real A]
+
+instance : ContinuousENorm (selfAdjoint A) where
+  toENorm := inferInstance
+  continuous_enorm :=
+    (continuous_enorm : Continuous fun a : A => enorm a).comp continuous_subtype_val
+
+instance : ContinuousENorm (selfAdjoint.submodule Real A) where
+  toENorm := inferInstance
+  continuous_enorm :=
+    (continuous_enorm : Continuous fun a : A => enorm a).comp continuous_subtype_val
+
+/-- The self-adjoint carrier inherits continuous real scalar multiplication
+from the ambient normed real vector space. This lets finite-dimensional linear
+equivalences on `selfAdjoint A` upgrade to continuous linear equivalences. -/
+instance instContinuousSMulSelfAdjoint : ContinuousSMul Real (selfAdjoint A) :=
+  Topology.IsInducing.continuousSMul (g := fun x : selfAdjoint A => (x : A))
+    (f := fun r : Real => r) Topology.IsInducing.subtypeVal continuous_id (by intro c x; rfl)
+
+omit [NormedSpace Real A] [StarModule Real A] in
+theorem isClosed [ContinuousStar A] : IsClosed (selfAdjoint A : Set A) := by
+  simpa [selfAdjoint.mem_iff] using
+    (isClosed_eq (continuous_star : Continuous fun a : A => star a) continuous_id :
+      IsClosed {a : A | star a = a})
+
+instance instCompleteSpaceSelfAdjoint
+    [CompleteSpace A] [ContinuousStar A] : CompleteSpace (selfAdjoint A) := by
+  let hClosed : IsClosed (selfAdjoint A : Set A) := selfAdjoint.isClosed (A := A)
+  exact hClosed.completeSpace_coe
+/-- Continuous linear equivalence between `selfAdjoint A` and the subtype carrier
+of `selfAdjoint.submodule Real A`. -/
+@[simps!]
+def submoduleContinuousLinearEquiv :
+    ContinuousLinearEquiv (RingHom.id Real) (selfAdjoint A) (selfAdjoint.submodule Real A) where
+  toLinearEquiv :=
+    { toFun := fun x => Subtype.mk x.1 x.2
+      invFun := fun x => Subtype.mk x.1 x.2
+      left_inv := fun _ => rfl
+      right_inv := fun _ => rfl
+      map_add' := fun _ _ => rfl
+      map_smul' := fun _ _ => rfl }
+  continuous_toFun := continuous_subtype_val.subtype_mk _
+  continuous_invFun := continuous_subtype_val.subtype_mk _
+
+instance instFiniteDimensionalSelfAdjoint [FiniteDimensional Real A] :
+    FiniteDimensional Real (selfAdjoint A) := by
+  letI : FiniteDimensional Real (selfAdjoint.submodule Real A) :=
+    FiniteDimensional.finiteDimensional_submodule (selfAdjoint.submodule Real A)
+  exact LinearEquiv.finiteDimensional
+    (submoduleContinuousLinearEquiv (A := A)).toLinearEquiv.symm
+
+@[simp]
+theorem coe_submoduleContinuousLinearEquiv_apply (x : selfAdjoint A) :
+    ((submoduleContinuousLinearEquiv (A := A) x : selfAdjoint.submodule Real A) : A) = x :=
+  rfl
+
+@[simp]
+theorem coe_submoduleContinuousLinearEquiv_symm_apply (x : selfAdjoint.submodule Real A) :
+    ((submoduleContinuousLinearEquiv (A := A)).symm x : A) = x :=
+  rfl
+
+/-- The coercion from `selfAdjoint A` to `A` as a continuous linear map. -/
+def subtypeL : ContinuousLinearMap (RingHom.id Real) (selfAdjoint A) A :=
+  (selfAdjoint.submodule Real A).subtypeL.comp
+    (submoduleContinuousLinearEquiv (A := A)).toContinuousLinearMap
+
+@[simp]
+theorem subtypeL_apply (x : selfAdjoint A) : subtypeL (A := A) x = (x : A) :=
+  rfl
+
+section Integral
+
+variable {X : Type*}
+variable [MeasurableSpace X] {mu : MeasureTheory.Measure X}
+
+/-- Lift ambient Bochner integrability into the `selfAdjoint` carrier when all values are
+pointwise self-adjoint. -/
+theorem integrable_mk_of_integrable_coe
+    [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul Real A]
+    [Invertible (2 : Real)]
+    {F : X -> A} (hF : MeasureTheory.Integrable F mu) (hSA : forall x, IsSelfAdjoint (F x)) :
+    MeasureTheory.Integrable (fun x => ((Subtype.mk (F x) (hSA x)) : selfAdjoint A)) mu := by
+  have hpart :
+      MeasureTheory.Integrable (fun x => selfAdjointPartL (R := Real) (A := A) (F x)) mu :=
+    (selfAdjointPartL (R := Real) (A := A)).integrable_comp hF
+  refine hpart.congr <| Filter.Eventually.of_forall fun x => ?_
+  simpa [selfAdjointPartL] using (hSA x).selfAdjointPart_apply (R := Real)
+
+variable [CompleteSpace A]
+
+theorem coe_integral [hSA : CompleteSpace (selfAdjoint A)] {F : X -> selfAdjoint A}
+    (hF : MeasureTheory.Integrable F mu) :
+    ((MeasureTheory.integral mu F : selfAdjoint A) : A) =
+      MeasureTheory.integral mu (fun x => (F x : A)) := by
+  simpa [subtypeL_apply] using
+    (@ContinuousLinearMap.integral_comp_comm X (selfAdjoint A) A _ mu Real _ _ _ _ _ _ _ _ hSA
+      (subtypeL (A := A)) F hF).symm
+
+end Integral
+
+end Carrier
+
+section Part
+
+variable {A : Type*}
+variable [NormedAddCommGroup A] [NormedSpace Real A]
+variable [StarAddMonoid A] [StarModule Real A]
+variable [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul Real A]
+variable [Invertible (2 : Real)]
+
+/-- `selfAdjointPartL` retargeted to the submodule carrier. -/
+def partSubmoduleL : ContinuousLinearMap (RingHom.id Real) A (selfAdjoint.submodule Real A) :=
+  (submoduleContinuousLinearEquiv (A := A)).toContinuousLinearMap.comp
+    (selfAdjointPartL (R := Real) (A := A))
+
+@[simp]
+theorem coe_partSubmoduleL_apply (x : A) :
+    ((partSubmoduleL (A := A) x : selfAdjoint.submodule Real A) : A) =
+      ((selfAdjointPartL (R := Real) (A := A) x : selfAdjoint A) : A) :=
+  rfl
+
+end Part
+
+end selfAdjoint
diff --git a/HighDimProb/Analysis/SelfAdjointPositiveDomain.lean b/HighDimProb/Analysis/SelfAdjointPositiveDomain.lean
new file mode 100644
index 0000000..693c136
--- /dev/null
+++ b/HighDimProb/Analysis/SelfAdjointPositiveDomain.lean
@@ -0,0 +1,94 @@
+import Mathlib.Analysis.CStarAlgebra.Matrix
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
+import Mathlib.Analysis.Normed.Algebra.Spectrum
+import HighDimProb.Analysis.SelfAdjointCarrier
+import Mathlib.Analysis.Matrix.Order
+
+/-!
+# Strictly positive self-adjoint matrix domain
+
+This module packages the strictly positive real matrix domain in the
+`selfAdjoint` carrier used by the provider's Jensen-side transport work.
+
+It only exposes carrier/domain wrappers and small reusable set-level API.
+It does not prove any Lieb/Jensen exact statement.
+-/
+
+noncomputable section
+
+namespace HighDimProb
+
+open Set Topology
+open scoped MatrixOrder Matrix.Norms.L2Operator
+open Matrix
+
+/-- The strictly positive real self-adjoint matrices, viewed in the
+`selfAdjoint` carrier. -/
+abbrev selfAdjointStrictlyPositiveSet (n : Nat) :
+    Set (selfAdjoint (Matrix (Fin n) (Fin n) ℝ)) :=
+  { M | IsStrictlyPositive (M : Matrix (Fin n) (Fin n) ℝ) }
+
+@[simp]
+theorem mem_selfAdjointStrictlyPositiveSet {n : Nat}
+    {M : selfAdjoint (Matrix (Fin n) (Fin n) ℝ)} :
+    M ∈ selfAdjointStrictlyPositiveSet n ↔
+      IsStrictlyPositive (M : Matrix (Fin n) (Fin n) ℝ) :=
+  Iff.rfl
+
+@[simp]
+theorem mem_selfAdjointStrictlyPositiveSet_iff_posDef {n : Nat}
+    {M : selfAdjoint (Matrix (Fin n) (Fin n) ℝ)} :
+    M ∈ selfAdjointStrictlyPositiveSet n ↔
+      ((M : Matrix (Fin n) (Fin n) ℝ)).PosDef := by
+  rw [mem_selfAdjointStrictlyPositiveSet, Matrix.isStrictlyPositive_iff_posDef]
+
+/-- The carrier-form strictly positive domain is convex. -/
+theorem convex_selfAdjointStrictlyPositiveSet (n : Nat) :
+    Convex ℝ (selfAdjointStrictlyPositiveSet n) := by
+  classical
+  intro x hx y hy a b ha hb hab
+  have hxpd : ((x : Matrix (Fin n) (Fin n) ℝ)).PosDef :=
+    (mem_selfAdjointStrictlyPositiveSet_iff_posDef).mp hx
+  have hypd : ((y : Matrix (Fin n) (Fin n) ℝ)).PosDef :=
+    (mem_selfAdjointStrictlyPositiveSet_iff_posDef).mp hy
+  by_cases ha0 : a = 0
+  · have hb1 : b = 1 := by nlinarith [hab, ha0]
+    subst ha0 hb1
+    simpa using hy
+  · by_cases hb0 : b = 0
+    · have ha1 : a = 1 := by nlinarith [hab, hb0]
+      subst hb0 ha1
+      simpa using hx
+    · have ha_pos : 0 < a := lt_of_le_of_ne ha (Ne.symm ha0)
+      have hb_pos : 0 < b := lt_of_le_of_ne hb (Ne.symm hb0)
+      have hsum :
+          (a • ((x : Matrix (Fin n) (Fin n) ℝ)) +
+              b • ((y : Matrix (Fin n) (Fin n) ℝ))).PosDef :=
+        (hxpd.smul ha_pos).add (hypd.smul hb_pos)
+      exact (mem_selfAdjointStrictlyPositiveSet_iff_posDef).mpr hsum
+
+private theorem isOpen_matrix_strictlyPositiveOnSelfAdjointCarrier (n : Nat) :
+    IsOpen {M : selfAdjoint (Matrix (Fin n) (Fin n) ℝ) |
+      spectrum ℝ (M : Matrix (Fin n) (Fin n) ℝ) ⊆ Ioi (0 : ℝ)} := by
+  let f : selfAdjoint (Matrix (Fin n) (Fin n) ℝ) → Set ℝ :=
+    fun M => spectrum ℝ (M : Matrix (Fin n) (Fin n) ℝ)
+  have hf : UpperHemicontinuous f := by
+    simpa [f] using
+      (upperHemicontinuous_spectrum ℝ (Matrix (Fin n) (Fin n) ℝ)).comp continuous_subtype_val
+  exact (upperHemicontinuous_iff_isOpen_preimage_Iic.mp hf) (Ioi (0 : ℝ)) isOpen_Ioi
+
+/-- The strictly positive self-adjoint carrier domain is open. -/
+theorem isOpen_selfAdjointStrictlyPositiveSet (n : Nat) :
+    IsOpen (selfAdjointStrictlyPositiveSet n) := by
+  rw [show selfAdjointStrictlyPositiveSet n =
+      {M : selfAdjoint (Matrix (Fin n) (Fin n) ℝ) |
+        spectrum ℝ (M : Matrix (Fin n) (Fin n) ℝ) ⊆ Ioi (0 : ℝ)} from by
+        ext M
+        change IsStrictlyPositive (M : Matrix (Fin n) (Fin n) ℝ) ↔
+          spectrum ℝ (M : Matrix (Fin n) (Fin n) ℝ) ⊆ Ioi (0 : ℝ)
+        simpa using
+          (StarOrderedRing.isStrictlyPositive_iff_spectrum_pos
+            (a := (M : Matrix (Fin n) (Fin n) ℝ)) M.2)]
+  exact isOpen_matrix_strictlyPositiveOnSelfAdjointCarrier n
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/CStarOrderTransport.lean b/HighDimProb/RandomMatrix/CStarOrderTransport.lean
new file mode 100644
index 0000000..defa53b
--- /dev/null
+++ b/HighDimProb/RandomMatrix/CStarOrderTransport.lean
@@ -0,0 +1,90 @@
+import HighDimProb.RandomMatrix.CStarBridge
+import Mathlib.Analysis.CStarAlgebra.CStarMatrix
+import Mathlib.Analysis.Matrix.Order
+
+/-!
+# CStar order transport providers
+
+This module proves the first representation bridges needed to reuse Mathlib's
+CStar functional-calculus order theorems from HighDimProb's matrix layer.
+
+The key point is that ordinary `Matrix` order and `CStarMatrix` spectral order
+are not definitionally equal. We therefore transport positivity through the
+`StarOrderedRing.nonneg_iff` positive-cone characterization instead of trying to
+rewrite one order instance into the other.
+-/
+
+namespace HighDimProb
+
+noncomputable section
+
+open scoped ComplexOrder MatrixOrder
+
+private theorem cstarMatrixOfMatrix_mem_positiveCone_of_mem_positiveCone {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Complex}
+    (hA : A ∈ AddSubmonoid.closure
+      (Set.range fun B : Matrix (Fin n) (Fin n) Complex => star B * B)) :
+    (CStarMatrix.ofMatrix A : CStarMatrix (Fin n) (Fin n) Complex) ∈
+      AddSubmonoid.closure
+        (Set.range fun B : CStarMatrix (Fin n) (Fin n) Complex => star B * B) := by
+  induction hA using AddSubmonoid.closure_induction with
+  | zero =>
+      simp
+  | add X Y hX hY ihX ihY =>
+      simpa [CStarMatrix.of_add_of] using AddSubmonoid.add_mem _ ihX ihY
+  | mem X hX =>
+      rcases hX with ⟨B, rfl⟩
+      refine AddSubmonoid.subset_closure ?_
+      refine ⟨(CStarMatrix.ofMatrix B : CStarMatrix (Fin n) (Fin n) Complex), ?_⟩
+      ext i j
+      simp [CStarMatrix.mul_apply, CStarMatrix.star_apply, Matrix.mul_apply]
+
+/-- Ordinary complex-matrix positive semidefiniteness transports to the
+`CStarMatrix` spectral order. -/
+theorem cstarMatrixOfMatrix_nonneg_of_posSemidef {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Complex) (hA : A.PosSemidef) :
+    0 <= (CStarMatrix.ofMatrix A : CStarMatrix (Fin n) (Fin n) Complex) := by
+  rw [StarOrderedRing.nonneg_iff]
+  exact cstarMatrixOfMatrix_mem_positiveCone_of_mem_positiveCone
+    ((StarOrderedRing.nonneg_iff).mp (Matrix.PosSemidef.nonneg hA))
+
+private theorem cstarMatrixOfMatrix_isUnit_of_isUnit {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Complex} (hA : IsUnit A) :
+    IsUnit (CStarMatrix.ofMatrix A : CStarMatrix (Fin n) (Fin n) Complex) := by
+  obtain ⟨B, hAB, hBA⟩ := isUnit_iff_exists.mp hA
+  refine isUnit_iff_exists.mpr
+    ⟨(CStarMatrix.ofMatrix B : CStarMatrix (Fin n) (Fin n) Complex), ?_, ?_⟩
+  · simpa using congrArg CStarMatrix.ofMatrix hAB
+  · simpa using congrArg CStarMatrix.ofMatrix hBA
+
+/-- Ordinary complex-matrix Loewner order transports to the `CStarMatrix`
+spectral order. -/
+theorem cstarMatrixOfMatrix_le_of_matrix_le {n : Nat}
+    {A B : Matrix (Fin n) (Fin n) Complex} (hAB : A <= B) :
+    (CStarMatrix.ofMatrix A : CStarMatrix (Fin n) (Fin n) Complex) <=
+      (CStarMatrix.ofMatrix B : CStarMatrix (Fin n) (Fin n) Complex) := by
+  rw [← sub_nonneg]
+  have hPSD : (B - A).PosSemidef := Matrix.le_iff.mp hAB
+  have hNonneg :
+      0 <= (CStarMatrix.ofMatrix (B - A) :
+        CStarMatrix (Fin n) (Fin n) Complex) :=
+    cstarMatrixOfMatrix_nonneg_of_posSemidef (B - A) hPSD
+  simpa [CStarMatrix.of_sub_of] using hNonneg
+
+/-- Ordinary complex-matrix positive definiteness transports to strict
+positivity of the corresponding `CStarMatrix`. -/
+theorem cstarMatrixOfMatrix_strictlyPositive_of_posDef {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Complex) (hA : A.PosDef) :
+    IsStrictlyPositive
+      (CStarMatrix.ofMatrix A : CStarMatrix (Fin n) (Fin n) Complex) := by
+  have hNonneg :
+      0 <= (CStarMatrix.ofMatrix A : CStarMatrix (Fin n) (Fin n) Complex) :=
+    cstarMatrixOfMatrix_nonneg_of_posSemidef A hA.posSemidef
+  have hUnitCStar :
+      IsUnit (CStarMatrix.ofMatrix A : CStarMatrix (Fin n) (Fin n) Complex) :=
+    cstarMatrixOfMatrix_isUnit_of_isUnit hA.isUnit
+  exact hUnitCStar.isStrictlyPositive hNonneg
+
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/ConcentrationStatements.lean b/HighDimProb/RandomMatrix/ConcentrationStatements.lean
index 2b227cd..18d6388 100644
--- a/HighDimProb/RandomMatrix/ConcentrationStatements.lean
+++ b/HighDimProb/RandomMatrix/ConcentrationStatements.lean
@@ -6,6 +6,7 @@ import HighDimProb.RandomMatrix.Sums
 import HighDimProb.RandomMatrix.VarianceProxy
 import HighDimProb.RandomMatrix.Laplace
 import HighDimProb.RandomMatrix.HardboneStatements
+import HighDimProb.RandomMatrix.LiebProvider
 import HighDimProb.Tail
 import Mathlib.Analysis.Normed.Algebra.Spectrum
 
@@ -5267,6 +5268,182 @@ structure MatrixBernsteinConditioningTraceMGFTailAssumptions
     quadraticFormUpperTailEvent (randomMatrixSum X) t ⊆
       traceExpThresholdEvent (randomMatrixSum X) theta t
 
+
+
+/-- Provider-compressed bounded assumptions for the S9/S10 conditioning
+trace-MGF-to-tail route.
+
+This bundle replaces only the provider-proved parts of
+`MatrixBernsteinConditioningTraceMGFTailAssumptions`: natural-history
+measurability, step/history trace-exponential integrability, scaled
+matrix-exponential integrability, and the corresponding `K`-right-hand-side
+integrability.  It keeps independence, conditional expectation, variance-proxy,
+finite-measure, operator-norm, and tail-side assumptions explicit. -/
+structure MatrixBernsteinConditioningTraceMGFProviderAssumptions
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P] {m n : Nat}
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (V : Matrix (Fin n) (Fin n) Real)
+    (theta R t RH RZ RK RX : Real)
+    (mHist : Fin m -> MeasurableSpace Omega) : Prop where
+  chain :
+    @troppConditionalStep_of_iIndepFun_statement Omega mOmega P m n
+      theta X K mHist
+  suffixEntryMeasurable :
+    forall i : Fin m,
+      forall j : Fin m,
+        ((i.succ : Fin (m + 1)) : Nat) <= (j : Nat) ->
+          forall r c,
+            @Measurable Omega Real (mHist i) inferInstance
+              (fun omega => X j omega r c)
+  historyStepIndependent :
+    @troppHistoryStepIndependent_of_iIndepFun_statement Omega mOmega P m n
+      theta X K
+  conditionalExpectation :
+    forall i,
+      @condExp_traceExp_history_add_independent_step_statement
+        Omega mOmega P n
+        (mHist i) (@troppStateHistory Omega mOmega m n theta X K i)
+        (@troppCurrentRandomStep Omega mOmega m n theta X i) (K i)
+  historySub : forall i, mHist i <= mOmega
+  historyRandom :
+    forall i,
+      @IsRandomMatrix Omega mOmega n n P
+        (troppStateHistory theta X K i)
+  stepRandom :
+    forall i,
+      @IsRandomMatrix Omega mOmega n n P
+        (troppCurrentRandomStep theta X i)
+  historySelfAdjoint :
+    forall i omega, IsSelfAdjointMatrix (troppStateHistory theta X K i omega)
+  stepSelfAdjoint :
+    forall i,
+      @RandomSelfAdjointMatrix Omega mOmega n P
+        (troppCurrentRandomStep theta X i)
+  finiteMeasure : IsFiniteMeasure P
+  historyOperatorNormBound :
+    forall i omega,
+      operatorNorm (@troppStateHistory Omega mOmega m n theta X K i) omega <= RH
+  stepOperatorNormBound :
+    forall i omega,
+      operatorNorm (@troppCurrentRandomStep Omega mOmega m n theta X i) omega <= RZ
+  kOperatorNormBound :
+    forall i omega,
+      operatorNorm (fun _ : Omega => K i) omega <= RK
+  summandOperatorNormBound :
+    forall i omega, operatorNorm (X i) omega <= RX
+  summandRadiusNonneg : 0 <= RX
+  expMeanSelfAdjoint :
+    forall i,
+      IsSelfAdjointMatrix
+        (@matrixExpect Omega mOmega n n P
+          (fun omega => matrixExp (troppCurrentRandomStep theta X i omega)))
+  expMeanStrictlyPositive :
+    forall i,
+      IsStrictlyPositive
+        (@matrixExpect Omega mOmega n n P
+          (fun omega => matrixExp (troppCurrentRandomStep theta X i omega)))
+  sigmaFiniteHistory : forall i, SigmaFinite (P.trim (historySub i))
+  randomMatrix : forall i, IsRandomMatrix P (X i)
+  selfAdjoint : forall i, RandomSelfAdjointMatrix P (X i)
+  independent : ProbabilityTheory.iIndepFun X P
+  traceIntegrable :
+    IntegrableRealRandomVariable P
+      (traceExpIntegrand (randomMatrixSum X) theta)
+  comparisonSelfAdjoint : forall i, IsSelfAdjointMatrix (K i)
+  varianceProxySelfAdjoint : IsSelfAdjointMatrix V
+  radiusNonneg : 0 <= R
+  thetaRange : abs theta * R < 3
+  mgfComparison :
+    forall i,
+      MatrixLE
+        (matrixExpect P
+          (fun omega => matrixExp (SMul.smul theta (X i omega))))
+        (matrixExp (K i))
+  varianceProxyNormalization :
+    Finset.univ.sum (fun i : Fin m => K i) =
+      SMul.smul (bernsteinMGFCoeff theta R) V
+  tailAEMeasurable :
+    AEMeasurable
+      (fun omega => ENNReal.ofReal
+        (traceExpIntegrand (randomMatrixSum X) theta omega)) P
+  tailEventSubset :
+    quadraticFormUpperTailEvent (randomMatrixSum X) t ⊆
+      traceExpThresholdEvent (randomMatrixSum X) theta t
+
+/-- Convert the bounded provider-compressed S9/S10 bundle into the original
+explicit tail-assumption bundle.
+
+Only the provider-backed fields are synthesized here.  The independence,
+conditional-expectation, variance-proxy, and tail-side assumptions remain fields
+of `MatrixBernsteinConditioningTraceMGFProviderAssumptions`. -/
+def MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P] {m n : Nat}
+    {X : Fin m -> RandomMatrix Omega n n}
+    {K : Fin m -> Matrix (Fin n) (Fin n) Real}
+    {V : Matrix (Fin n) (Fin n) Real}
+    {theta R t RH RZ RK RX : Real}
+    {mHist : Fin m -> MeasurableSpace Omega}
+    (h : MatrixBernsteinConditioningTraceMGFProviderAssumptions
+      (P := P) X K V theta R t RH RZ RK RX mHist) :
+    MatrixBernsteinConditioningTraceMGFTailAssumptions
+      (P := P) X K V theta R t mHist := by
+  letI : IsFiniteMeasure P := h.finiteMeasure
+  refine
+    { chain := h.chain
+      historyMeasurable := ?historyMeasurable
+      historyStepIndependent := h.historyStepIndependent
+      conditionalExpectation := h.conditionalExpectation
+      historySub := h.historySub
+      historyRandom := h.historyRandom
+      stepRandom := h.stepRandom
+      historySelfAdjoint := h.historySelfAdjoint
+      stepSelfAdjoint := h.stepSelfAdjoint
+      conditionalTraceIntegrable := ?conditionalTraceIntegrable
+      stepExpIntegrable := ?stepExpIntegrable
+      expMeanSelfAdjoint := h.expMeanSelfAdjoint
+      expMeanStrictlyPositive := h.expMeanStrictlyPositive
+      sigmaFiniteHistory := h.sigmaFiniteHistory
+      rhsTraceIntegrable := ?rhsTraceIntegrable
+      randomMatrix := h.randomMatrix
+      selfAdjoint := h.selfAdjoint
+      independent := h.independent
+      expIntegrable := ?expIntegrable
+      traceIntegrable := h.traceIntegrable
+      comparisonSelfAdjoint := h.comparisonSelfAdjoint
+      varianceProxySelfAdjoint := h.varianceProxySelfAdjoint
+      radiusNonneg := h.radiusNonneg
+      thetaRange := h.thetaRange
+      mgfComparison := h.mgfComparison
+      varianceProxyNormalization := h.varianceProxyNormalization
+      tailAEMeasurable := h.tailAEMeasurable
+      tailEventSubset := h.tailEventSubset }
+  · exact
+      troppNaturalHistoryMeasurable_of_suffix_entry_measurable
+        theta X K mHist h.suffixEntryMeasurable
+  · exact
+      traceExpIntegrable_troppStateHistory_add_step_of_operatorNormBounds_finiteMeasure
+        theta X K RH RZ h.historyRandom h.stepRandom
+        h.historyOperatorNormBound h.stepOperatorNormBound
+  · intro i
+    have hExp :=
+      matrixExpScaledIntegrable_of_provider_finiteMeasure
+        theta RX X h.randomMatrix h.summandRadiusNonneg
+        h.summandOperatorNormBound i
+    simpa [troppCurrentRandomStep, scaledRandomMatrixFamily, scaledRandomMatrix]
+      using hExp
+  · exact
+      traceExpIntegrable_troppStateHistory_add_K_of_operatorNormBounds_finiteMeasure
+        theta X K RH RK h.historyRandom h.historyOperatorNormBound
+        h.kOperatorNormBound
+  · intro i
+    exact
+      matrixExpScaledIntegrable_of_provider_finiteMeasure
+        theta RX X h.randomMatrix h.summandRadiusNonneg
+        h.summandOperatorNormBound i
+
 /-- Progress-first composition from the S9 conditioning trace-MGF bridge to the
 quadratic-form Laplace/tail bound.
 
@@ -5427,6 +5604,32 @@ theorem matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumpt
       h.varianceProxySelfAdjoint h.radiusNonneg h.thetaRange h.mgfComparison
       h.varianceProxyNormalization h.tailAEMeasurable h.tailEventSubset
 
+/-- Bounded-provider S10 wrapper: synthesize the provider-backed assumptions and
+then call the existing conditioning trace-MGF-to-tail theorem.
+
+This is not an unconditional Matrix Bernstein theorem.  Finite measure,
+operator-norm bounds, suffix-entry measurability, independence,
+conditional-expectation, variance-proxy, and tail-side hypotheses remain
+explicit in the input bundle. -/
+theorem matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P] {m n : Nat}
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (V : Matrix (Fin n) (Fin n) Real)
+    (theta R t RH RZ RK RX : Real)
+    (mHist : Fin m -> MeasurableSpace Omega)
+    (h : MatrixBernsteinConditioningTraceMGFProviderAssumptions
+      (P := P) X K V theta R t RH RZ RK RX mHist) :
+    P (quadraticFormUpperTailEvent (randomMatrixSum X) t) <=
+      ENNReal.ofReal (Real.exp (-(theta * t))) *
+        ENNReal.ofReal
+          (traceMatrixExp (SMul.smul (bernsteinMGFCoeff theta R) V)) := by
+  exact
+    matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions
+      X K V theta R t mHist h.toTailAssumptions
+
+
 /-- Typed target for the spectral-radius reduction for self-adjoint matrices.
 
 This records a future bridge between HighDimProb's deterministic L2 operator
diff --git a/HighDimProb/RandomMatrix/EpsteinProvider.lean b/HighDimProb/RandomMatrix/EpsteinProvider.lean
new file mode 100644
index 0000000..9ec54dd
--- /dev/null
+++ b/HighDimProb/RandomMatrix/EpsteinProvider.lean
@@ -0,0 +1,324 @@
+import HighDimProb.RandomMatrix.TraceExpLogContinuityProvider
+import Mathlib.Analysis.Convex.Deriv
+
+/-!
+# Conditional Epstein-to-Lieb bridge
+
+This module does not prove Epstein's theorem. Instead, it packages the exact
+finite-dimensional affine-line concavity hypothesis needed to derive the
+provider's carrier-native Lieb concavity theorem and the ambient HighDimProb
+hardbone statement.
+-/
+
+namespace HighDimProb
+
+open HighDimProb
+open scoped MatrixOrder Matrix.Norms.L2Operator
+
+noncomputable section
+
+/-- Self-adjointness is preserved along real affine lines. -/
+private theorem isSelfAdjointMatrix_add_smul
+    {n : Nat} (A C : Matrix (Fin n) (Fin n) Real) (t : Real)
+    (hA : IsSelfAdjointMatrix A)
+    (hC : IsSelfAdjointMatrix C) :
+    IsSelfAdjointMatrix (A + t • C) := by
+  have ht : IsSelfAdjoint t := by
+    simp [IsSelfAdjoint]
+  change (A + t • C).IsHermitian
+  exact hA.add (hC.smul ht)
+
+/-- Finite-dimensional affine-line Epstein concavity hypothesis, stated in the
+exact form consumed by the provider bridge. -/
+abbrev EpsteinAffineLineConcavity : Prop :=
+  forall {n : Nat} (H A C : Matrix (Fin n) (Fin n) Real),
+    IsSelfAdjointMatrix H ->
+    IsSelfAdjointMatrix A ->
+    IsSelfAdjointMatrix C ->
+    (forall t : Real, t ∈ Set.Icc (0 : Real) 1 ->
+      IsStrictlyPositive (A + t • C)) ->
+    ConcaveOn Real (Set.Icc (0 : Real) 1)
+      (fun t : Real =>
+        traceMatrixExp (H + CFC.log (A + t • C)))
+
+/-- The trace-exp/log affine-line restriction is continuous on `[0, 1]` as soon
+as the whole line stays in the strictly positive self-adjoint cone. -/
+theorem continuousOn_traceMatrixExp_add_cfcLog_affineLine
+    {n : Nat} (H A C : Matrix (Fin n) (Fin n) Real)
+    (hA : IsSelfAdjointMatrix A)
+    (hC : IsSelfAdjointMatrix C)
+    (hPos : forall t : Real, t ∈ Set.Icc (0 : Real) 1 ->
+      IsStrictlyPositive (A + t • C)) :
+    ContinuousOn
+      (fun t : Real => traceMatrixExp (H + CFC.log (A + t • C)))
+      (Set.Icc (0 : Real) 1) := by
+  let s : Set (Matrix (Fin n) (Fin n) Real) :=
+    {M : Matrix (Fin n) (Fin n) Real |
+      And (IsSelfAdjointMatrix M) (IsStrictlyPositive M)}
+  have hAmbient :
+      ContinuousOn
+        (fun M : Matrix (Fin n) (Fin n) Real =>
+          traceMatrixExp (H + CFC.log M))
+        s :=
+    continuousOn_traceMatrixExp_add_cfcLog_selfAdjoint_strictlyPositive (H := H)
+  have hLine :
+      ContinuousOn (fun t : Real => A + t • C) (Set.Icc (0 : Real) 1) := by
+    simpa using
+      (continuous_const.add (continuous_id.smul continuous_const)).continuousOn
+  have hMapsTo :
+      Set.MapsTo
+        (fun t : Real => A + t • C)
+        (Set.Icc (0 : Real) 1)
+        s := by
+    intro t ht
+    exact ⟨isSelfAdjointMatrix_add_smul A C t hA hC, hPos t ht⟩
+  simpa [s] using hAmbient.comp hLine hMapsTo
+
+/-- Fixed affine-line concavity from scalar second-derivative control.
+
+This is the exact one-dimensional analytic bridge needed to reduce
+`EpsteinAffineLineConcavity` to a derivative/Hessian theorem for
+`t ↦ tr exp (H + log (A + t C))` on a strictly positive affine line. -/
+theorem concaveOn_traceMatrixExp_add_cfcLog_affineLine_of_hasDerivWithinAt2_nonpos
+    {n : Nat} (H A C : Matrix (Fin n) (Fin n) Real)
+    (hA : IsSelfAdjointMatrix A)
+    (hC : IsSelfAdjointMatrix C)
+    (hPos : forall t : Real, t ∈ Set.Icc (0 : Real) 1 ->
+      IsStrictlyPositive (A + t • C))
+    {f' f'' : Real -> Real}
+    (hf' : forall t : Real, t ∈ Set.Ioo (0 : Real) 1 ->
+      HasDerivWithinAt
+        (fun s : Real => traceMatrixExp (H + CFC.log (A + s • C)))
+        (f' t)
+        (Set.Ioo (0 : Real) 1)
+        t)
+    (hf'' : forall t : Real, t ∈ Set.Ioo (0 : Real) 1 ->
+      HasDerivWithinAt f' (f'' t) (Set.Ioo (0 : Real) 1) t)
+    (hf''_nonpos : forall t : Real, t ∈ Set.Ioo (0 : Real) 1 -> f'' t <= 0) :
+    ConcaveOn Real (Set.Icc (0 : Real) 1)
+      (fun t : Real => traceMatrixExp (H + CFC.log (A + t • C))) := by
+  refine concaveOn_of_hasDerivWithinAt2_nonpos (D := Set.Icc (0 : Real) 1) (f' := f') (f'' := f'')
+    (convex_Icc (0 : Real) 1) ?_ ?_ ?_ ?_
+  · exact continuousOn_traceMatrixExp_add_cfcLog_affineLine H A C hA hC hPos
+  · simpa using hf'
+  · simpa using hf''
+  · simpa using hf''_nonpos
+
+/-- Fixed affine-line concavity from ordinary scalar second-derivative control.
+
+This is the same bridge as
+`concaveOn_traceMatrixExp_add_cfcLog_affineLine_of_hasDerivWithinAt2_nonpos`,
+but with ordinary `HasDerivAt` hypotheses. Analytic proofs often produce this
+shape on the open interval before restricting to `Set.Ioo (0 : Real) 1`.
+-/
+theorem concaveOn_traceMatrixExp_add_cfcLog_affineLine_of_hasDerivAt2_nonpos
+    {n : Nat} (H A C : Matrix (Fin n) (Fin n) Real)
+    (hA : IsSelfAdjointMatrix A)
+    (hC : IsSelfAdjointMatrix C)
+    (hPos : forall t : Real, t ∈ Set.Icc (0 : Real) 1 ->
+      IsStrictlyPositive (A + t • C))
+    {f' f'' : Real -> Real}
+    (hf' : forall t : Real, t ∈ Set.Ioo (0 : Real) 1 ->
+      HasDerivAt
+        (fun s : Real => traceMatrixExp (H + CFC.log (A + s • C)))
+        (f' t)
+        t)
+    (hf'' : forall t : Real, t ∈ Set.Ioo (0 : Real) 1 ->
+      HasDerivAt f' (f'' t) t)
+    (hf''_nonpos : forall t : Real, t ∈ Set.Ioo (0 : Real) 1 -> f'' t <= 0) :
+    ConcaveOn Real (Set.Icc (0 : Real) 1)
+      (fun t : Real => traceMatrixExp (H + CFC.log (A + t • C))) :=
+  concaveOn_traceMatrixExp_add_cfcLog_affineLine_of_hasDerivWithinAt2_nonpos
+    H A C hA hC hPos
+    (fun t ht => (hf' t ht).hasDerivWithinAt)
+    (fun t ht => (hf'' t ht).hasDerivWithinAt)
+    hf''_nonpos
+
+/-- Global Epstein affine-line concavity from linewise derivative/Hessian
+control.
+
+This is the proof-facing form of the remaining analytic target: prove the
+linewise derivatives and the nonpositivity of the scalar second derivative, and
+the exact `EpsteinAffineLineConcavity` hypothesis consumed downstream follows.
+-/
+theorem epsteinAffineLineConcavity_of_hasDerivWithinAt2_nonpos
+    (hDeriv : forall {n : Nat} (H A C : Matrix (Fin n) (Fin n) Real),
+      IsSelfAdjointMatrix H ->
+      IsSelfAdjointMatrix A ->
+      IsSelfAdjointMatrix C ->
+      (forall t : Real, t ∈ Set.Icc (0 : Real) 1 ->
+        IsStrictlyPositive (A + t • C)) ->
+      exists f' f'' : Real -> Real,
+        (forall t : Real, t ∈ Set.Ioo (0 : Real) 1 ->
+          HasDerivWithinAt
+            (fun s : Real => traceMatrixExp (H + CFC.log (A + s • C)))
+            (f' t)
+            (Set.Ioo (0 : Real) 1)
+            t) ∧
+        (forall t : Real, t ∈ Set.Ioo (0 : Real) 1 ->
+          HasDerivWithinAt f' (f'' t) (Set.Ioo (0 : Real) 1) t) ∧
+        (forall t : Real, t ∈ Set.Ioo (0 : Real) 1 -> f'' t <= 0)) :
+    EpsteinAffineLineConcavity := by
+  intro n H A C hH hA hC hPos
+  rcases hDeriv H A C hH hA hC hPos with ⟨f', f'', hf', hf'', hf''_nonpos⟩
+  exact
+    concaveOn_traceMatrixExp_add_cfcLog_affineLine_of_hasDerivWithinAt2_nonpos
+      H A C hA hC hPos hf' hf'' hf''_nonpos
+
+/-- Global Epstein affine-line concavity from ordinary linewise derivative/Hessian
+control.
+
+This wrapper is intended for the remaining analytic Epstein target when it is
+proved with ordinary `HasDerivAt` statements on the open interval.
+-/
+theorem epsteinAffineLineConcavity_of_hasDerivAt2_nonpos
+    (hDeriv : forall {n : Nat} (H A C : Matrix (Fin n) (Fin n) Real),
+      IsSelfAdjointMatrix H ->
+      IsSelfAdjointMatrix A ->
+      IsSelfAdjointMatrix C ->
+      (forall t : Real, t ∈ Set.Icc (0 : Real) 1 ->
+        IsStrictlyPositive (A + t • C)) ->
+      exists f' f'' : Real -> Real,
+        (forall t : Real, t ∈ Set.Ioo (0 : Real) 1 ->
+          HasDerivAt
+            (fun s : Real => traceMatrixExp (H + CFC.log (A + s • C)))
+            (f' t)
+            t) ∧
+        (forall t : Real, t ∈ Set.Ioo (0 : Real) 1 ->
+          HasDerivAt f' (f'' t) t) ∧
+        (forall t : Real, t ∈ Set.Ioo (0 : Real) 1 -> f'' t <= 0)) :
+    EpsteinAffineLineConcavity := by
+  intro n H A C hH hA hC hPos
+  rcases hDeriv H A C hH hA hC hPos with ⟨f', f'', hf', hf'', hf''_nonpos⟩
+  exact
+    concaveOn_traceMatrixExp_add_cfcLog_affineLine_of_hasDerivAt2_nonpos
+      H A C hA hC hPos hf' hf'' hf''_nonpos
+
+private theorem affineLine_eq_segment
+    {n : Nat} (A B : selfAdjoint (Matrix (Fin n) (Fin n) Real)) (t : Real) :
+    (A : Matrix (Fin n) (Fin n) Real) + t • ((B : Matrix (Fin n) (Fin n) Real) - (A : Matrix (Fin n) (Fin n) Real)) =
+      ((((1 - t) • A + t • B : selfAdjoint (Matrix (Fin n) (Fin n) Real)) : Matrix (Fin n) (Fin n) Real)) := by
+  ext i j
+  simp [sub_eq_add_neg]
+  ring
+
+private theorem affineLine_eq_weighted
+    {n : Nat} (A B : selfAdjoint (Matrix (Fin n) (Fin n) Real)) {a b : Real} (hab : a + b = 1) :
+    (A : Matrix (Fin n) (Fin n) Real) + b • ((B : Matrix (Fin n) (Fin n) Real) - (A : Matrix (Fin n) (Fin n) Real)) =
+      (((a • A + b • B : selfAdjoint (Matrix (Fin n) (Fin n) Real)) : Matrix (Fin n) (Fin n) Real)) := by
+  calc
+    (A : Matrix (Fin n) (Fin n) Real) + b • ((B : Matrix (Fin n) (Fin n) Real) - (A : Matrix (Fin n) (Fin n) Real)) =
+        ((((1 - b) • A + b • B : selfAdjoint (Matrix (Fin n) (Fin n) Real)) : Matrix (Fin n) (Fin n) Real)) := by
+          simpa using affineLine_eq_segment A B b
+    _ = (((a • A + b • B : selfAdjoint (Matrix (Fin n) (Fin n) Real)) : Matrix (Fin n) (Fin n) Real)) := by
+          have ha : a = 1 - b := by linarith
+          simp [ha]
+
+private theorem affineLine_strictlyPositive
+    {n : Nat} {A B : selfAdjoint (Matrix (Fin n) (Fin n) Real)}
+    (hA : A ∈ selfAdjointStrictlyPositiveSet n)
+    (hB : B ∈ selfAdjointStrictlyPositiveSet n) :
+    forall t : Real, t ∈ Set.Icc (0 : Real) 1 ->
+      IsStrictlyPositive ((A : Matrix (Fin n) (Fin n) Real) + t • ((B : Matrix (Fin n) (Fin n) Real) - (A : Matrix (Fin n) (Fin n) Real))) := by
+  intro t ht
+  have hSegment :
+      (((1 - t) • A + t • B : selfAdjoint (Matrix (Fin n) (Fin n) Real)) ∈
+        selfAdjointStrictlyPositiveSet n) :=
+    (convex_selfAdjointStrictlyPositiveSet n) hA hB (by linarith [ht.2]) ht.1
+      (by linarith)
+  simpa [affineLine_eq_segment A B t] using hSegment
+
+/-- Conditional carrier Lieb concavity from a finite-dimensional Epstein
+affine-line theorem. -/
+theorem liebTraceExpConcavity_selfAdjointCarrier_analytic_of_epsteinAffineLine
+    (hEpstein : EpsteinAffineLineConcavity)
+    {n : Nat} (H : Matrix (Fin n) (Fin n) Real) :
+    IsSelfAdjointMatrix H ->
+      ConcaveOn Real (selfAdjointStrictlyPositiveSet n)
+        (fun M : selfAdjoint (Matrix (Fin n) (Fin n) Real) =>
+          traceMatrixExp (H + CFC.log (M : Matrix (Fin n) (Fin n) Real))) := by
+  intro hH
+  constructor
+  · exact convex_selfAdjointStrictlyPositiveSet n
+  · intro A hA B hB a b ha hb hab
+    let C : Matrix (Fin n) (Fin n) Real := (B : Matrix (Fin n) (Fin n) Real) - (A : Matrix (Fin n) (Fin n) Real)
+    have hC : IsSelfAdjointMatrix C := by
+      dsimp [C]
+      simpa using B.2.sub A.2
+    have hSegPos :
+        forall t : Real, t ∈ Set.Icc (0 : Real) 1 ->
+          IsStrictlyPositive ((A : Matrix (Fin n) (Fin n) Real) + t • C) := by
+      simpa [C] using affineLine_strictlyPositive hA hB
+    let g : Real -> Real := fun t : Real =>
+      traceMatrixExp (H + CFC.log ((A : Matrix (Fin n) (Fin n) Real) + t • C))
+    have hSegConcave :
+        ConcaveOn Real (Set.Icc (0 : Real) 1) g := by
+      simpa [g] using hEpstein H (A : Matrix (Fin n) (Fin n) Real) C hH A.2 hC hSegPos
+    have h0 : (0 : Real) ∈ Set.Icc (0 : Real) 1 := by
+      simp
+    have h1 : (1 : Real) ∈ Set.Icc (0 : Real) 1 := by
+      simp
+    have hSegIneq : a • g 0 + b • g 1 ≤ g b := by
+      simpa using hSegConcave.2 h0 h1 ha hb hab
+    have hAtOne : (A : Matrix (Fin n) (Fin n) Real) + C = (B : Matrix (Fin n) (Fin n) Real) := by dsimp [C]; abel
+    have hAtWeighted :
+        (A : Matrix (Fin n) (Fin n) Real) + b • C = (((a • A + b • B : selfAdjoint (Matrix (Fin n) (Fin n) Real)) : Matrix (Fin n) (Fin n) Real)) := by simpa [C] using (affineLine_eq_weighted (A := A) (B := B) (a := a) (b := b) hab)
+    simpa [g, one_smul, hAtOne, hAtWeighted] using hSegIneq
+
+/-- Conditional exact main hardbone witness from the same Epstein affine-line
+theorem. -/
+theorem liebTraceExpConcavity_of_epsteinAffineLine
+    (hEpstein : EpsteinAffineLineConcavity)
+    {n : Nat} (H : Matrix (Fin n) (Fin n) Real) :
+    liebTraceExpConcavity_statement H :=
+  liebTraceExpConcavity_of_selfAdjointCarrier H
+    (liebTraceExpConcavity_selfAdjointCarrier_analytic_of_epsteinAffineLine
+      hEpstein H)
+
+/-- Exact Jensen statement supplied from the same explicit Epstein affine-line
+hypothesis.
+
+The statement still has HighDimProb's original Lieb-concavity argument slot,
+but this provider witness ignores that slot and uses `hEpstein` instead. This
+is the form consumed by main-repo Tropp chain statements. -/
+theorem liebJensenTraceExp_statement_of_epsteinAffineLine
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    (hEpstein : EpsteinAffineLineConcavity)
+    {n : Nat}
+    (H : Matrix (Fin n) (Fin n) Real)
+    (Y : RandomMatrix Omega n n) :
+    liebJensenTraceExp_statement (P := P) H Y := by
+  intro _hConcave
+  exact
+    (liebJensenTraceExp_statement_of_liebConcavity (P := P) H Y)
+      (liebTraceExpConcavity_of_epsteinAffineLine hEpstein H)
+
+/-- Direct Jensen inequality from the explicit Epstein affine-line hypothesis.
+
+This is the same inequality as `liebJensenTraceExp_statement`, but with the
+Lieb-concavity premise discharged by `hEpstein`. -/
+theorem liebJensenTraceExp_of_epsteinAffineLine
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    (hEpstein : EpsteinAffineLineConcavity)
+    {n : Nat}
+    (H : Matrix (Fin n) (Fin n) Real)
+    (Y : RandomMatrix Omega n n)
+    (hH : IsSelfAdjointMatrix H)
+    (hYsa : forall omega, IsSelfAdjointMatrix (Y omega))
+    (hYpos : forall omega, IsStrictlyPositive (Y omega))
+    (hInt : IntegrableRandomMatrix P Y)
+    (hMeanSA : IsSelfAdjointMatrix (matrixExpect P Y))
+    (hMeanPos : IsStrictlyPositive (matrixExpect P Y))
+    (hTraceInt : IntegrableRealRandomVariable P
+      (fun omega => traceMatrixExp (H + CFC.log (Y omega)))) :
+    expect P (fun omega => traceMatrixExp (H + CFC.log (Y omega))) <=
+      traceMatrixExp (H + CFC.log (matrixExpect P Y)) :=
+  (liebJensenTraceExp_statement_of_epsteinAffineLine (P := P) hEpstein H Y)
+    (liebTraceExpConcavity_of_epsteinAffineLine hEpstein H)
+    hH hYsa hYpos hInt hMeanSA hMeanPos hTraceInt
+
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/IntegrabilityProvider.lean b/HighDimProb/RandomMatrix/IntegrabilityProvider.lean
new file mode 100644
index 0000000..7c376e7
--- /dev/null
+++ b/HighDimProb/RandomMatrix/IntegrabilityProvider.lean
@@ -0,0 +1,62 @@
+import HighDimProb.RandomMatrix.Basic
+import HighDimProb.RandomMatrix.OperatorNorm
+import HighDimProb.RandomMatrix.TraceExp
+
+namespace HighDimProb
+
+open HighDimProb
+open MeasureTheory
+open scoped Matrix.Norms.L2Operator
+
+noncomputable section
+
+/-- Finite-measure provider bridge for the scaled matrix exponential.
+
+The proof is entrywise: each entry of `matrixExp (theta • X_k)` is continuous
+on a compact closed ball, hence bounded; the bound is then turned into
+integrability using `MeasureTheory.Integrable.of_bound`.
+
+This is intentionally narrower than HighDimProb's exact statement, because the
+exact statement quantifies over an arbitrary measure `P` and therefore is not
+honestly provable without a finite/probability-measure hypothesis. -/
+theorem matrixExpScaledIntegrable_of_provider_finiteMeasure
+    {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} [IsFiniteMeasure P]
+    {m n : Nat} (theta R : Real) (X : Fin m -> RandomMatrix Omega n n) :
+    (forall k, IsRandomMatrix P (X k)) ->
+      0 <= R ->
+        (forall k omega, operatorNorm (X k) omega <= R) ->
+          forall k, IntegrableRandomMatrix P (fun omega => matrixExp (theta • (X k omega))) := by
+  intro hX hR hbound k i j
+  letI : NormedAlgebra Rat (Matrix (Fin n) (Fin n) Real) :=
+    NormedAlgebra.restrictScalars Rat Real (Matrix (Fin n) (Fin n) Real)
+  have hEntry : Continuous (fun M : Matrix (Fin n) (Fin n) Real => matrixExp M i j) := by
+    have hEntry' : Continuous (fun M : Matrix (Fin n) (Fin n) Real => M i j) := by
+      simpa using (continuous_apply j).comp (continuous_apply i)
+    simpa [HighDimProb.matrixExp] using hEntry'.comp NormedSpace.exp_continuous
+  have hcompact :
+      IsCompact (Metric.closedBall (0 : Matrix (Fin n) (Fin n) Real) (abs theta * R)) := by
+    simpa using
+      (isCompact_closedBall (0 : Matrix (Fin n) (Fin n) Real) (abs theta * R))
+  rcases hcompact.exists_bound_of_continuousOn hEntry.continuousOn with ⟨C, hC⟩
+  have hsmul_meas : Measurable (fun omega => theta • (X k omega)) := by
+    change Measurable (fun omega => fun i : Fin n => fun j : Fin n => theta * (X k omega i j))
+    refine measurable_pi_lambda (fun omega i => fun j : Fin n => theta * (X k omega i j)) ?_
+    intro i'
+    refine measurable_pi_lambda (fun omega j => theta * (X k omega i' j)) ?_
+    intro j'
+    simpa using (hX k i' j').const_mul theta
+  have hmeas : Measurable (fun omega => matrixExp (theta • (X k omega)) i j) :=
+    hEntry.measurable.comp hsmul_meas
+  apply MeasureTheory.Integrable.of_bound hmeas.aestronglyMeasurable C
+  filter_upwards with omega
+  have hdist :
+      dist (theta • (X k omega)) (0 : Matrix (Fin n) (Fin n) Real) <= abs theta * R := by
+    rw [dist_eq_norm, sub_zero, norm_smul, Real.norm_eq_abs]
+    exact mul_le_mul_of_nonneg_left (hbound k omega) (abs_nonneg theta)
+  have hmem : theta • (X k omega) ∈ Metric.closedBall (0 : Matrix (Fin n) (Fin n) Real) (abs theta * R) := by
+    simpa [Metric.mem_closedBall] using hdist
+  exact hC _ hmem
+
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/LiebProvider.lean b/HighDimProb/RandomMatrix/LiebProvider.lean
new file mode 100644
index 0000000..bd26533
--- /dev/null
+++ b/HighDimProb/RandomMatrix/LiebProvider.lean
@@ -0,0 +1,17 @@
+import HighDimProb.RandomMatrix.MatrixLogProvider
+import HighDimProb.RandomMatrix.TraceExpTroppStepProvider
+import HighDimProb.RandomMatrix.IntegrabilityProvider
+import HighDimProb.RandomMatrix.TraceExpIntegrabilityProvider
+import HighDimProb.RandomMatrix.NaturalHistoryProvider
+import HighDimProb.RandomMatrix.SupportProvider
+
+/-!
+# Provider-backed Lieb/Tropp theorem-push wrappers
+
+This aggregate module exposes the provider-proof leaves ported into the main
+HighDimProb namespace.  The imported modules keep the theorem boundaries
+explicit: deterministic log/order and trace-exp monotonicity, conditional
+Epstein-to-Lieb/Tropp wrappers, bounded finite-measure integrability providers,
+natural-history measurability from suffix entries, and identity support
+domination.
+-/
diff --git a/HighDimProb/RandomMatrix/MatrixLogProvider.lean b/HighDimProb/RandomMatrix/MatrixLogProvider.lean
new file mode 100644
index 0000000..0da7950
--- /dev/null
+++ b/HighDimProb/RandomMatrix/MatrixLogProvider.lean
@@ -0,0 +1,264 @@
+import HighDimProb.RandomMatrix.CStarOrderTransport
+import HighDimProb.RandomMatrix.HardboneStatements
+import HighDimProb.RandomMatrix.Spectral
+import Mathlib.Analysis.CStarAlgebra.CStarMatrix
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
+import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
+import Mathlib.Analysis.Matrix.Order
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
+
+/-!
+# Real-matrix logarithm monotonicity provider
+
+This module proves HighDimProb's real-matrix operator-log monotonicity
+statement by transporting real matrices through `CStarMatrix`, applying
+Mathlib's C-star functional-calculus theorem `CFC.log_le_log`, and reflecting
+matrix order back to HighDimProb's `MatrixLE` vocabulary.
+
+It deliberately does not prove Lieb concavity, Golden-Thompson, Tropp's
+trace-MGF theorem, or Matrix Bernstein. The only hard theorem consumed here is
+Mathlib's C-star logarithm monotonicity theorem.
+-/
+
+namespace HighDimProb
+
+noncomputable section
+
+open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator
+
+local instance cstarMatrixRealCFC {n : Nat} :
+    ContinuousFunctionalCalculus Real
+      (CStarMatrix (Fin n) (Fin n) Complex) IsSelfAdjoint :=
+  IsSelfAdjoint.instContinuousFunctionalCalculus
+
+/-- The HighDimProb real-to-`CStarMatrix` representation as a real star-algebra hom. -/
+def realMatrixToCStarStarAlgHom {n : Nat} :
+    Matrix (Fin n) (Fin n) Real →⋆ₐ[Real]
+      CStarMatrix (Fin n) (Fin n) Complex where
+  toFun := HighDimProb.realMatrixToCStarMatrix
+  map_zero' := by
+    ext i j
+    simp [HighDimProb.realMatrixToCStarMatrix]
+  map_one' := by
+    ext i j
+    by_cases h : i = j
+    · subst j
+      simp [HighDimProb.realMatrixToCStarMatrix]
+    · simp [HighDimProb.realMatrixToCStarMatrix, h]
+  map_add' A B := by
+    ext i j
+    simp [HighDimProb.realMatrixToCStarMatrix]
+  map_mul' A B := by
+    ext i j
+    simp [HighDimProb.realMatrixToCStarMatrix, CStarMatrix.mul_apply, Matrix.mul_apply]
+  commutes' r := by
+    ext i j
+    by_cases h : i = j
+    · subst j
+      simp [HighDimProb.realMatrixToCStarMatrix, CStarMatrix.algebraMap_apply,
+        Algebra.algebraMap_eq_smul_one]
+    · simp [HighDimProb.realMatrixToCStarMatrix, CStarMatrix.algebraMap_apply,
+        Algebra.algebraMap_eq_smul_one, h]
+  map_star' A := by
+    ext i j
+    simp [HighDimProb.realMatrixToCStarMatrix, CStarMatrix.star_apply, Matrix.star_apply]
+
+private theorem realMatrixToCStar_mem_positiveCone_of_mem_positiveCone {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real}
+    (hA : A ∈ AddSubmonoid.closure
+      (Set.range fun B : Matrix (Fin n) (Fin n) Real => star B * B)) :
+    HighDimProb.realMatrixToCStarMatrix A ∈ AddSubmonoid.closure
+      (Set.range fun B : CStarMatrix (Fin n) (Fin n) Complex => star B * B) := by
+  induction hA using AddSubmonoid.closure_induction with
+  | zero =>
+      simp
+  | add X Y _ _ ihX ihY =>
+      simpa [map_add] using AddSubmonoid.add_mem _ ihX ihY
+  | mem X hX =>
+      rcases hX with ⟨B, rfl⟩
+      refine AddSubmonoid.subset_closure ?_
+      refine ⟨HighDimProb.realMatrixToCStarMatrix B, ?_⟩
+      change star (realMatrixToCStarStarAlgHom (n := n) B) *
+          realMatrixToCStarStarAlgHom (n := n) B =
+        realMatrixToCStarStarAlgHom (n := n) (star B * B)
+      rw [map_mul, map_star]
+
+/-- Nonnegativity of a real matrix transports through the `CStarMatrix`
+representation. -/
+theorem realMatrixToCStar_nonneg {n : Nat} {A : Matrix (Fin n) (Fin n) Real}
+    (hA : 0 <= A) :
+    0 <= HighDimProb.realMatrixToCStarMatrix A := by
+  rw [StarOrderedRing.nonneg_iff] at hA
+  rw [StarOrderedRing.nonneg_iff]
+  exact realMatrixToCStar_mem_positiveCone_of_mem_positiveCone hA
+
+/-- Strict positivity of a real matrix transports through the `CStarMatrix`
+representation. -/
+theorem realMatrixToCStar_strictlyPositive {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real} (hA : IsStrictlyPositive A) :
+    IsStrictlyPositive (HighDimProb.realMatrixToCStarMatrix A) := by
+  have hNonneg : 0 <= HighDimProb.realMatrixToCStarMatrix A :=
+    realMatrixToCStar_nonneg hA.nonneg
+  have hUnit : IsUnit (HighDimProb.realMatrixToCStarMatrix A) := by
+    simpa [realMatrixToCStarStarAlgHom] using
+      hA.isUnit.map (realMatrixToCStarStarAlgHom (n := n))
+  exact hUnit.isStrictlyPositive hNonneg
+
+/-- HighDimProb matrix order transports through the `CStarMatrix` representation. -/
+theorem realMatrixToCStar_matrixLE {n : Nat}
+    {A B : Matrix (Fin n) (Fin n) Real} (hAB : HighDimProb.MatrixLE A B) :
+    HighDimProb.realMatrixToCStarMatrix A <= HighDimProb.realMatrixToCStarMatrix B := by
+  have hAB' : A <= B := HighDimProb.mathlib_le_of_matrixLE hAB
+  rw [← sub_nonneg] at hAB'
+  rw [← sub_nonneg]
+  have hC : 0 <= HighDimProb.realMatrixToCStarMatrix (B - A) :=
+    realMatrixToCStar_nonneg hAB'
+  simpa [HighDimProb.realMatrixToCStarMatrix_sub] using hC
+
+set_option maxHeartbeats 2000000 in
+/-- Strict-positive real functional-calculus logarithm commutes with the
+`CStarMatrix` representation. -/
+theorem realMatrixToCStar_log {n : Nat} {A : Matrix (Fin n) (Fin n) Real}
+    (hA : IsSelfAdjoint A) (hApos : IsStrictlyPositive A) :
+    HighDimProb.realMatrixToCStarMatrix (CFC.log A) =
+      CFC.log (HighDimProb.realMatrixToCStarMatrix A) := by
+  have hspec : ∀ x ∈ spectrum Real A, 0 < x :=
+    (StarOrderedRing.isStrictlyPositive_iff_spectrum_pos (R := Real) A hA).mp hApos
+  have hCont : ContinuousOn Real.log (spectrum Real A) :=
+    Real.continuousOn_log.mono (by intro x hx; exact ne_of_gt (hspec x hx))
+  have hMapEntries : Continuous (fun A : Matrix (Fin n) (Fin n) Real =>
+      A.map (algebraMap Real Complex)) := by
+    fun_prop
+  have hMapCont : Continuous (realMatrixToCStarStarAlgHom (n := n)) := by
+    change Continuous (fun A : Matrix (Fin n) (Fin n) Real =>
+      CStarMatrix.ofMatrix (A.map (algebraMap Real Complex)))
+    simpa [CStarMatrix.ofMatrix_eq_ofMatrixL] using
+      (CStarMatrix.ofMatrixL : Matrix (Fin n) (Fin n) Complex ≃L[Complex]
+        CStarMatrix (Fin n) (Fin n) Complex).continuous.comp hMapEntries
+  simpa [CFC.log] using
+    (StarAlgHom.map_cfc
+      (φ := (realMatrixToCStarStarAlgHom (n := n)))
+      (f := Real.log) (a := A)
+      (hf := hCont)
+      (hφ := hMapCont)
+      (ha := hA)
+      (hφa := HighDimProb.isSelfAdjoint_realMatrixToCStarMatrix hA))
+
+/-- The CFC logarithm of a real self-adjoint matrix is self-adjoint in
+HighDimProb's matrix vocabulary. -/
+theorem isSelfAdjointMatrix_cfc_log {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real}
+    (_hA : HighDimProb.IsSelfAdjointMatrix A) :
+    HighDimProb.IsSelfAdjointMatrix (CFC.log A) := by
+  exact (IsSelfAdjoint.log (a := A)).isHermitian
+
+private theorem cstarMatrix_mem_positiveCone_reflect {n : Nat}
+    {A : CStarMatrix (Fin n) (Fin n) Complex}
+    (hA : A ∈ AddSubmonoid.closure
+      (Set.range fun B : CStarMatrix (Fin n) (Fin n) Complex => star B * B)) :
+    (CStarMatrix.ofMatrix.symm A : Matrix (Fin n) (Fin n) Complex) ∈
+      AddSubmonoid.closure
+        (Set.range fun B : Matrix (Fin n) (Fin n) Complex => star B * B) := by
+  induction hA using AddSubmonoid.closure_induction with
+  | zero =>
+      change (0 : Matrix (Fin n) (Fin n) Complex) ∈
+        AddSubmonoid.closure
+          (Set.range fun B : Matrix (Fin n) (Fin n) Complex => star B * B)
+      exact AddSubmonoid.zero_mem _
+  | add X Y _ _ ihX ihY =>
+      simpa using AddSubmonoid.add_mem _ ihX ihY
+  | mem X hX =>
+      rcases hX with ⟨B, rfl⟩
+      refine AddSubmonoid.subset_closure ?_
+      refine ⟨(CStarMatrix.ofMatrix.symm B : Matrix (Fin n) (Fin n) Complex), ?_⟩
+      ext i j
+      simp [CStarMatrix.mul_apply, CStarMatrix.star_apply, Matrix.mul_apply]
+
+/-- Reflect `CStarMatrix` spectral nonnegativity back to ordinary complex
+matrix positive semidefiniteness. -/
+theorem cstarMatrixOfMatrix_posSemidef_of_nonneg {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Complex)
+    (hA : 0 <= (CStarMatrix.ofMatrix A : CStarMatrix (Fin n) (Fin n) Complex)) :
+    A.PosSemidef := by
+  rw [StarOrderedRing.nonneg_iff] at hA
+  have hCone := cstarMatrix_mem_positiveCone_reflect hA
+  have hNonneg : 0 <= A := by
+    rw [StarOrderedRing.nonneg_iff]
+    simpa using hCone
+  exact Matrix.nonneg_iff_posSemidef.mp hNonneg
+
+/-- Reflect positive semidefiniteness of a complexification back to the real
+matrix. -/
+theorem posSemidef_of_complexification_posSemidef {n : Nat}
+    {A : Matrix (Fin n) (Fin n) Real}
+    (hA : (A.map (algebraMap Real Complex)).PosSemidef) :
+    A.PosSemidef := by
+  have hHerm : A.IsHermitian := by
+    exact Matrix.isHermitian_map_iff (A := A)
+      (f := algebraMap Real Complex) (by intro x; simp) Complex.ofReal_injective |>.mp hA.isHermitian
+  refine Matrix.PosSemidef.of_dotProduct_mulVec_nonneg hHerm ?_
+  intro x
+  have hqC := hA.dotProduct_mulVec_nonneg (fun i => (x i : Complex))
+  have hcast :
+      ((dotProduct (star x) (A.mulVec x) : Real) : Complex) =
+        dotProduct (star fun i => (x i : Complex))
+          ((A.map (algebraMap Real Complex)).mulVec fun i => (x i : Complex)) := by
+    simp [dotProduct, Matrix.mulVec, Finset.mul_sum]
+  have hqC' : 0 <= ((dotProduct (star x) (A.mulVec x) : Real) : Complex) := by
+    rw [hcast]
+    exact hqC
+  exact (RCLike.ofReal_nonneg (K := Complex)).mp hqC'
+
+/-- Reflect order of represented real matrices back to HighDimProb's explicit
+`MatrixLE` vocabulary. -/
+theorem matrixLE_of_realMatrixToCStar_matrixLE {n : Nat}
+    {A B : Matrix (Fin n) (Fin n) Real}
+    (hAB : HighDimProb.realMatrixToCStarMatrix A <=
+      HighDimProb.realMatrixToCStarMatrix B) :
+    HighDimProb.MatrixLE A B := by
+  rw [← sub_nonneg] at hAB
+  have hCSub : 0 <= HighDimProb.realMatrixToCStarMatrix (B - A) := by
+    simpa [HighDimProb.realMatrixToCStarMatrix_sub] using hAB
+  have hComplexPSD : ((B - A).map (algebraMap Real Complex)).PosSemidef := by
+    exact cstarMatrixOfMatrix_posSemidef_of_nonneg
+      ((B - A).map (algebraMap Real Complex))
+      (by simpa [HighDimProb.realMatrixToCStarMatrix] using hCSub)
+  have hRealPSD : (B - A).PosSemidef :=
+    posSemidef_of_complexification_posSemidef hComplexPSD
+  exact HighDimProb.matrixLE_of_mathlib_le (Matrix.le_iff.mpr hRealPSD)
+
+set_option maxHeartbeats 2000000 in
+/-- Provider proof of HighDimProb's real-matrix operator-log monotonicity
+statement. -/
+theorem operatorLogMonotoneOnPositiveMatrices {n : Nat}
+    (M N : Matrix (Fin n) (Fin n) Real) :
+    HighDimProb.operatorLogMonotoneOnPositiveMatrices_statement M N := by
+  intro hM hMpos hN hNpos hMN
+  have hCOrder :
+      HighDimProb.realMatrixToCStarMatrix M <= HighDimProb.realMatrixToCStarMatrix N :=
+    realMatrixToCStar_matrixLE hMN
+  have hCPos : IsStrictlyPositive (HighDimProb.realMatrixToCStarMatrix M) :=
+    realMatrixToCStar_strictlyPositive hMpos
+  have hCLog :
+      CFC.log (HighDimProb.realMatrixToCStarMatrix M) <=
+        CFC.log (HighDimProb.realMatrixToCStarMatrix N) :=
+    CFC.log_le_log hCOrder hCPos
+  have hBackM :
+      HighDimProb.realMatrixToCStarMatrix (CFC.log M) =
+        CFC.log (HighDimProb.realMatrixToCStarMatrix M) :=
+    realMatrixToCStar_log hM hMpos
+  have hBackN :
+      HighDimProb.realMatrixToCStarMatrix (CFC.log N) =
+        CFC.log (HighDimProb.realMatrixToCStarMatrix N) :=
+    realMatrixToCStar_log hN hNpos
+  have hImageOrder :
+      HighDimProb.realMatrixToCStarMatrix (CFC.log M) <=
+        HighDimProb.realMatrixToCStarMatrix (CFC.log N) := by
+    simpa [hBackM, hBackN] using hCLog
+  exact matrixLE_of_realMatrixToCStar_matrixLE hImageOrder
+
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/NaturalHistoryProvider.lean b/HighDimProb/RandomMatrix/NaturalHistoryProvider.lean
new file mode 100644
index 0000000..1b69bc6
--- /dev/null
+++ b/HighDimProb/RandomMatrix/NaturalHistoryProvider.lean
@@ -0,0 +1,61 @@
+import HighDimProb.RandomMatrix.HardboneStatements
+
+/-!
+# Natural-history measurability provider
+
+This module proves the smallest suffix-entry measurability bridge needed by
+the Tropp natural-history statement. It does not prove independence or
+conditional expectation.
+-/
+
+namespace HighDimProb
+
+open HighDimProb
+open MeasureTheory
+open scoped BigOperators
+
+noncomputable section
+
+/-- Natural-history measurability from explicit suffix-entry measurability.
+
+This is the smallest honest bridge for the Tropp natural-history statement:
+the deterministic comparison prefix is constant, and the random suffix is a
+finite sum of explicitly measurable suffix entries. It does not prove
+independence or conditional expectation. -/
+theorem troppNaturalHistoryMeasurable_of_suffix_entry_measurable
+    {Omega : Type*} [MeasurableSpace Omega] {m n : Nat}
+    (theta : Real)
+    (X : Fin m -> HighDimProb.RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (mHist : Fin m -> MeasurableSpace Omega)
+    (hSuffix : forall i : Fin m,
+      forall j : Fin m,
+        ((i.succ : Fin (m + 1)) : Nat) <= (j : Nat) ->
+          forall r c,
+            @Measurable Omega Real (mHist i) inferInstance
+              (fun omega => X j omega r c)) :
+    HighDimProb.troppNaturalHistoryMeasurable_statement theta X K mHist := by
+  intro _hHistSub i r c
+  have hComp : @Measurable Omega Real (mHist i) inferInstance
+      (fun omega => HighDimProb.troppComparisonHistory K i r c) :=
+    measurable_const
+  have hRand : @Measurable Omega Real (mHist i) inferInstance
+      (fun omega => HighDimProb.troppRandomHistory theta X i omega r c) := by
+    simpa [HighDimProb.troppRandomHistory, HighDimProb.randomMatrixSuffixSum,
+      HighDimProb.comparisonMatrixSuffixSum, HighDimProb.scaledRandomMatrixFamily,
+      Matrix.sum_apply]
+      using
+        (Finset.measurable_sum
+          (s := Finset.univ.filter fun j : Fin m =>
+            ((i.succ : Fin (m + 1)) : Nat) <= (j : Nat))
+          (f := fun j : Fin m => fun omega => theta * X j omega r c)
+          (hf := by
+            intro j hj
+            have hj' : ((i.succ : Fin (m + 1)) : Nat) <= (j : Nat) := by
+              simpa using hj
+            exact (hSuffix i j hj' r c).const_mul theta))
+  simpa [HighDimProb.troppStateHistory] using hComp.add hRand
+
+end
+
+end HighDimProb
diff --git a/HighDimProb/RandomMatrix/SupportProvider.lean b/HighDimProb/RandomMatrix/SupportProvider.lean
new file mode 100644
index 0000000..e5497e7
--- /dev/null
+++ b/HighDimProb/RandomMatrix/SupportProvider.lean
@@ -0,0 +1,69 @@
+import HighDimProb.RandomMatrix.HardboneStatements
+import HighDimProb.RandomMatrix.Spectral
+import HighDimProb.RandomMatrix.TraceExp
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
+
+/-!
+# Support-side trace-exponential providers
+
+This module proves the first honest support certificate needed by the
+support/effective-rank trace-exponential lane: the ambient identity matrix
+already dominates `matrixExp A` after scaling by `exp (lambdaMaxOrdered A)`.
+
+It does not construct smaller support projections, prove excess-support
+certificates, or prove any Golden-Thompson, Lieb, or Matrix Bernstein fact.
+-/
+
+namespace HighDimProb
+
+noncomputable section
+
+open scoped MatrixOrder Matrix.Norms.Operator
+
+private theorem spectrum_real_le_lambdaMaxOrdered {n : Nat}
+    {A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real}
+    (hA : HighDimProb.IsSelfAdjointMatrix A) {x : Real}
+    (hx : x ∈ spectrum Real A) :
+    x <= HighDimProb.lambdaMaxOrdered A hA := by
+  classical
+  let e : Fin (Fintype.card (Fin (n + 1))) ≃ Fin (n + 1) :=
+    Fintype.equivOfCardEq (by simp)
+  rw [hA.spectrum_real_eq_range_eigenvalues] at hx
+  rcases hx with ⟨i, rfl⟩
+  simpa [HighDimProb.lambdaMaxOrdered, Matrix.IsHermitian.eigenvalues, e] using
+    hA.eigenvalues₀_antitone (Fin.zero_le (e.symm i))
+
+/-- Ambient identity-support domination for the matrix exponential.
+
+This is the smallest support-certificate provider in the support/effective-rank
+lane. It reuses the ordered lambda-max endpoint from HighDimProb, applies the
+scalar inequality `exp x <= exp lambdaMax` on the spectrum of one self-adjoint
+matrix, lifts it through `cfc_mono`, and reflects the resulting Mathlib matrix
+order back into HighDimProb's `MatrixLE` vocabulary. -/
+theorem matrixExpSupportDomination_identity {n : Nat}
+    (A : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) :
+    HighDimProb.matrixExpSupportDomination_identity_statement A := by
+  intro hA
+  unfold HighDimProb.MatrixExpSupportDomination
+  have hle :
+      HighDimProb.matrixExp A <=
+        SMul.smul (Real.exp (HighDimProb.lambdaMaxOrdered A hA))
+          (1 : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) := by
+    calc
+      HighDimProb.matrixExp A = cfc Real.exp A := by
+        symm
+        simpa [HighDimProb.matrixExp] using
+          (CFC.real_exp_eq_normedSpace_exp (a := A) hA.isSelfAdjoint)
+      _ <= cfc (fun _ : Real => Real.exp (HighDimProb.lambdaMaxOrdered A hA)) A := by
+        exact cfc_mono (a := A) (fun x hx =>
+          Real.exp_le_exp.mpr (spectrum_real_le_lambdaMaxOrdered hA hx))
+      _ = SMul.smul (Real.exp (HighDimProb.lambdaMaxOrdered A hA))
+            (1 : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) := by
+        simpa [Algebra.algebraMap_eq_smul_one] using
+          (cfc_const (R := Real)
+            (r := Real.exp (HighDimProb.lambdaMaxOrdered A hA)) (a := A))
+  exact HighDimProb.matrixLE_of_mathlib_le hle
+
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/TraceExpDerivative.lean b/HighDimProb/RandomMatrix/TraceExpDerivative.lean
new file mode 100644
index 0000000..a6fef93
--- /dev/null
+++ b/HighDimProb/RandomMatrix/TraceExpDerivative.lean
@@ -0,0 +1,580 @@
+import Mathlib.Analysis.Calculus.FDeriv.Pow
+import Mathlib.Analysis.Calculus.FDeriv.Linear
+import Mathlib.Analysis.Calculus.Deriv.Comp
+import Mathlib.Analysis.Calculus.Deriv.Linear
+import Mathlib.Analysis.Calculus.Deriv.Add
+import Mathlib.Analysis.Calculus.Deriv.Mul
+import Mathlib.Analysis.Calculus.SmoothSeries
+import Mathlib.Analysis.Normed.Algebra.MatrixExponential
+import Mathlib.Analysis.Normed.Module.FiniteDimension
+import Mathlib.Analysis.SpecificLimits.Normed
+import Mathlib.Data.Real.Basic
+import Mathlib.LinearAlgebra.Matrix.Trace
+
+/-!
+# Trace derivatives for noncommutative matrix powers
+
+This module provides the finite-polynomial trace derivative used as the
+termwise ingredient for the noncommutative trace-exponential derivative route.
+It proves the affine derivative of `trace (exp (X + t • C))` by summing the
+finite-polynomial derivative route. It does not prove the Duhamel integral
+formula.
+-/
+
+namespace HighDimProb
+
+open scoped Matrix.Norms.Operator RightActions
+
+noncomputable section
+
+private theorem trace_pow_deriv_trace_sum_eq_trace_mul_pow
+    {n k : Nat} (A C : Matrix (Fin n) (Fin n) Real) :
+    Finset.sum (Finset.range k)
+      (fun i => Matrix.trace (A ^ (k - 1 - i) * C * A ^ i)) =
+      (k : Real) * Matrix.trace (C * A ^ (k - 1)) := by
+  trans Finset.sum (Finset.range k) (fun _ => Matrix.trace (C * A ^ (k - 1)))
+  . apply Finset.sum_congr rfl
+    intro i hi
+    have hi' : i < k := Finset.mem_range.mp hi
+    have hi_le_pred : i <= k.pred := Nat.le_pred_of_lt hi'
+    have hi_le : i <= k - 1 := by
+      simpa [Nat.pred_eq_sub_one] using hi_le_pred
+    calc
+      Matrix.trace (A ^ (k - 1 - i) * C * A ^ i)
+          = Matrix.trace (A ^ i * A ^ (k - 1 - i) * C) := by
+              rw [Matrix.trace_mul_cycle]
+      _ = Matrix.trace (C * (A ^ i * A ^ (k - 1 - i))) := by
+              rw [Matrix.trace_mul_comm]
+      _ = Matrix.trace (C * A ^ (k - 1)) := by
+              congr 1
+              rw [<- pow_add]
+              have hsum : i + (k - 1 - i) = k - 1 := Nat.add_sub_of_le hi_le
+              exact congrArg (fun m : Nat => C * A ^ m) hsum
+  . rw [Finset.sum_const, Finset.card_range]
+    simp [nsmul_eq_mul]
+/-- Frechet derivative of `X ↦ trace (X ^ k)` in the noncommutative sum form.
+
+This packages Mathlib's noncommutative power derivative into a reusable theorem
+with a matrix-to-scalar continuous linear map target.
+-/
+theorem hasFDerivAt_trace_pow_sum
+    {n k : Nat} (A : Matrix (Fin n) (Fin n) Real) :
+    HasFDerivAt
+      (fun X : Matrix (Fin n) (Fin n) Real => Matrix.trace (X ^ k))
+      (LinearMap.toContinuousLinearMap
+        (Finset.sum (Finset.range k) fun i =>
+          (Matrix.traceLinearMap (Fin n) Real Real).comp
+            ((LinearMap.mulLeft Real (A ^ (k - 1 - i))).comp
+              (LinearMap.mulRight Real (A ^ i)))))
+      A := by
+  have hId : HasFDerivAt (fun X : Matrix (Fin n) (Fin n) Real => X)
+      (ContinuousLinearMap.id Real (Matrix (Fin n) (Fin n) Real)) A := by
+    simpa using (hasFDerivAt_id A)
+  have hPowF := hId.fun_pow' k
+  have hTraceF :=
+    ((LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)).hasFDerivAt.comp
+      A hPowF)
+  refine hTraceF.congr_fderiv ?_
+  ext H
+  simp [ContinuousLinearMap.comp_apply, ContinuousLinearMap.sum_apply,
+    Matrix.traceLinearMap_apply, LinearMap.comp_apply, LinearMap.mulLeft_apply,
+    LinearMap.mulRight_apply, MulOpposite.smul_eq_mul_unop, mul_assoc]
+
+/-- Frechet derivative of `X ↦ trace (X ^ k)` after collapsing the cyclic sum.
+
+The derivative map is the scalar multiple of right multiplication by A ^ (k - 1)
+followed by the trace.
+-/
+theorem hasFDerivAt_trace_pow
+    {n k : Nat} (A : Matrix (Fin n) (Fin n) Real) :
+    HasFDerivAt
+      (fun X : Matrix (Fin n) (Fin n) Real => Matrix.trace (X ^ k))
+      ((k : Real) •
+        ((LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)).comp
+          (LinearMap.toContinuousLinearMap (LinearMap.mulRight Real (A ^ (k - 1))))))
+      A := by
+  have hsum := hasFDerivAt_trace_pow_sum (A := A) (k := k)
+  refine hsum.congr_fderiv ?_
+  ext H
+  simp [ContinuousLinearMap.sum_apply, Matrix.traceLinearMap_apply, LinearMap.comp_apply,
+    LinearMap.mulRight_apply, smul_eq_mul]
+  simpa [mul_assoc] using
+    trace_pow_deriv_trace_sum_eq_trace_mul_pow (A := A) (C := H) (k := k)
+
+/-- Derivative of the trace of a noncommutative matrix power along an affine line.
+
+Mathlib's `HasFDerivAt.fun_pow'` gives the noncommutative Frechet derivative of
+`A => A ^ k` as a cyclic sum. Taking the trace collapses the cyclic sum to
+`k * trace (C * A ^ (k - 1))`.
+
+This is a finite-polynomial ingredient for the trace-exponential derivative
+route; it is not the Duhamel integral formula and it is not the derivative of
+`trace (NormedSpace.exp _)`.
+-/
+theorem hasDerivAt_trace_pow_add_smul_const
+    {n k : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real) :
+    HasDerivAt
+      (fun u : Real => Matrix.trace ((X + SMul.smul u C) ^ k))
+      ((k : Real) * Matrix.trace (C * (X + SMul.smul t C) ^ (k - 1)))
+      t := by
+  let A : Matrix (Fin n) (Fin n) Real := X + SMul.smul t C
+  have hAffine : HasDerivAt (fun u : Real => X + SMul.smul u C) C t := by
+    have hConst : HasDerivAt (fun _ : Real => X) 0 t := hasDerivAt_const t X
+    have hLin : HasDerivAt (fun u : Real => SMul.smul u C) C t := by
+      simpa using
+        (HasDerivAt.smul_const
+          (hasDerivAt_id t : HasDerivAt (fun u : Real => u) 1 t) C)
+    change HasDerivAt ((fun _ : Real => X) + (fun u : Real => SMul.smul u C)) C t
+    simpa using hConst.add hLin
+  have hDeriv := (hasFDerivAt_trace_pow (A := A) (k := k)).comp_hasDerivAt t hAffine
+  simpa [A, ContinuousLinearMap.comp_apply, Matrix.traceLinearMap_apply,
+    LinearMap.mulRight_apply, smul_eq_mul] using hDeriv
+
+/-- Termwise derivative of the finite truncated trace-exponential series along an affine line.
+
+This is a finite truncation only: it packages the polynomial power derivative above into a
+finite sum with exponential-series coefficients. It does not prove the derivative of the
+infinite trace exponential series.
+-/
+theorem hasDerivAt_trace_exp_trunc_add_smul_const
+    {n m : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real) :
+    HasDerivAt
+      (fun u : Real =>
+        Finset.sum (Finset.range m)
+          (fun k => (1 / (Nat.factorial k : Real)) *
+            Matrix.trace ((X + SMul.smul u C) ^ k)))
+      (Finset.sum (Finset.range m)
+        (fun k => (1 / (Nat.factorial k : Real)) *
+          ((k : Real) * Matrix.trace (C * (X + SMul.smul t C) ^ (k - 1)))))
+      t := by
+  simpa using
+    (HasDerivAt.fun_sum
+      (u := Finset.range m)
+      (A := fun k u =>
+        (1 / (Nat.factorial k : Real)) *
+          Matrix.trace ((X + SMul.smul u C) ^ k))
+      (A' := fun k =>
+        (1 / (Nat.factorial k : Real)) *
+          ((k : Real) * Matrix.trace (C * (X + SMul.smul t C) ^ (k - 1))))
+      (x := t)
+      (fun k hk =>
+        (hasDerivAt_trace_pow_add_smul_const (k := k) X C t).const_mul
+          (1 / (Nat.factorial k : Real))))
+
+/-- Algebraic normalization of the differentiated truncated trace-exponential sum. -/
+private theorem trace_exp_trunc_deriv_weight_succ
+    (x : Real) (k : Nat) :
+    (1 / (Nat.factorial (k + 1) : Real)) * ((k + 1 : Real) * x) =
+    (1 / (Nat.factorial k : Real)) * x := by
+  rw [Nat.factorial_succ]
+  field_simp [Nat.factorial_ne_zero]
+  norm_num [Nat.cast_add, Nat.cast_mul, mul_add, add_mul, mul_assoc, mul_left_comm, mul_comm]
+
+/-- Continuous-linear-map version of the factorial weight normalization. -/
+private theorem trace_exp_trunc_deriv_weight_succ_clm
+    {E F : Type*} [NormedAddCommGroup E] [NormedSpace Real E]
+    [NormedAddCommGroup F] [NormedSpace Real F]
+    (L : E →L[Real] F) (k : Nat) :
+    (1 / (Nat.factorial (k + 1) : Real)) • ((k + 1 : Real) • L) =
+      (1 / (Nat.factorial k : Real)) • L := by
+  have hcoef : (1 / (Nat.factorial (k + 1) : Real)) * (k + 1 : Real) =
+      1 / (Nat.factorial k : Real) := by
+    simpa using (trace_exp_trunc_deriv_weight_succ (x := (1 : Real)) k)
+  ext x
+  simpa [ContinuousLinearMap.smul_apply, smul_smul] using
+    congrArg (fun a : Real => a • L x) hcoef
+/-- Frechet derivative of the finite truncated trace-exponential polynomial. -/
+theorem hasFDerivAt_trace_exp_trunc
+    {n m : Nat} (A : Matrix (Fin n) (Fin n) Real) :
+    HasFDerivAt
+      (fun X : Matrix (Fin n) (Fin n) Real =>
+        Finset.sum (Finset.range m)
+          (fun k => (1 / (Nat.factorial k : Real)) * Matrix.trace (X ^ k)))
+      (Finset.sum (Finset.range m)
+        (fun k =>
+          SMul.smul (1 / (Nat.factorial k : Real))
+            (SMul.smul (k : Real)
+              ((LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)).comp
+                (LinearMap.toContinuousLinearMap (LinearMap.mulRight Real (A ^ (k - 1))))))))
+      A := by
+  refine HasFDerivAt.fun_sum (u := Finset.range m) ?_
+  intro k hk
+  simpa [smul_eq_mul] using
+    (hasFDerivAt_trace_pow (A := A) (k := k)).const_smul
+      (1 / (Nat.factorial k : Real))
+
+/-- Algebraic normalization of the shifted Frechet derivative sum for trace-exp truncations. -/
+private theorem trace_exp_trunc_fderiv_sum_eq_shifted
+    {n m : Nat} (A : Matrix (Fin n) (Fin n) Real) :
+    Finset.sum (Finset.range (m + 1))
+      (fun k =>
+        SMul.smul (1 / (Nat.factorial k : Real))
+          (SMul.smul (k : Real)
+            ((LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)).comp
+              (LinearMap.toContinuousLinearMap (LinearMap.mulRight Real (A ^ (k - 1))))))) =
+    Finset.sum (Finset.range m)
+      (fun j =>
+        SMul.smul (1 / (Nat.factorial j : Real))
+          ((LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)).comp
+            (LinearMap.toContinuousLinearMap (LinearMap.mulRight Real (A ^ j))))) := by
+  induction m with
+  | zero =>
+      simp
+      have hzero :
+          SMul.smul (0 : Real)
+            ((LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)).comp
+              (LinearMap.toContinuousLinearMap LinearMap.id)) = 0 := by
+        exact zero_smul Real _
+      rw [hzero]
+      exact smul_zero (1 : Real)
+  | succ m ih =>
+      rw [Finset.sum_range_succ]
+      conv_rhs => rw [Finset.sum_range_succ]
+      rw [ih]
+      congr 1
+      simpa [Nat.succ_eq_add_one, Nat.add_comm, Nat.add_left_comm, Nat.add_assoc,
+        Nat.add_sub_cancel] using
+        (trace_exp_trunc_deriv_weight_succ_clm
+          (((LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)).comp
+            (LinearMap.toContinuousLinearMap (LinearMap.mulRight Real (A ^ m))))) m)
+
+/-- Frechet derivative of the shifted truncated trace-exponential polynomial. -/
+theorem hasFDerivAt_trace_exp_trunc_succ
+    {n m : Nat} (A : Matrix (Fin n) (Fin n) Real) :
+    HasFDerivAt
+      (fun X : Matrix (Fin n) (Fin n) Real =>
+        Finset.sum (Finset.range (m + 1))
+          (fun k => (1 / (Nat.factorial k : Real)) * Matrix.trace (X ^ k)))
+      (Finset.sum (Finset.range m)
+        (fun j =>
+          SMul.smul (1 / (Nat.factorial j : Real))
+            ((LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)).comp
+              (LinearMap.toContinuousLinearMap (LinearMap.mulRight Real (A ^ j))))))
+      A := by
+  have h := hasFDerivAt_trace_exp_trunc (A := A) (m := m + 1)
+  refine h.congr_fderiv ?_
+  simpa using trace_exp_trunc_fderiv_sum_eq_shifted (A := A) (m := m)
+
+/-- Algebraic normalization for the shifted differentiated truncated trace-exponential sum. -/
+theorem trace_exp_trunc_deriv_sum_eq_shifted
+    {n m : Nat} (A C : Matrix (Fin n) (Fin n) Real) :
+    Finset.sum (Finset.range (m + 1))
+      (fun k => (1 / (Nat.factorial k : Real)) *
+        ((k : Real) * Matrix.trace (C * A ^ (k - 1)))) =
+    Finset.sum (Finset.range m)
+      (fun j => (1 / (Nat.factorial j : Real)) * Matrix.trace (C * A ^ j)) := by
+  induction m with
+  | zero =>
+      simp
+  | succ m ih =>
+      rw [Finset.sum_range_succ]
+      conv_rhs => rw [Finset.sum_range_succ]
+      rw [ih]
+      congr 1
+      simpa [Nat.add_comm, Nat.add_left_comm, Nat.add_assoc, mul_assoc, mul_left_comm,
+        mul_comm] using
+        (trace_exp_trunc_deriv_weight_succ (x := Matrix.trace (C * A ^ m)) m)
+
+/-- Derivative of the truncated trace exponential with the shifted normalized sum on the right. -/
+theorem hasDerivAt_trace_exp_trunc_succ_add_smul_const
+    {n m : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real) :
+    HasDerivAt
+      (fun u : Real =>
+        Finset.sum (Finset.range (m + 1))
+          (fun k => (1 / (Nat.factorial k : Real)) *
+            Matrix.trace ((X + SMul.smul u C) ^ k)))
+      (Finset.sum (Finset.range m)
+        (fun j => (1 / (Nat.factorial j : Real)) *
+          Matrix.trace (C * (X + SMul.smul t C) ^ j)))
+      t := by
+  have h := hasDerivAt_trace_exp_trunc_add_smul_const (m := m + 1) X C t
+  rw [trace_exp_trunc_deriv_sum_eq_shifted (A := X + SMul.smul t C) (C := C)] at h
+  exact h
+
+private theorem matrix_norm_one_le_one {n : Nat} :
+    ‖(1 : Matrix (Fin n) (Fin n) Real)‖ ≤ 1 := by
+  rw [← Matrix.diagonal_one]
+  simpa using
+    (Matrix.linfty_opNorm_diagonal (m := Fin n) (α := Real) (fun _ : Fin n => (1 : Real))).trans_le
+      (pi_norm_const_le (ι := Fin n) (a := (1 : Real)))
+
+private theorem matrix_norm_pow_le_of_norm_le
+    {n j : Nat} {A : Matrix (Fin n) (Fin n) Real} {R : Real}
+    (hR0 : 0 ≤ R) (hA : ‖A‖ ≤ R) :
+    ‖A ^ j‖ ≤ R ^ j := by
+  induction j with
+  | zero =>
+      simpa using (matrix_norm_one_le_one (n := n))
+  | succ j ih =>
+      calc
+        ‖A ^ (j + 1)‖ = ‖A ^ j * A‖ := by rw [pow_succ]
+        _ ≤ ‖A ^ j‖ * ‖A‖ := Matrix.linfty_opNorm_mul (A ^ j) A
+        _ ≤ R ^ j * R := mul_le_mul ih hA (norm_nonneg A) (pow_nonneg hR0 j)
+        _ = R ^ (j + 1) := by rw [pow_succ]
+
+private theorem norm_affine_le_of_mem_Ioo
+    {n : Nat} (X C : Matrix (Fin n) (Fin n) Real) {t y : Real}
+    (hy : y ∈ Set.Ioo (t - 1) (t + 1)) :
+    ‖X + SMul.smul y C‖ ≤ ‖X‖ + (|t| + 1) * ‖C‖ := by
+  have hy_abs : |y| ≤ |t| + 1 := by
+    rw [abs_le]
+    constructor <;> linarith [hy.1, hy.2, le_abs_self t, neg_le_abs t]
+  calc
+    ‖X + SMul.smul y C‖ ≤ ‖X‖ + ‖SMul.smul y C‖ := norm_add_le X (SMul.smul y C)
+    _ = ‖X‖ + |y| * ‖C‖ := by
+      congr 1
+      change ‖y • C‖ = |y| * ‖C‖
+      rw [norm_smul, Real.norm_eq_abs]
+    _ ≤ ‖X‖ + (|t| + 1) * ‖C‖ := by gcongr
+
+private theorem trace_exp_shifted_deriv_term_norm_le
+    {n j : Nat} (X C : Matrix (Fin n) (Fin n) Real) {t y : Real}
+    (hy : y ∈ Set.Ioo (t - 1) (t + 1)) :
+    let traceCLM : Matrix (Fin n) (Fin n) Real →L[Real] Real :=
+      LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)
+    let R : Real := ‖X‖ + (|t| + 1) * ‖C‖
+    ‖(1 / (Nat.factorial j : Real)) *
+        Matrix.trace (C * (X + SMul.smul y C) ^ j)‖ ≤
+      (‖traceCLM‖ * ‖C‖) * (R ^ j / (Nat.factorial j : Real)) := by
+  intro traceCLM R
+  have hR0 : 0 ≤ R := by
+    dsimp [R]
+    positivity
+  have hA : ‖X + SMul.smul y C‖ ≤ R := by
+    simpa [R] using norm_affine_le_of_mem_Ioo X C hy
+  have hpow : ‖(X + SMul.smul y C) ^ j‖ ≤ R ^ j :=
+    matrix_norm_pow_le_of_norm_le hR0 hA
+  have hmul : ‖C * (X + SMul.smul y C) ^ j‖ ≤ ‖C‖ * R ^ j := by
+    exact (Matrix.linfty_opNorm_mul C ((X + SMul.smul y C) ^ j)).trans
+      (mul_le_mul_of_nonneg_left hpow (norm_nonneg C))
+  have htrace : ‖Matrix.trace (C * (X + SMul.smul y C) ^ j)‖ ≤
+      ‖traceCLM‖ * (‖C‖ * R ^ j) := by
+    calc
+      ‖Matrix.trace (C * (X + SMul.smul y C) ^ j)‖ =
+          ‖traceCLM (C * (X + SMul.smul y C) ^ j)‖ := by
+            simp [traceCLM, Matrix.traceLinearMap_apply]
+      _ ≤ ‖traceCLM‖ * ‖C * (X + SMul.smul y C) ^ j‖ := traceCLM.le_opNorm _
+      _ ≤ ‖traceCLM‖ * (‖C‖ * R ^ j) := by
+            exact mul_le_mul_of_nonneg_left hmul (norm_nonneg traceCLM)
+  have hcoeff_nonneg : 0 ≤ (1 / (Nat.factorial j : Real)) := by positivity
+  calc
+    ‖(1 / (Nat.factorial j : Real)) *
+        Matrix.trace (C * (X + SMul.smul y C) ^ j)‖
+        = (1 / (Nat.factorial j : Real)) *
+            ‖Matrix.trace (C * (X + SMul.smul y C) ^ j)‖ := by
+              rw [norm_mul, Real.norm_of_nonneg hcoeff_nonneg]
+    _ ≤ (1 / (Nat.factorial j : Real)) * (‖traceCLM‖ * (‖C‖ * R ^ j)) := by
+          exact mul_le_mul_of_nonneg_left htrace hcoeff_nonneg
+    _ = (‖traceCLM‖ * ‖C‖) * (R ^ j / (Nat.factorial j : Real)) := by
+          ring
+
+/-- Termwise derivative of the shifted trace-exponential tail. -/
+theorem hasDerivAt_trace_exp_shifted_term_add_smul_const
+    {n j : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real) :
+    HasDerivAt
+      (fun u : Real =>
+        (1 / (Nat.factorial (j + 1) : Real)) *
+          Matrix.trace ((X + SMul.smul u C) ^ (j + 1)))
+      ((1 / (Nat.factorial j : Real)) *
+          Matrix.trace (C * (X + SMul.smul t C) ^ j))
+      t := by
+  have h :=
+    (hasDerivAt_trace_pow_add_smul_const (n := n) (k := j + 1) X C t).const_mul
+      (1 / (Nat.factorial (j + 1) : Real))
+  exact h.congr_deriv (by
+    simpa [Nat.add_sub_cancel] using
+      (trace_exp_trunc_deriv_weight_succ
+        (x := Matrix.trace (C * (X + SMul.smul t C) ^ j)) j))
+
+/-- The trace of the matrix exponential is the sum of the traced power series. -/
+theorem hasSum_trace_exp_series
+    {n : Nat} (A : Matrix (Fin n) (Fin n) Real) :
+    HasSum
+      (fun k : Nat => (1 / (Nat.factorial k : Real)) * Matrix.trace (A ^ k))
+      (Matrix.trace (NormedSpace.exp A)) := by
+  let traceCLM : Matrix (Fin n) (Fin n) Real →L[Real] Real :=
+    LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)
+  have hExp :
+      HasSum
+        (fun k : Nat => ((Nat.factorial k : Real)⁻¹) • A ^ k)
+        (NormedSpace.exp A) :=
+    NormedSpace.exp_series_hasSum_exp' (𝕂 := Real) A
+  have hTrace :
+      HasSum
+        (fun k : Nat => ((Nat.factorial k : Real)⁻¹) • traceCLM (A ^ k))
+        (traceCLM (NormedSpace.exp A)) := by
+    simpa using traceCLM.hasSum hExp
+  simpa [traceCLM, one_div, Matrix.traceLinearMap_apply, smul_eq_mul] using hTrace
+
+private theorem summable_trace_exp_shifted_tail_terms
+    {n : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real) :
+    Summable
+      (fun j : Nat =>
+        (1 / (Nat.factorial (j + 1) : Real)) *
+          Matrix.trace ((X + SMul.smul t C) ^ (j + 1))) := by
+  have hfull :
+      Summable
+        (fun k : Nat =>
+          (1 / (Nat.factorial k : Real)) *
+            Matrix.trace ((X + SMul.smul t C) ^ k)) :=
+    (hasSum_trace_exp_series (A := X + SMul.smul t C)).summable
+  have htail := Summable.comp_injective hfull Nat.succ_injective
+  simpa [Function.comp_def, Nat.succ_eq_add_one] using htail
+
+private theorem summable_trace_exp_shifted_deriv_majorant
+    {n : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real) :
+    let traceCLM : Matrix (Fin n) (Fin n) Real →L[Real] Real :=
+      LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)
+    let R : Real := ‖X‖ + (|t| + 1) * ‖C‖
+    Summable
+      (fun j : Nat => ‖traceCLM‖ * ‖C‖ * (R ^ j / (Nat.factorial j : Real))) := by
+  intro traceCLM R
+  have hpow : Summable (fun j : Nat => R ^ j / (Nat.factorial j : Real)) :=
+    Real.summable_pow_div_factorial R
+  simpa [mul_assoc] using Summable.mul_left (‖traceCLM‖ * ‖C‖) hpow
+
+/-- Termwise derivative of the shifted trace-exponential tail. -/
+theorem hasDerivAt_tsum_trace_exp_shifted_tail_add_smul_const
+    {n : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real) :
+    HasDerivAt
+      (fun z : Real => ∑' j : Nat,
+        (1 / (Nat.factorial (j + 1) : Real)) *
+          Matrix.trace ((X + SMul.smul z C) ^ (j + 1)))
+      (∑' j : Nat,
+        (1 / (Nat.factorial j : Real)) *
+          Matrix.trace (C * (X + SMul.smul t C) ^ j))
+      t := by
+  let s : Set Real := Set.Ioo (t - 1) (t + 1)
+  let traceCLM : Matrix (Fin n) (Fin n) Real →L[Real] Real :=
+    LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)
+  let R : Real := ‖X‖ + (|t| + 1) * ‖C‖
+  let u : Nat → Real :=
+    fun j => ‖traceCLM‖ * ‖C‖ * (R ^ j / (Nat.factorial j : Real))
+  let g : Nat → Real → Real :=
+    fun j z =>
+      (1 / (Nat.factorial (j + 1) : Real)) *
+        Matrix.trace ((X + SMul.smul z C) ^ (j + 1))
+  let g' : Nat → Real → Real :=
+    fun j z =>
+      (1 / (Nat.factorial j : Real)) *
+        Matrix.trace (C * (X + SMul.smul z C) ^ j)
+  have hu : Summable u := by
+    simpa [u, traceCLM, R] using
+      summable_trace_exp_shifted_deriv_majorant X C t
+  have hs_open : IsOpen s := by
+    simpa [s] using (isOpen_Ioo : IsOpen (Set.Ioo (t - 1) (t + 1)))
+  have hs_preconnected : IsPreconnected s := by
+    simpa [s] using (isPreconnected_Ioo : IsPreconnected (Set.Ioo (t - 1) (t + 1)))
+  have ht_mem : t ∈ s := by
+    dsimp [s]
+    constructor <;> linarith
+  have hg : ∀ j : Nat, ∀ y ∈ s, HasDerivAt (g j) (g' j y) y := by
+    intro j y hy
+    simpa [g, g'] using
+      (hasDerivAt_trace_exp_shifted_term_add_smul_const (j := j) X C y)
+  have hg' : ∀ j : Nat, ∀ y ∈ s, ‖g' j y‖ ≤ u j := by
+    intro j y hy
+    have hy' : y ∈ Set.Ioo (t - 1) (t + 1) := by simpa [s] using hy
+    simpa [g', u, traceCLM, R] using
+      (trace_exp_shifted_deriv_term_norm_le (j := j) X C hy')
+  have hg0 : Summable fun j : Nat => g j t := by
+    simpa [g] using summable_trace_exp_shifted_tail_terms X C t
+  have h :=
+    hasDerivAt_tsum_of_isPreconnected
+      (u := u) (g := g) (g' := g') (t := s) (y₀ := t) (y := t)
+      hu hs_open hs_preconnected hg hg' ht_mem hg0 ht_mem
+  simpa [g, g'] using h
+/-- The trace of left multiplication of the matrix exponential is the sum of the
+traced left-multiplied power series. -/
+theorem hasSum_trace_mul_exp_series
+    {n : Nat} (A C : Matrix (Fin n) (Fin n) Real) :
+    HasSum
+      (fun k : Nat => (1 / (Nat.factorial k : Real)) * Matrix.trace (C * A ^ k))
+      (Matrix.trace (C * NormedSpace.exp A)) := by
+  let leftMulCLM : Matrix (Fin n) (Fin n) Real →L[Real] Matrix (Fin n) (Fin n) Real :=
+    LinearMap.toContinuousLinearMap (LinearMap.mulLeft Real C)
+  let traceCLM : Matrix (Fin n) (Fin n) Real →L[Real] Real :=
+    LinearMap.toContinuousLinearMap (Matrix.traceLinearMap (Fin n) Real Real)
+  let traceMulCLM : Matrix (Fin n) (Fin n) Real →L[Real] Real :=
+    traceCLM.comp leftMulCLM
+  have hExp :
+      HasSum
+        (fun k : Nat => ((Nat.factorial k : Real)⁻¹) • A ^ k)
+        (NormedSpace.exp A) :=
+    NormedSpace.exp_series_hasSum_exp' (𝕂 := Real) A
+  have hTraceMul :
+      HasSum
+        (fun k : Nat => ((Nat.factorial k : Real)⁻¹) • traceMulCLM (A ^ k))
+        (traceMulCLM (NormedSpace.exp A)) := by
+    simpa using traceMulCLM.hasSum hExp
+  simpa [traceMulCLM, traceCLM, leftMulCLM, one_div, Matrix.traceLinearMap_apply,
+    LinearMap.mulLeft_apply, ContinuousLinearMap.comp_apply, smul_eq_mul] using hTraceMul
+
+/-- `tsum` form of `hasSum_trace_exp_series`. -/
+theorem trace_exp_eq_tsum_trace_power
+    {n : Nat} (A : Matrix (Fin n) (Fin n) Real) :
+    Matrix.trace (NormedSpace.exp A) =
+      ∑' k : Nat, (1 / (Nat.factorial k : Real)) * Matrix.trace (A ^ k) := by
+  exact (hasSum_trace_exp_series A).tsum_eq.symm
+
+/-- `tsum` form of `hasSum_trace_mul_exp_series`. -/
+theorem trace_mul_exp_eq_tsum_trace_mul_power
+    {n : Nat} (A C : Matrix (Fin n) (Fin n) Real) :
+    Matrix.trace (C * NormedSpace.exp A) =
+      ∑' k : Nat, (1 / (Nat.factorial k : Real)) * Matrix.trace (C * A ^ k) := by
+  exact (hasSum_trace_mul_exp_series A C).tsum_eq.symm
+
+/-- Derivative of the affine trace exponential along a constant direction. -/
+theorem hasDerivAt_trace_exp_add_smul_const
+    {n : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real) :
+    HasDerivAt
+      (fun u : Real => Matrix.trace (NormedSpace.exp (X + SMul.smul u C)))
+      (Matrix.trace (C * NormedSpace.exp (X + SMul.smul t C)))
+      t := by
+  have htail :
+      HasDerivAt
+        (fun u : Real =>
+          Matrix.trace (1 : Matrix (Fin n) (Fin n) Real) +
+            ∑' j : Nat,
+              (1 / (Nat.factorial (j + 1) : Real)) *
+                Matrix.trace ((X + SMul.smul u C) ^ (j + 1)))
+        (∑' j : Nat,
+          (1 / (Nat.factorial j : Real)) *
+            Matrix.trace (C * (X + SMul.smul t C) ^ j))
+        t :=
+    (hasDerivAt_tsum_trace_exp_shifted_tail_add_smul_const X C t).const_add
+      (Matrix.trace (1 : Matrix (Fin n) (Fin n) Real))
+  have htrace :
+      HasDerivAt
+        (fun u : Real => Matrix.trace (NormedSpace.exp (X + SMul.smul u C)))
+        (∑' j : Nat,
+          (1 / (Nat.factorial j : Real)) *
+            Matrix.trace (C * (X + SMul.smul t C) ^ j))
+        t := by
+    refine htail.congr_of_eventuallyEq (Filter.Eventually.of_forall ?_)
+    intro u
+    calc
+      Matrix.trace (NormedSpace.exp (X + SMul.smul u C))
+          = ∑' k : Nat,
+              (1 / (Nat.factorial k : Real)) *
+                Matrix.trace ((X + SMul.smul u C) ^ k) := by
+              simpa using trace_exp_eq_tsum_trace_power (A := X + SMul.smul u C)
+      _ = Matrix.trace (1 : Matrix (Fin n) (Fin n) Real) +
+            ∑' j : Nat,
+              (1 / (Nat.factorial (j + 1) : Real)) *
+                Matrix.trace ((X + SMul.smul u C) ^ (j + 1)) := by
+            have hsum :
+                Summable
+                  (fun k : Nat =>
+                    (1 / (Nat.factorial k : Real)) *
+                      Matrix.trace ((X + SMul.smul u C) ^ k)) :=
+              (hasSum_trace_exp_series (A := X + SMul.smul u C)).summable
+            simpa [pow_zero, Nat.succ_eq_add_one] using hsum.tsum_eq_zero_add
+  exact htrace.congr_deriv
+    (trace_mul_exp_eq_tsum_trace_mul_power (A := X + SMul.smul t C) (C := C)).symm
+
+
+
+end
+
+end HighDimProb
diff --git a/HighDimProb/RandomMatrix/TraceExpIntegrabilityProvider.lean b/HighDimProb/RandomMatrix/TraceExpIntegrabilityProvider.lean
new file mode 100644
index 0000000..6f5f486
--- /dev/null
+++ b/HighDimProb/RandomMatrix/TraceExpIntegrabilityProvider.lean
@@ -0,0 +1,149 @@
+import HighDimProb.RandomMatrix.Basic
+import HighDimProb.RandomMatrix.OperatorNorm
+import HighDimProb.RandomMatrix.TraceExp
+
+namespace HighDimProb
+
+open HighDimProb
+open MeasureTheory
+open scoped Matrix.Norms.L2Operator
+
+noncomputable section
+
+/-- Finite-measure trace-exponential integrability from uniform operator-norm bounds.
+
+The proof is a compactness argument: the sum `H + Z` is uniformly contained in
+a closed ball, `traceMatrixExp` is continuous on that ball, and a continuous
+function on a compact set is bounded. The final step is
+`MeasureTheory.Integrable.of_bound`.
+
+This is intentionally narrower than the exact HighDimProb Tropp statement,
+which does not assume finite measure or any domination on the trace-exponential
+integrand. -/
+theorem traceMatrixExp_add_integrable_of_operatorNormBounds_finiteMeasure
+    {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} [IsFiniteMeasure P]
+    {n : Nat} (H Z : RandomMatrix Omega n n) (RH RZ : Real)
+    (hH : IsRandomMatrix P H) (hZ : IsRandomMatrix P Z)
+    (hHbound : ∀ ω, operatorNorm H ω ≤ RH)
+    (hZbound : ∀ ω, operatorNorm Z ω ≤ RZ) :
+    IntegrableRealRandomVariable P (fun ω => traceMatrixExp (H ω + Z ω)) := by
+  have hSum : IsRandomMatrix P (fun ω => H ω + Z ω) := by
+    intro i j
+    simpa [HighDimProb.matrixEntry] using (hH i j).add (hZ i j)
+
+  have hSumMeas : Measurable (fun ω => H ω + Z ω) :=
+    measurable_randomMatrix_of_isRandomMatrix hSum
+
+  letI : NormedAlgebra Rat (Matrix (Fin n) (Fin n) Real) :=
+    NormedAlgebra.restrictScalars Rat Real (Matrix (Fin n) (Fin n) Real)
+
+  have hTrace : Continuous
+      (Matrix.traceLinearMap (n := Fin n) (α := Real) (R := Real) :
+        Matrix (Fin n) (Fin n) Real →ₗ[Real] Real) :=
+    LinearMap.continuous_of_finiteDimensional _
+
+  have hTraceExp : Continuous (fun A : Matrix (Fin n) (Fin n) Real => traceMatrixExp A) := by
+    simpa [HighDimProb.traceMatrixExp, HighDimProb.matrixTrace, HighDimProb.matrixExp] using
+      hTrace.comp NormedSpace.exp_continuous
+
+  have hcompact :
+      IsCompact (Metric.closedBall (0 : Matrix (Fin n) (Fin n) Real) (RH + RZ)) := by
+    simpa using
+      (isCompact_closedBall (0 : Matrix (Fin n) (Fin n) Real) (RH + RZ))
+
+  rcases hcompact.exists_bound_of_continuousOn hTraceExp.continuousOn with ⟨C, hC⟩
+  have hbound : ∀ ω, |traceMatrixExp (H ω + Z ω)| ≤ C := by
+    intro ω
+    have hdist : dist (H ω + Z ω) (0 : Matrix (Fin n) (Fin n) Real) ≤ RH + RZ := by
+      rw [dist_eq_norm, sub_zero]
+      calc
+        ‖H ω + Z ω‖ ≤ ‖H ω‖ + ‖Z ω‖ := norm_add_le _ _
+        _ ≤ RH + RZ := add_le_add (hHbound ω) (hZbound ω)
+    have hmem : H ω + Z ω ∈ Metric.closedBall (0 : Matrix (Fin n) (Fin n) Real) (RH + RZ) := by
+      simpa [Metric.mem_closedBall] using hdist
+    exact hC _ hmem
+
+  have hMeas : Measurable (fun ω => traceMatrixExp (H ω + Z ω)) :=
+    hTraceExp.measurable.comp hSumMeas
+
+  exact MeasureTheory.Integrable.of_bound hMeas.aestronglyMeasurable C (ae_of_all _ hbound)
+
+/-- Tropp-state-history add-step integrability under explicit operator-norm bounds.
+
+This is a thin wrapper around the generic finite-measure bound above. It keeps
+the Tropp naming available without claiming the exact HighDimProb theorem,
+which is missing finite-measure and domination hypotheses. -/
+theorem traceExpIntegrable_troppStateHistory_add_step_of_operatorNormBounds_finiteMeasure
+    {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} [IsFiniteMeasure P]
+    {m n : Nat} (theta : Real)
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (RH RZ : Real)
+    (hHist : ∀ i,
+      IsRandomMatrix P
+        (@troppStateHistory Omega _ m n theta X K i))
+    (hStep : ∀ i,
+      IsRandomMatrix P
+        (@troppCurrentRandomStep Omega _ m n theta X i))
+    (hHistBound : ∀ i ω,
+      operatorNorm (@troppStateHistory Omega _ m n theta X K i) ω ≤ RH)
+    (hStepBound : ∀ i ω,
+      operatorNorm (@troppCurrentRandomStep Omega _ m n theta X i) ω ≤ RZ) :
+    ∀ i,
+      IntegrableRealRandomVariable P
+        (fun ω =>
+          traceMatrixExp
+            (@troppStateHistory Omega _ m n theta X K i ω +
+              @troppCurrentRandomStep Omega _ m n theta X i ω)) := by
+  intro i
+  exact
+    traceMatrixExp_add_integrable_of_operatorNormBounds_finiteMeasure
+      (P := P)
+      (@troppStateHistory Omega _ m n theta X K i)
+      (@troppCurrentRandomStep Omega _ m n theta X i)
+      RH RZ (hHist i) (hStep i) (hHistBound i) (hStepBound i)
+
+end
+
+
+noncomputable section
+
+/-- Tropp-state-history add-K integrability under explicit operator-norm bounds.
+
+This is a thin wrapper around the generic finite-measure bound above. The
+deterministic comparison matrix `K i` is treated as a constant random matrix so
+the bridge stays reusable without claiming the exact HighDimProb statement.
+-/
+theorem traceExpIntegrable_troppStateHistory_add_K_of_operatorNormBounds_finiteMeasure
+    {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega} [IsFiniteMeasure P]
+    {m n : Nat} (theta : Real)
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (RH RK : Real)
+    (hHist : forall i,
+      IsRandomMatrix P
+        (@troppStateHistory Omega _ m n theta X K i))
+    (hHistBound : forall i omega,
+      operatorNorm (@troppStateHistory Omega _ m n theta X K i) omega <= RH)
+    (hKBound : forall i omega, operatorNorm (fun _ : Omega => K i) omega <= RK) :
+    forall i,
+      IntegrableRealRandomVariable P
+        (fun omega =>
+          traceMatrixExp
+            (@troppStateHistory Omega _ m n theta X K i omega + K i)) := by
+  intro i
+  have hKrand : IsRandomMatrix P (fun _ : Omega => K i) := by
+    intro a b
+    change Measurable (fun _ : Omega => K i a b)
+    exact measurable_const
+  exact
+    traceMatrixExp_add_integrable_of_operatorNormBounds_finiteMeasure
+      (P := P)
+      (@troppStateHistory Omega _ m n theta X K i)
+      (fun _ : Omega => K i)
+      RH RK
+      (hHist i) hKrand (hHistBound i) (hKBound i)
+
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/TraceExpJensenProvider.lean b/HighDimProb/RandomMatrix/TraceExpJensenProvider.lean
new file mode 100644
index 0000000..169c7a8
--- /dev/null
+++ b/HighDimProb/RandomMatrix/TraceExpJensenProvider.lean
@@ -0,0 +1,299 @@
+import HighDimProb.RandomMatrix.Expectation
+import HighDimProb.RandomMatrix.HardboneStatements
+import HighDimProb.RandomMatrix.TraceExp
+import HighDimProb.Analysis.SelfAdjointPositiveDomain
+import HighDimProb.Analysis.OpenJensen
+import Mathlib.Analysis.Convex.Integral
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
+import Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
+import Mathlib.Analysis.CStarAlgebra.Matrix
+import Mathlib.Topology.Instances.Matrix
+
+/-!
+# Trace-exp Jensen bridge
+
+This module proves a reusable Jensen bridge on an explicit closed convex
+domain contained in the positive self-adjoint cone, together with the exact
+open-domain wrapper that consumes the existing Lieb concavity statement.
+-/
+
+namespace HighDimProb
+
+open HighDimProb
+open MeasureTheory
+open scoped MatrixOrder Matrix.Norms.L2Operator
+
+noncomputable section
+
+private def matrixToPiContinuousLinearEquiv {m n : Nat} :
+    Matrix (Fin m) (Fin n) Real ≃L[Real] (Fin m -> Fin n -> Real) :=
+  let e : Matrix (Fin m) (Fin n) Real ≃ₗ[Real] (Fin m -> Fin n -> Real) :=
+    { toFun := fun A => fun i => fun j => A i j
+      invFun := fun f => fun i => fun j => f i j
+      left_inv := by intro A; rfl
+      right_inv := by intro f; rfl
+      map_add' := by intro A B; rfl
+      map_smul' := by intro c A; rfl }
+  e.toContinuousLinearEquiv
+
+private theorem integrable_matrix_of_integrableRandomMatrix {Omega : Type*}
+    [MeasurableSpace Omega] {P : Measure Omega} {m n : Nat}
+    {A : RandomMatrix Omega m n} (hA : IntegrableRandomMatrix P A) :
+    Integrable A P := by
+  let toPi := matrixToPiContinuousLinearEquiv (m := m) (n := n)
+  have hRows : forall i : Fin m, Integrable (fun omega => A omega i) P := by
+    intro i
+    apply Integrable.of_eval
+    intro j
+    exact hA i j
+  have hEntries :
+      Integrable (fun omega => fun i : Fin m => fun j : Fin n => A omega i j) P :=
+    Integrable.of_eval hRows
+  have hPi : Integrable (fun omega => toPi (A omega)) P := by
+    simpa [toPi, matrixToPiContinuousLinearEquiv] using hEntries
+  have hMatrix : Integrable (fun omega => toPi.symm (toPi (A omega))) P :=
+    (ContinuousLinearEquiv.integrable_comp_iff (L := toPi.symm)).2 hPi
+  simpa using hMatrix
+
+/-- Carrier-native Lieb concavity wrapper on the strictly positive self-adjoint
+domain. -/
+theorem liebTraceExpConcavity_selfAdjointCarrier
+    {n : Nat} (H : Matrix (Fin n) (Fin n) Real)
+    (hConcave : liebTraceExpConcavity_statement H)
+    (hH : IsSelfAdjointMatrix H) :
+    ConcaveOn Real (selfAdjointStrictlyPositiveSet n)
+      (fun M : selfAdjoint (Matrix (Fin n) (Fin n) Real) =>
+        traceMatrixExp (H + CFC.log (M : Matrix (Fin n) (Fin n) Real))) := by
+  refine ⟨convex_selfAdjointStrictlyPositiveSet n, ?_⟩
+  intro x hx y hy a b ha hb hab
+  have hxAmbient :
+      (x : Matrix (Fin n) (Fin n) Real) ∈
+        {M : Matrix (Fin n) (Fin n) Real |
+          IsSelfAdjointMatrix M ∧ IsStrictlyPositive M} :=
+    And.intro x.2 hx
+  have hyAmbient :
+      (y : Matrix (Fin n) (Fin n) Real) ∈
+        {M : Matrix (Fin n) (Fin n) Real |
+          IsSelfAdjointMatrix M ∧ IsStrictlyPositive M} :=
+    And.intro y.2 hy
+  simpa using (hConcave hH).2 hxAmbient hyAmbient ha hb hab
+
+/-- Recover the exact HighDimProb Lieb concavity statement from a carrier-native
+concavity theorem on `selfAdjoint` matrices.
+
+This is the reverse transport needed if a future Mathlib theorem is most
+naturally stated on the `selfAdjoint` carrier. -/
+theorem liebTraceExpConcavity_of_selfAdjointCarrier
+    {n : Nat} (H : Matrix (Fin n) (Fin n) Real)
+    (hCarrier :
+      IsSelfAdjointMatrix H ->
+        ConcaveOn Real (selfAdjointStrictlyPositiveSet n)
+          (fun M : selfAdjoint (Matrix (Fin n) (Fin n) Real) =>
+            traceMatrixExp (H + CFC.log (M : Matrix (Fin n) (Fin n) Real)))) :
+    liebTraceExpConcavity_statement H := by
+  intro hH
+  let s : Set (Matrix (Fin n) (Fin n) Real) :=
+    {M : Matrix (Fin n) (Fin n) Real |
+      IsSelfAdjointMatrix M ∧ IsStrictlyPositive M}
+  let g : Matrix (Fin n) (Fin n) Real -> Real :=
+    fun M => traceMatrixExp (H + CFC.log M)
+  let gSA : selfAdjoint (Matrix (Fin n) (Fin n) Real) -> Real :=
+    fun M => traceMatrixExp (H + CFC.log (M : Matrix (Fin n) (Fin n) Real))
+  have hCarrierConcave := hCarrier hH
+  refine ⟨?_, ?_⟩
+  · intro x hx y hy a b ha hb hab
+    let xSA : selfAdjoint (Matrix (Fin n) (Fin n) Real) := ⟨x, hx.1⟩
+    let ySA : selfAdjoint (Matrix (Fin n) (Fin n) Real) := ⟨y, hy.1⟩
+    have hxSA : xSA ∈ selfAdjointStrictlyPositiveSet n := hx.2
+    have hySA : ySA ∈ selfAdjointStrictlyPositiveSet n := hy.2
+    have hxySA :
+        a • xSA + b • ySA ∈ selfAdjointStrictlyPositiveSet n :=
+      hCarrierConcave.1 hxSA hySA ha hb hab
+    refine And.intro ?_ ?_
+    · simpa [xSA, ySA] using (a • xSA + b • ySA).2
+    · simpa [xSA, ySA] using hxySA
+  · intro x hx y hy a b ha hb hab
+    let xSA : selfAdjoint (Matrix (Fin n) (Fin n) Real) := ⟨x, hx.1⟩
+    let ySA : selfAdjoint (Matrix (Fin n) (Fin n) Real) := ⟨y, hy.1⟩
+    have hxSA : xSA ∈ selfAdjointStrictlyPositiveSet n := hx.2
+    have hySA : ySA ∈ selfAdjointStrictlyPositiveSet n := hy.2
+    simpa [s, g, gSA, xSA, ySA] using
+      (hCarrierConcave.2 hxSA hySA ha hb hab)
+
+/-- Exact equivalence between the ambient HighDimProb Lieb concavity contract
+and its carrier-native `selfAdjoint` form. -/
+theorem liebTraceExpConcavity_statement_iff_selfAdjointCarrier
+    {n : Nat} (H : Matrix (Fin n) (Fin n) Real) :
+    liebTraceExpConcavity_statement H ↔
+      IsSelfAdjointMatrix H ->
+        ConcaveOn Real (selfAdjointStrictlyPositiveSet n)
+          (fun M : selfAdjoint (Matrix (Fin n) (Fin n) Real) =>
+            traceMatrixExp (H + CFC.log (M : Matrix (Fin n) (Fin n) Real))) := by
+  constructor
+  · intro hConcave hH
+    exact liebTraceExpConcavity_selfAdjointCarrier H hConcave hH
+  · intro hCarrier
+    exact liebTraceExpConcavity_of_selfAdjointCarrier H hCarrier
+
+/-- Jensen bridge for a closed convex subset of the positive self-adjoint cone.
+
+The theorem consumes the existing Lieb concavity statement and the repository's
+entrywise matrix expectation / integrability API. The extra hypothesis is the
+continuity of the trace-log-exponential integrand on the chosen closed convex
+set. -/
+theorem liebJensenTraceExp_of_closedConvexSubset
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P]
+    {n : Nat}
+    (H : Matrix (Fin n) (Fin n) Real)
+    (Y : RandomMatrix Omega n n)
+    (s : Set (Matrix (Fin n) (Fin n) Real))
+    (hsClosed : IsClosed s)
+    (hsConvex : Convex Real s)
+    (hsSubset : Set.Subset s (fun M : Matrix (Fin n) (Fin n) Real =>
+      And (IsSelfAdjointMatrix M) (IsStrictlyPositive M)))
+    (hConcave : liebTraceExpConcavity_statement H)
+    (hH : IsSelfAdjointMatrix H)
+    (hYmem : forall omega, Y omega ∈ s)
+    (hInt : IntegrableRandomMatrix P Y)
+    (hTraceInt : IntegrableRealRandomVariable P
+      (fun omega => traceMatrixExp (H + CFC.log (Y omega))))
+    (hGCont : ContinuousOn (fun M : Matrix (Fin n) (Fin n) Real =>
+      traceMatrixExp (H + CFC.log M)) s) :
+    expect P (fun omega => traceMatrixExp (H + CFC.log (Y omega))) <=
+      traceMatrixExp (H + CFC.log (matrixExpect P Y)) := by
+  let g : Matrix (Fin n) (Fin n) Real -> Real :=
+    fun M => traceMatrixExp (H + CFC.log M)
+
+  have hConcaveS : ConcaveOn Real s g := (hConcave hH).subset hsSubset hsConvex
+
+  have hIntY : Integrable (fun omega => Y omega) P :=
+    integrable_matrix_of_integrableRandomMatrix (P := P) (A := Y) hInt
+
+  have hIntG : Integrable (fun omega => g (Y omega)) P := by
+    change Integrable (fun omega => traceMatrixExp (H + CFC.log (Y omega))) P
+    exact hTraceInt
+
+  have hJensen :=
+    hConcaveS.le_map_integral hGCont hsClosed (ae_of_all _ hYmem) hIntY hIntG
+
+  have hExpectEq : matrixExpect P Y = ∫ omega, Y omega ∂P :=
+    matrixExpect_eq_integral (P := P) (A := Y) hInt
+
+  have hJensen' :
+      expect P (fun omega => traceMatrixExp (H + CFC.log (Y omega))) <=
+        traceMatrixExp (H + CFC.log (∫ omega, Y omega ∂P)) := by
+    change ∫ omega, traceMatrixExp (H + CFC.log (Y omega)) ∂P <=
+      traceMatrixExp (H + CFC.log (∫ omega, Y omega ∂P))
+    exact hJensen
+
+  rw [hExpectEq]
+  exact hJensen'
+
+/-- Exact Jensen wrapper consuming the existing Lieb concavity statement and
+the provider's self-adjoint strictly positive carrier infrastructure. -/
+theorem liebJensenTraceExp_statement_of_liebConcavity
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P]
+    {n : Nat}
+    (H : Matrix (Fin n) (Fin n) Real)
+    (Y : RandomMatrix Omega n n) :
+    liebJensenTraceExp_statement (P := P) H Y := by
+  intro hConcave hH hYsa hYpos hInt _hMeanSA hMeanPos hTraceInt
+  let F : Omega -> selfAdjoint (Matrix (Fin n) (Fin n) Real) :=
+    fun omega =>
+      (Subtype.mk (Y omega) (hYsa omega) : selfAdjoint (Matrix (Fin n) (Fin n) Real))
+  let g : selfAdjoint (Matrix (Fin n) (Fin n) Real) -> Real := fun M =>
+    traceMatrixExp (H + CFC.log (M : Matrix (Fin n) (Fin n) Real))
+
+  have hIntY : Integrable (fun omega => Y omega) P :=
+    integrable_matrix_of_integrableRandomMatrix (P := P) (A := Y) hInt
+  have hFint : Integrable F P := by
+    exact
+      selfAdjoint.integrable_mk_of_integrable_coe
+        (A := Matrix (Fin n) (Fin n) Real)
+        (F := fun omega => Y omega) hIntY fun omega => hYsa omega
+  have hFmem :
+      Filter.Eventually
+        (fun omega => Set.Mem (selfAdjointStrictlyPositiveSet n) (F omega))
+        (MeasureTheory.ae P) :=
+    Filter.Eventually.of_forall fun omega => hYpos omega
+  have hgInt : Integrable (fun omega => g (F omega)) P := by
+    change Integrable (fun omega => traceMatrixExp (H + CFC.log (Y omega))) P
+    exact hTraceInt
+  have hMeanEq :
+      ((MeasureTheory.integral P F : selfAdjoint (Matrix (Fin n) (Fin n) Real)) :
+          Matrix (Fin n) (Fin n) Real) = matrixExpect P Y := by
+    calc
+      ((MeasureTheory.integral P F : selfAdjoint (Matrix (Fin n) (Fin n) Real)) :
+          Matrix (Fin n) (Fin n) Real)
+          = MeasureTheory.integral P
+              (fun omega =>
+                ((F omega : selfAdjoint (Matrix (Fin n) (Fin n) Real)) :
+                  Matrix (Fin n) (Fin n) Real)) :=
+            selfAdjoint.coe_integral hFint
+      _ = MeasureTheory.integral P (fun omega => Y omega) := by
+        rfl
+      _ = matrixExpect P Y := by
+        symm
+        exact matrixExpect_eq_integral (P := P) (A := Y) hInt
+  have hMeanMem :
+      Set.Mem (selfAdjointStrictlyPositiveSet n)
+        (MeasureTheory.integral P F : selfAdjoint (Matrix (Fin n) (Fin n) Real)) := by
+    change IsStrictlyPositive
+      (((MeasureTheory.integral P F : selfAdjoint (Matrix (Fin n) (Fin n) Real)) :
+        Matrix (Fin n) (Fin n) Real))
+    rw [hMeanEq]
+    exact hMeanPos
+
+  have hJensen :
+      MeasureTheory.integral P (fun omega => g (F omega)) <=
+        g (MeasureTheory.integral P F) := by
+    exact
+      @ConcaveOn.le_map_integral_of_mem_open
+        Omega
+        (selfAdjoint (Matrix (Fin n) (Fin n) Real))
+        inferInstance
+        inferInstance
+        inferInstance
+        (selfAdjoint.instCompleteSpaceSelfAdjoint (A := Matrix (Fin n) (Fin n) Real))
+        (selfAdjoint.instFiniteDimensionalSelfAdjoint (A := Matrix (Fin n) (Fin n) Real))
+        P
+        inferInstance
+        (selfAdjointStrictlyPositiveSet n)
+        F
+        g
+        (liebTraceExpConcavity_selfAdjointCarrier H hConcave hH)
+        (isOpen_selfAdjointStrictlyPositiveSet n)
+        hFmem
+        hFint
+        (by
+          change Integrable (fun omega => g (F omega)) P
+          exact hgInt)
+        hMeanMem
+
+  have leftEq :
+      MeasureTheory.integral P (fun omega => g (F omega)) =
+        expect P (fun omega => traceMatrixExp (H + CFC.log (Y omega))) := by
+    rfl
+  have rightEq :
+      g (MeasureTheory.integral P F) =
+        traceMatrixExp (H + CFC.log (matrixExpect P Y)) := by
+    change traceMatrixExp
+        (H +
+          CFC.log
+            (((MeasureTheory.integral P F : selfAdjoint (Matrix (Fin n) (Fin n) Real)) :
+              Matrix (Fin n) (Fin n) Real))) =
+      traceMatrixExp (H + CFC.log (matrixExpect P Y))
+    rw [hMeanEq]
+
+  calc
+    expect P (fun omega => traceMatrixExp (H + CFC.log (Y omega)))
+        = MeasureTheory.integral P (fun omega => g (F omega)) := leftEq.symm
+    _ <= g (MeasureTheory.integral P F) := hJensen
+    _ = traceMatrixExp (H + CFC.log (matrixExpect P Y)) := rightEq
+
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/TraceExpLogContinuityProvider.lean b/HighDimProb/RandomMatrix/TraceExpLogContinuityProvider.lean
new file mode 100644
index 0000000..9cd3144
--- /dev/null
+++ b/HighDimProb/RandomMatrix/TraceExpLogContinuityProvider.lean
@@ -0,0 +1,186 @@
+import HighDimProb.RandomMatrix.MatrixLogProvider
+import HighDimProb.Analysis.SelfAdjointCarrier
+import HighDimProb.Analysis.SelfAdjointPositiveDomain
+import HighDimProb.RandomMatrix.TraceExpJensenProvider
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
+import Mathlib.Topology.Algebra.Module.FiniteDimension
+
+/-!
+# Log continuity for the trace-exp Jensen bridge
+
+This module packages the raw continuity facts needed to remove the explicit
+continuity hypothesis from the provider's closed-convex Jensen bridge. The
+exact open-domain Jensen statement is proved in `TraceExp.Jensen`; this module
+keeps the continuity facts reusable for smaller closed-domain variants.
+-/
+
+namespace HighDimProb
+
+open HighDimProb
+open MeasureTheory
+open scoped ComplexOrder MatrixOrder Matrix.Norms.L2Operator Matrix.Norms.Operator
+
+noncomputable section
+
+private theorem continuous_realMatrixToCStarMatrix {n : Nat} :
+    Continuous (fun M : Matrix (Fin n) (Fin n) Real =>
+      HighDimProb.realMatrixToCStarMatrix M) := by
+  have hMapEntries : Continuous (fun A : Matrix (Fin n) (Fin n) Real =>
+      A.map (algebraMap Real Complex)) := by
+    fun_prop
+  change Continuous (fun A : Matrix (Fin n) (Fin n) Real =>
+    CStarMatrix.ofMatrix (A.map (algebraMap Real Complex)))
+  simpa [CStarMatrix.ofMatrix_eq_ofMatrixL] using
+    (CStarMatrix.ofMatrixL.continuous.comp hMapEntries)
+
+private def cstarMatrixToRealMatrix {n : Nat}
+    (A : CStarMatrix (Fin n) (Fin n) Complex) :
+    Matrix (Fin n) (Fin n) Real :=
+  fun i j => Complex.re (A i j)
+
+@[simp] private theorem cstarMatrixToRealMatrix_realMatrixToCStarMatrix {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Real) :
+    cstarMatrixToRealMatrix (HighDimProb.realMatrixToCStarMatrix A) = A := by
+  ext i j
+  simp [cstarMatrixToRealMatrix, HighDimProb.realMatrixToCStarMatrix]
+
+private theorem continuous_cstarMatrixToRealMatrix {n : Nat} :
+    Continuous (fun A : CStarMatrix (Fin n) (Fin n) Complex =>
+      cstarMatrixToRealMatrix A) := by
+  change Continuous (fun A : CStarMatrix (Fin n) (Fin n) Complex =>
+    fun i => fun j => Complex.re (A i j))
+  fun_prop
+
+/-- The real-matrix CFC logarithm is continuous on the self-adjoint strictly
+positive domain, proved by transporting to `CStarMatrix`, using Mathlib's
+CStar-side continuity theorem there, and pulling back through the existing
+provider log bridge. -/
+theorem continuousOn_cfcLog_selfAdjoint_strictlyPositive {n : Nat} :
+    ContinuousOn (fun M : Matrix (Fin n) (Fin n) Real => CFC.log M)
+      {M : Matrix (Fin n) (Fin n) Real |
+        And (IsSelfAdjointMatrix M) (IsStrictlyPositive M)} := by
+  let s : Set (Matrix (Fin n) (Fin n) Real) :=
+    {M | And (IsSelfAdjointMatrix M) (IsStrictlyPositive M)}
+  have hLift : ContinuousOn (fun M : Matrix (Fin n) (Fin n) Real =>
+      HighDimProb.realMatrixToCStarMatrix M) s :=
+    continuous_realMatrixToCStarMatrix.continuousOn
+  have hCStarLog : ContinuousOn (fun A : CStarMatrix (Fin n) (Fin n) Complex =>
+      CFC.log A)
+      {A : CStarMatrix (Fin n) (Fin n) Complex |
+        And (IsSelfAdjoint A) (IsUnit A)} :=
+    CFC.continuousOn_log
+  have hLogLift : ContinuousOn (fun M : Matrix (Fin n) (Fin n) Real =>
+      CFC.log (HighDimProb.realMatrixToCStarMatrix M)) s :=
+    hCStarLog.comp hLift (by
+      intro M hM
+      exact And.intro
+        (HighDimProb.isSelfAdjoint_realMatrixToCStarMatrix hM.1)
+        ((realMatrixToCStar_strictlyPositive hM.2).isUnit))
+  have hRecoverLog : ContinuousOn (fun M : Matrix (Fin n) (Fin n) Real =>
+      cstarMatrixToRealMatrix
+        (CFC.log (HighDimProb.realMatrixToCStarMatrix M))) s :=
+    continuous_cstarMatrixToRealMatrix.continuousOn.comp hLogLift
+      (by
+        intro M hM
+        exact Set.mem_univ _)
+  refine hRecoverLog.congr ?_
+  intro M hM
+  ext i j
+  have hBack := realMatrixToCStar_log hM.1.isSelfAdjoint hM.2
+  have hEntry := congrFun (congrFun hBack i) j
+  simpa [cstarMatrixToRealMatrix] using congrArg Complex.re hEntry
+
+/-- The trace-exponential Jensen integrand is continuous on the self-adjoint
+strictly positive domain. -/
+theorem continuousOn_traceMatrixExp_add_cfcLog_selfAdjoint_strictlyPositive
+    {n : Nat} (H : Matrix (Fin n) (Fin n) Real) :
+    ContinuousOn (fun M : Matrix (Fin n) (Fin n) Real =>
+      traceMatrixExp (H + CFC.log M))
+      {M : Matrix (Fin n) (Fin n) Real |
+        And (IsSelfAdjointMatrix M) (IsStrictlyPositive M)} := by
+  let s : Set (Matrix (Fin n) (Fin n) Real) :=
+    {M | And (IsSelfAdjointMatrix M) (IsStrictlyPositive M)}
+  have hLog : ContinuousOn (fun M : Matrix (Fin n) (Fin n) Real => CFC.log M) s :=
+    continuousOn_cfcLog_selfAdjoint_strictlyPositive
+  have hAddH : Continuous (fun A : Matrix (Fin n) (Fin n) Real => H + A) :=
+    continuous_const.add continuous_id
+  have hAddLog : ContinuousOn (fun M : Matrix (Fin n) (Fin n) Real => H + CFC.log M) s :=
+    hAddH.continuousOn.comp hLog (by
+      intro M hM
+      exact Set.mem_univ _)
+  have hTraceExp : Continuous (fun A : Matrix (Fin n) (Fin n) Real => traceMatrixExp A) := by
+    change Continuous (fun A : Matrix (Fin n) (Fin n) Real =>
+      Matrix.trace (NormedSpace.exp A))
+    fun_prop
+  simpa [s] using
+    (hTraceExp.continuousOn.comp hAddLog (by
+      intro M hM
+      exact Set.mem_univ _))
+
+/-- Carrier-native continuity wrapper for the trace-exp/log Jensen integrand on
+the strictly positive self-adjoint domain. -/
+theorem continuousOn_traceMatrixExp_add_cfcLog_selfAdjointCarrier_strictlyPositive
+    {n : Nat} (H : Matrix (Fin n) (Fin n) Real) :
+    ContinuousOn
+      (fun M : selfAdjoint (Matrix (Fin n) (Fin n) Real) =>
+        traceMatrixExp (H + CFC.log (M : Matrix (Fin n) (Fin n) Real)))
+      (selfAdjointStrictlyPositiveSet n) := by
+  let s : Set (Matrix (Fin n) (Fin n) Real) :=
+    {M | And (IsSelfAdjointMatrix M) (IsStrictlyPositive M)}
+  have hAmbient :
+      ContinuousOn
+        (fun M : Matrix (Fin n) (Fin n) Real =>
+          traceMatrixExp (H + CFC.log M))
+        s :=
+    continuousOn_traceMatrixExp_add_cfcLog_selfAdjoint_strictlyPositive (H := H)
+  have hSubtype :
+      ContinuousOn
+        (fun M : selfAdjoint (Matrix (Fin n) (Fin n) Real) =>
+          (M : Matrix (Fin n) (Fin n) Real))
+        (selfAdjointStrictlyPositiveSet n) :=
+    continuous_subtype_val.continuousOn
+  have hMapsTo :
+      Set.MapsTo
+        (fun M : selfAdjoint (Matrix (Fin n) (Fin n) Real) =>
+          (M : Matrix (Fin n) (Fin n) Real))
+        (selfAdjointStrictlyPositiveSet n) s := by
+    intro M hM
+    exact And.intro
+      (show IsSelfAdjointMatrix (M : Matrix (Fin n) (Fin n) Real) from M.2)
+      hM
+  simpa [s] using hAmbient.comp hSubtype hMapsTo
+
+/-- Closed-convex Jensen bridge without an explicit continuity hypothesis.
+
+The continuity side condition is discharged by
+`continuousOn_traceMatrixExp_add_cfcLog_selfAdjoint_strictlyPositive` together
+with the existing subset hypothesis into the positive self-adjoint domain.
+-/
+theorem liebJensenTraceExp_of_closedConvexSubset_autoContinuous
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P]
+    {n : Nat}
+    (H : Matrix (Fin n) (Fin n) Real)
+    (Y : RandomMatrix Omega n n)
+    (s : Set (Matrix (Fin n) (Fin n) Real))
+    (hsClosed : IsClosed s)
+    (hsConvex : Convex Real s)
+    (hsSubset : Set.Subset s (fun M : Matrix (Fin n) (Fin n) Real =>
+      And (IsSelfAdjointMatrix M) (IsStrictlyPositive M)))
+    (hConcave : liebTraceExpConcavity_statement H)
+    (hH : IsSelfAdjointMatrix H)
+    (hYmem : forall omega, Set.Mem s (Y omega))
+    (hInt : IntegrableRandomMatrix P Y)
+    (hTraceInt : IntegrableRealRandomVariable P
+      (fun omega => traceMatrixExp (H + CFC.log (Y omega)))) :
+    expect P (fun omega => traceMatrixExp (H + CFC.log (Y omega))) <=
+      traceMatrixExp (H + CFC.log (matrixExpect P Y)) := by
+  exact liebJensenTraceExp_of_closedConvexSubset
+    (H := H) (Y := Y) (s := s) hsClosed hsConvex hsSubset hConcave hH hYmem
+    hInt hTraceInt
+    ((continuousOn_traceMatrixExp_add_cfcLog_selfAdjoint_strictlyPositive
+      (H := H)).mono hsSubset)
+
+end
+
+end HighDimProb
diff --git a/HighDimProb/RandomMatrix/TraceExpLogOrderProvider.lean b/HighDimProb/RandomMatrix/TraceExpLogOrderProvider.lean
new file mode 100644
index 0000000..4554dfd
--- /dev/null
+++ b/HighDimProb/RandomMatrix/TraceExpLogOrderProvider.lean
@@ -0,0 +1,40 @@
+import HighDimProb.RandomMatrix.MatrixLogProvider
+import HighDimProb.RandomMatrix.HardboneStatements
+
+/-!
+# Log-order bridge for the Tropp trace-exp step
+
+This module keeps the explicit provider-side log-order bridge used to decompose
+the Tropp trace-exp step. The exact statement
+`HighDimProb.matrixLog_le_of_le_matrixExp_statement` is already proved in the
+main repository; the provider only keeps the hypothesis-level helper that
+packages its operator-log contribution for downstream decomposition theorems.
+-/
+
+namespace HighDimProb
+
+open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator
+
+noncomputable section
+
+/-- Provider-side log-order bridge from `M <= exp K` to `log M <= K`.
+
+This supplies HighDimProb's operator-log monotonicity premise from
+`operatorLogMonotoneOnPositiveMatrices` and its log-domain premise from the main
+`matrixExpLogDomainForSelfAdjoint`. It does not prove trace-exp monotonicity,
+Lieb concavity, Golden-Thompson, or any Bernstein CFC fact. -/
+theorem matrixLog_le_of_le_matrixExp_of_providerLogMonotone {n : Nat}
+    (M K : Matrix (Fin n) (Fin n) Real)
+    (hM : HighDimProb.IsSelfAdjointMatrix M)
+    (hMpos : IsStrictlyPositive M)
+    (hK : HighDimProb.IsSelfAdjointMatrix K)
+    (hMK : HighDimProb.MatrixLE M (HighDimProb.matrixExp K)) :
+    HighDimProb.MatrixLE (CFC.log M) K :=
+  HighDimProb.matrixLog_le_of_le_matrixExp M K
+    (operatorLogMonotoneOnPositiveMatrices M (HighDimProb.matrixExp K))
+    (HighDimProb.matrixExpLogDomainForSelfAdjoint K)
+    hM hMpos hK hMK
+
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/TraceExpMonotonicityProvider.lean b/HighDimProb/RandomMatrix/TraceExpMonotonicityProvider.lean
new file mode 100644
index 0000000..ccb98e9
--- /dev/null
+++ b/HighDimProb/RandomMatrix/TraceExpMonotonicityProvider.lean
@@ -0,0 +1,131 @@
+import Mathlib.Analysis.Calculus.Deriv.MeanValue
+import HighDimProb.RandomMatrix.HardboneStatements
+import HighDimProb.RandomMatrix.TraceExp
+import HighDimProb.RandomMatrix.TraceExpDerivative
+
+/-!
+# Trace-exponential monotonicity bridge
+
+This module proves the exact HighDimProb trace-exponential monotonicity witness.
+The key ingredients are: if `C` is PSD in HighDimProb's explicit matrix order
+and `X` is self-adjoint, then `trace (C * exp X)` is nonnegative; from the
+affine derivative formula, this yields monotonicity of `t => tr exp (X + t C)`
+and then the endpoint theorem `traceMatrixExp_mono_add_selfAdjoint`.
+
+It does not prove Lieb concavity, Golden-Thompson, Tropp trace-MGF, or Matrix
+Bernstein.
+-/
+
+namespace HighDimProb
+
+noncomputable section
+
+open scoped MatrixOrder
+
+private theorem isSelfAdjointMatrix_add_smul
+    {n : Nat} (X C : Matrix (Fin n) (Fin n) Real) (t : Real)
+    (hX : HighDimProb.IsSelfAdjointMatrix X)
+    (hC : HighDimProb.IsSelfAdjointMatrix C) :
+    HighDimProb.IsSelfAdjointMatrix (X + SMul.smul t C) := by
+  have ht : IsSelfAdjoint t := by
+    simp [IsSelfAdjoint]
+  change (X + SMul.smul t C).IsHermitian
+  exact hX.add (hC.smul ht)
+
+/-- Minimal PSD/self-adjoint trace-exponential product bridge.
+
+If C is nonnegative in HighDimProb's explicit matrix order and X is
+self-adjoint, then the trace of C * exp X is nonnegative. -/
+theorem matrixTrace_mul_matrixExp_nonneg_of_selfAdjoint_of_matrixLE_zero
+    {n : Nat} (X C : Matrix (Fin n) (Fin n) Real)
+    (hX : HighDimProb.IsSelfAdjointMatrix X)
+    (hC0 : HighDimProb.MatrixLE 0 C) :
+    0 <= Matrix.trace (C * HighDimProb.matrixExp X) := by
+  have hCmath : (0 : Matrix (Fin n) (Fin n) Real) <= C :=
+    HighDimProb.mathlib_le_of_matrixLE hC0
+  have hCPSD : Matrix.PosSemidef C := by
+    simpa [Matrix.le_iff] using hCmath
+  have hExpPSD : Matrix.PosSemidef (HighDimProb.matrixExp X) :=
+    HighDimProb.matrixExp_posSemidef_of_selfAdjoint hX
+  obtain ⟨B, rfl⟩ :=
+    CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hCPSD.nonneg
+  have hProdPSD := hExpPSD.mul_mul_conjTranspose_same B
+  calc
+    0 <= Matrix.trace (B * HighDimProb.matrixExp X * star B) := by
+      simpa using hProdPSD.trace_nonneg
+    _ = Matrix.trace (star B * B * HighDimProb.matrixExp X) := by
+      simpa using Matrix.trace_mul_cycle B (HighDimProb.matrixExp X) (star B)
+    _ = Matrix.trace ((star B * B) * HighDimProb.matrixExp X) := by
+      rfl
+
+/-- Affine-line monotonicity for the trace exponential along a PSD direction.
+
+This is the minimal wrapper that combines the existing derivative formula with
+the nonnegative trace-product bridge. It does not prove the full
+`A ≤ B ↦ tr exp (H + A) ≤ tr exp (H + B)` witness. -/
+theorem monotone_traceMatrixExp_add_smul_of_selfAdjoint_of_matrixLE_zero
+    {n : Nat} (X C : Matrix (Fin n) (Fin n) Real)
+    (hX : HighDimProb.IsSelfAdjointMatrix X)
+    (hC : HighDimProb.IsSelfAdjointMatrix C)
+    (hC0 : HighDimProb.MatrixLE 0 C) :
+    Monotone (fun t : Real => HighDimProb.traceMatrixExp (X + SMul.smul t C)) := by
+  refine monotone_of_hasDerivAt_nonneg
+      (f' := fun t : Real =>
+        Matrix.trace (C * HighDimProb.matrixExp (X + SMul.smul t C))) ?_ ?_
+  · intro t
+    simpa [HighDimProb.traceMatrixExp, HighDimProb.matrixTrace, HighDimProb.matrixExp] using
+      hasDerivAt_trace_exp_add_smul_const X C t
+  · change ∀ t : Real, 0 <= Matrix.trace (C * HighDimProb.matrixExp (X + SMul.smul t C))
+    intro t
+    exact matrixTrace_mul_matrixExp_nonneg_of_selfAdjoint_of_matrixLE_zero
+      (X + SMul.smul t C) C
+      (isSelfAdjointMatrix_add_smul X C t hX hC) hC0
+
+private theorem isSelfAdjointMatrix_sub
+    {n : Nat} {A B : Matrix (Fin n) (Fin n) Real}
+    (hA : HighDimProb.IsSelfAdjointMatrix A)
+    (hB : HighDimProb.IsSelfAdjointMatrix B) :
+    HighDimProb.IsSelfAdjointMatrix (B - A) := by
+  change (B - A).IsHermitian
+  exact hB.sub hA
+
+private theorem matrixLE_zero_sub_of_matrixLE
+    {n : Nat} {A B : Matrix (Fin n) (Fin n) Real}
+    (hAB : HighDimProb.MatrixLE A B) :
+    HighDimProb.MatrixLE 0 (B - A) := by
+  unfold HighDimProb.MatrixLE at *
+  simpa using hAB
+
+private theorem traceMatrixExp_endpoint_zero
+    {n : Nat} (H A B : Matrix (Fin n) (Fin n) Real) :
+    (H + A) + SMul.smul (0 : Real) (B - A) = H + A := by
+  change (H + A) + (0 : Real) • (B - A) = H + A
+  simp
+
+private theorem traceMatrixExp_endpoint_one
+    {n : Nat} (H A B : Matrix (Fin n) (Fin n) Real) :
+    (H + A) + SMul.smul (1 : Real) (B - A) = H + B := by
+  change (H + A) + (1 : Real) • (B - A) = H + B
+  rw [one_smul]
+  abel
+
+/-- Exact provider witness for HighDimProb's trace-exponential monotonicity statement. -/
+theorem traceMatrixExp_mono_add_selfAdjoint {n : Nat}
+    (H A B : Matrix (Fin n) (Fin n) Real) :
+    HighDimProb.traceMatrixExp_mono_add_selfAdjoint_statement H A B := by
+  intro hH hA hB hAB
+  have hX : HighDimProb.IsSelfAdjointMatrix (H + A) := by
+    change (H + A).IsHermitian
+    exact hH.add hA
+  have hC : HighDimProb.IsSelfAdjointMatrix (B - A) :=
+    isSelfAdjointMatrix_sub hA hB
+  have hC0 : HighDimProb.MatrixLE 0 (B - A) :=
+    matrixLE_zero_sub_of_matrixLE hAB
+  have hmono := monotone_traceMatrixExp_add_smul_of_selfAdjoint_of_matrixLE_zero
+    (X := H + A) (C := B - A) hX hC hC0
+  have hle := hmono (show (0 : Real) <= 1 by norm_num)
+  simpa [HighDimProb.traceMatrixExp, HighDimProb.matrixTrace,
+    traceMatrixExp_endpoint_zero H A B, traceMatrixExp_endpoint_one H A B] using hle
+end
+
+end HighDimProb
\ No newline at end of file
diff --git a/HighDimProb/RandomMatrix/TraceExpTroppStepProvider.lean b/HighDimProb/RandomMatrix/TraceExpTroppStepProvider.lean
new file mode 100644
index 0000000..bb15588
--- /dev/null
+++ b/HighDimProb/RandomMatrix/TraceExpTroppStepProvider.lean
@@ -0,0 +1,239 @@
+import HighDimProb.RandomMatrix.EpsteinProvider
+import HighDimProb.RandomMatrix.TraceExpLogOrderProvider
+import HighDimProb.RandomMatrix.TraceExpJensenProvider
+import HighDimProb.RandomMatrix.TraceExpMonotonicityProvider
+
+/-!
+# Tropp step composition wrappers
+
+This module packages thin provider-side Tropp wrappers.
+
+- `troppLogExpComparisonToK_of_traceMatrixExp_mono_add_selfAdjoint` reuses the
+  provider log-order bridge plus the provider trace-exp monotonicity theorem.
+- `troppMasterTraceMGFStep_of_providerJensen` reuses the provider Jensen bridge
+  and main-library matrix-log normalization while keeping the one-step chain
+  premise explicit.
+
+It does not prove Lieb concavity, the one-step Tropp chain, Golden-Thompson, or
+Matrix Bernstein.
+-/
+
+namespace HighDimProb
+
+open HighDimProb
+open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator
+
+noncomputable section
+
+/-- Tropp log/`K` comparison from provider log-order plus trace-exp monotonicity.
+
+The only analytic input left explicit is
+`HighDimProb.traceMatrixExp_mono_add_selfAdjoint_statement`. This theorem does
+not prove that monotonicity statement, Lieb concavity, Golden-Thompson, or any
+Bernstein CFC fact. -/
+theorem troppLogExpComparisonToK_of_traceMatrixExp_mono_add_selfAdjoint {n : Nat}
+    (H M K : Matrix (Fin n) (Fin n) Real)
+    (hTrace :
+      HighDimProb.traceMatrixExp_mono_add_selfAdjoint_statement H (CFC.log M) K) :
+    HighDimProb.troppLogExpComparisonToK_statement H M K := by
+  intro hH hM hMpos hK hMK
+  have hLogLE : HighDimProb.MatrixLE (CFC.log M) K :=
+    matrixLog_le_of_le_matrixExp_of_providerLogMonotone M K hM hMpos hK hMK
+  have hLogSelfAdjoint : HighDimProb.IsSelfAdjointMatrix (CFC.log M) :=
+    isSelfAdjointMatrix_cfc_log hM
+  exact hTrace hH hLogSelfAdjoint hK hLogLE
+
+/-- Tropp log/`K` comparison using only provider log-order and provider trace-exp monotonicity. -/
+theorem troppLogExpComparisonToK_of_providerLogOrder {n : Nat}
+    (H M K : Matrix (Fin n) (Fin n) Real) :
+    HighDimProb.troppLogExpComparisonToK_statement H M K := by
+  intro hH hM hMpos hK hMK
+  exact
+    troppLogExpComparisonToK_of_traceMatrixExp_mono_add_selfAdjoint
+      H M K (traceMatrixExp_mono_add_selfAdjoint H (CFC.log M) K)
+      hH hM hMpos hK hMK
+/-- Thin Tropp one-step composition from the provider's exact Jensen theorem.
+
+This theorem keeps the hard one-step chain hypothesis explicit. The provider
+only discharges the Jensen input using the exact Lieb-concavity-to-Jensen
+wrapper, while HighDimProb supplies the pointwise `log (exp Z) = Z`
+normalization for self-adjoint `Z`. It does not prove Lieb concavity,
+Golden-Thompson, trace-exp monotonicity, or Matrix Bernstein. -/
+theorem troppMasterTraceMGFStep_of_providerJensen
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    {n : Nat}
+    (H : Matrix (Fin n) (Fin n) Real)
+    (Z : RandomMatrix Omega n n)
+    (hChain : troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Z) :
+    troppMasterTraceMGFStep_statement (P := P) H Z :=
+  HighDimProb.troppMasterTraceMGFStep_of_liebJensen H Z hChain
+    (liebJensenTraceExp_statement_of_liebConcavity
+      (P := P) H (fun omega => HighDimProb.matrixExp (Z omega)))
+    (fun omega => HighDimProb.matrixExpLogSelfAdjointNormalization (Z omega))
+
+/-- Conditional Tropp one-step bound from the explicit Epstein affine-line
+hypothesis.
+
+This discharges the Lieb/Jensen part of the one-step trace-MGF primitive, while
+keeping the original statement's self-adjointness, integrability, and mean
+strict-positivity inputs explicit. -/
+theorem troppMasterTraceMGFStep_of_epsteinAffineLine
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    (hEpstein : EpsteinAffineLineConcavity)
+    {n : Nat}
+    (H : Matrix (Fin n) (Fin n) Real)
+    (Z : RandomMatrix Omega n n) :
+    HighDimProb.troppMasterTraceMGFStep_statement (P := P) H Z := by
+  intro hH hZ hTraceInt hExpInt hExpMeanSA hExpMeanPos
+  have hIntegrandEq :
+      (fun omega => HighDimProb.traceMatrixExp
+        (H + CFC.log (HighDimProb.matrixExp (Z omega)))) =
+        (fun omega => HighDimProb.traceMatrixExp (H + Z omega)) := by
+    funext omega
+    rw [HighDimProb.matrixExpLogSelfAdjointNormalization (Z omega) (hZ omega)]
+  have hTraceLogInt : HighDimProb.IntegrableRealRandomVariable P
+      (fun omega => HighDimProb.traceMatrixExp
+        (H + CFC.log (HighDimProb.matrixExp (Z omega)))) := by
+    rw [hIntegrandEq]
+    exact hTraceInt
+  have hJensen :=
+    liebJensenTraceExp_of_epsteinAffineLine (P := P) hEpstein H
+      (fun omega => HighDimProb.matrixExp (Z omega))
+      hH
+      (fun omega => HighDimProb.isSelfAdjointMatrix_matrixExp (hZ omega))
+      (fun omega =>
+        (HighDimProb.matrixExpLogDomainForSelfAdjoint (Z omega) (hZ omega)).2.1)
+      hExpInt hExpMeanSA hExpMeanPos hTraceLogInt
+  rw [← hIntegrandEq]
+  exact hJensen
+
+/-- Conditional Tropp one-step-to-`K` trace bound from the explicit Epstein
+hypothesis plus the provider log-order bridge. -/
+theorem troppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrder
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    (hEpstein : EpsteinAffineLineConcavity)
+    {n : Nat}
+    (H K : Matrix (Fin n) (Fin n) Real)
+    (Z : HighDimProb.RandomMatrix Omega n n)
+    (hH : HighDimProb.IsSelfAdjointMatrix H)
+    (hZ : HighDimProb.RandomSelfAdjointMatrix P Z)
+    (hTraceInt : HighDimProb.IntegrableRealRandomVariable P
+      (fun omega => HighDimProb.traceMatrixExp (H + Z omega)))
+    (hExpInt : HighDimProb.IntegrableRandomMatrix P
+      (fun omega => HighDimProb.matrixExp (Z omega)))
+    (hExpMeanSA : HighDimProb.IsSelfAdjointMatrix
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega))))
+    (hExpMeanPos : IsStrictlyPositive
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega))))
+    (hKSA : HighDimProb.IsSelfAdjointMatrix K)
+    (hMGF : HighDimProb.MatrixLE
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega)))
+      (HighDimProb.matrixExp K)) :
+    HighDimProb.expect P (fun omega => HighDimProb.traceMatrixExp (H + Z omega)) <=
+      HighDimProb.traceMatrixExp (H + K) := by
+  have hStep : HighDimProb.troppMasterTraceMGFStep_statement (P := P) H Z :=
+    troppMasterTraceMGFStep_of_epsteinAffineLine (P := P) hEpstein H Z
+  have hBridge :
+      HighDimProb.troppLogExpComparisonToK_statement H
+        (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega))) K :=
+    troppLogExpComparisonToK_of_providerLogOrder
+      H
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega)))
+      K
+  exact
+    HighDimProb.troppMasterTraceMGFStep_trace_bound_of_logExpComparisonToK
+      H K Z hStep hBridge hH hZ hTraceInt hExpInt hExpMeanSA hExpMeanPos
+      hKSA hMGF
+/-- Thin Tropp one-step-to-`K` composition from the provider Jensen and
+log-order bridges.
+
+This theorem keeps the hard one-step chain and trace-exp monotonicity bridge
+explicit. It only composes existing provider wrappers with the main
+HighDimProb trace-bound theorem. -/
+theorem troppMasterTraceMGFStep_trace_bound_of_providerJensen_and_logOrder
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    {n : Nat}
+    (H K : Matrix (Fin n) (Fin n) Real)
+    (Z : HighDimProb.RandomMatrix Omega n n)
+    (hChain : HighDimProb.troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Z)
+    (hTraceMono : HighDimProb.traceMatrixExp_mono_add_selfAdjoint_statement H
+      (CFC.log (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega)))) K)
+    (hH : HighDimProb.IsSelfAdjointMatrix H)
+    (hZ : HighDimProb.RandomSelfAdjointMatrix P Z)
+    (hTraceInt : HighDimProb.IntegrableRealRandomVariable P
+      (fun omega => HighDimProb.traceMatrixExp (H + Z omega)))
+    (hExpInt : HighDimProb.IntegrableRandomMatrix P
+      (fun omega => HighDimProb.matrixExp (Z omega)))
+    (hExpMeanSA : HighDimProb.IsSelfAdjointMatrix
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega))))
+    (hExpMeanPos : IsStrictlyPositive
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega))))
+    (hKSA : HighDimProb.IsSelfAdjointMatrix K)
+    (hMGF : HighDimProb.MatrixLE
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega)))
+      (HighDimProb.matrixExp K)) :
+    HighDimProb.expect P (fun omega => HighDimProb.traceMatrixExp (H + Z omega)) <=
+      HighDimProb.traceMatrixExp (H + K) := by
+  let hStep := troppMasterTraceMGFStep_of_providerJensen (P := P) H Z hChain
+  let hBridge :=
+    troppLogExpComparisonToK_of_traceMatrixExp_mono_add_selfAdjoint
+      H
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega)))
+      K
+      hTraceMono
+  exact
+    HighDimProb.troppMasterTraceMGFStep_trace_bound_of_logExpComparisonToK
+      H K Z hStep hBridge hH hZ hTraceInt hExpInt hExpMeanSA hExpMeanPos
+      hKSA hMGF
+
+
+/-- Thin Tropp one-step-to-`K` composition from the provider Jensen and
+provider log-order bridges.
+
+This theorem keeps the hard one-step chain explicit, but discharges the
+trace-exp monotonicity bridge internally via the provider theorem
+`traceMatrixExp_mono_add_selfAdjoint`. It only composes existing provider
+wrappers with the main HighDimProb trace-bound theorem. -/
+theorem troppMasterTraceMGFStep_trace_bound_of_providerJensen_and_providerLogOrder
+    {Omega : Type*} [MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    {n : Nat}
+    (H K : Matrix (Fin n) (Fin n) Real)
+    (Z : HighDimProb.RandomMatrix Omega n n)
+    (hChain : HighDimProb.troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Z)
+    (hH : HighDimProb.IsSelfAdjointMatrix H)
+    (hZ : HighDimProb.RandomSelfAdjointMatrix P Z)
+    (hTraceInt : HighDimProb.IntegrableRealRandomVariable P
+      (fun omega => HighDimProb.traceMatrixExp (H + Z omega)))
+    (hExpInt : HighDimProb.IntegrableRandomMatrix P
+      (fun omega => HighDimProb.matrixExp (Z omega)))
+    (hExpMeanSA : HighDimProb.IsSelfAdjointMatrix
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega))))
+    (hExpMeanPos : IsStrictlyPositive
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega))))
+    (hKSA : HighDimProb.IsSelfAdjointMatrix K)
+    (hMGF : HighDimProb.MatrixLE
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega)))
+      (HighDimProb.matrixExp K)) :
+    HighDimProb.expect P (fun omega => HighDimProb.traceMatrixExp (H + Z omega)) <=
+      HighDimProb.traceMatrixExp (H + K) := by
+  have hStep : HighDimProb.troppMasterTraceMGFStep_statement (P := P) H Z :=
+    troppMasterTraceMGFStep_of_providerJensen (P := P) H Z hChain
+  have hBridge :
+      HighDimProb.troppLogExpComparisonToK_statement H
+        (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega))) K :=
+    troppLogExpComparisonToK_of_providerLogOrder
+      H
+      (HighDimProb.matrixExpect P (fun omega => HighDimProb.matrixExp (Z omega)))
+      K
+  exact
+    HighDimProb.troppMasterTraceMGFStep_trace_bound_of_logExpComparisonToK
+      H K Z hStep hBridge hH hZ hTraceInt hExpInt hExpMeanSA hExpMeanPos
+      hKSA hMGF
+end
+
+end HighDimProb
diff --git a/HighDimProbJudge.lean b/HighDimProbJudge.lean
index bfed956..cd7bd60 100644
--- a/HighDimProbJudge.lean
+++ b/HighDimProbJudge.lean
@@ -18,3 +18,4 @@ import HighDimProbJudge.RandomMatrix.SpectralUse
 import HighDimProbJudge.RandomMatrix.TraceExpUse
 import HighDimProbJudge.RandomMatrix.LaplaceUse
 import HighDimProbJudge.RandomMatrix.MatrixBernsteinUse
+import HighDimProbJudge.RandomMatrix.LiebProviderUse
diff --git a/HighDimProbJudge/RandomMatrix/LiebProviderUse.lean b/HighDimProbJudge/RandomMatrix/LiebProviderUse.lean
new file mode 100644
index 0000000..ab4d8e6
--- /dev/null
+++ b/HighDimProbJudge/RandomMatrix/LiebProviderUse.lean
@@ -0,0 +1,16 @@
+import HighDimProb.RandomMatrix.LiebProvider
+import HighDimProb.RandomMatrix.ConcentrationStatements
+
+#check HighDimProb.operatorLogMonotoneOnPositiveMatrices
+#check HighDimProb.traceMatrixExp_mono_add_selfAdjoint
+#check HighDimProb.troppLogExpComparisonToK_of_providerLogOrder
+#check HighDimProb.EpsteinAffineLineConcavity
+#check HighDimProb.troppMasterTraceMGFStep_of_epsteinAffineLine
+#check HighDimProb.troppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrder
+#check HighDimProb.troppNaturalHistoryMeasurable_of_suffix_entry_measurable
+#check HighDimProb.matrixExpScaledIntegrable_of_provider_finiteMeasure
+#check HighDimProb.traceExpIntegrable_troppStateHistory_add_step_of_operatorNormBounds_finiteMeasure
+#check HighDimProb.traceExpIntegrable_troppStateHistory_add_K_of_operatorNormBounds_finiteMeasure
+#check HighDimProb.matrixExpSupportDomination_identity
+#check HighDimProb.MatrixBernsteinConditioningTraceMGFProviderAssumptions
+#check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions
diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean
index 70f1751..f18795a 100644
--- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean
+++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean
@@ -1,5 +1,6 @@
 import HighDimProb.RandomMatrix.CStarBridge
 import HighDimProb.RandomMatrix.HardboneStatements
+import HighDimProb.RandomMatrix.LiebProvider
 
 open MeasureTheory
 open HighDimProb
@@ -25,6 +26,19 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #check bernsteinCFCExpressionNormalization_statement
 #check bernsteinMatrixExp_le_quadratic_of_cfcChain_statement
 #check operatorLogMonotoneOnPositiveMatrices_statement
+#check operatorLogMonotoneOnPositiveMatrices
+#check traceMatrixExp_mono_add_selfAdjoint
+#check troppLogExpComparisonToK_of_providerLogOrder
+#check EpsteinAffineLineConcavity
+#check liebTraceExpConcavity_of_epsteinAffineLine
+#check liebJensenTraceExp_statement_of_epsteinAffineLine
+#check troppMasterTraceMGFStep_of_epsteinAffineLine
+#check troppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrder
+#check troppNaturalHistoryMeasurable_of_suffix_entry_measurable
+#check matrixExpScaledIntegrable_of_provider_finiteMeasure
+#check traceExpIntegrable_troppStateHistory_add_step_of_operatorNormBounds_finiteMeasure
+#check traceExpIntegrable_troppStateHistory_add_K_of_operatorNormBounds_finiteMeasure
+#check matrixExpSupportDomination_identity
 #check matrixExpLogDomainForSelfAdjoint_statement
 #check matrixLog_le_of_le_matrixExp_statement
 #check matrixLog_le_of_le_matrixExp
diff --git a/HighDimProbTest/RandomMatrixLiebProviderAPI.lean b/HighDimProbTest/RandomMatrixLiebProviderAPI.lean
new file mode 100644
index 0000000..989e000
--- /dev/null
+++ b/HighDimProbTest/RandomMatrixLiebProviderAPI.lean
@@ -0,0 +1,23 @@
+import HighDimProb.RandomMatrix.LiebProvider
+import HighDimProb.RandomMatrix.ConcentrationStatements
+
+open MeasureTheory
+open HighDimProb
+open scoped MatrixOrder Matrix.Norms.Operator Matrix.Norms.L2Operator
+
+#check operatorLogMonotoneOnPositiveMatrices
+#check traceMatrixExp_mono_add_selfAdjoint
+#check troppLogExpComparisonToK_of_providerLogOrder
+#check EpsteinAffineLineConcavity
+#check liebTraceExpConcavity_of_epsteinAffineLine
+#check liebJensenTraceExp_statement_of_epsteinAffineLine
+#check troppMasterTraceMGFStep_of_epsteinAffineLine
+#check troppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrder
+#check troppNaturalHistoryMeasurable_of_suffix_entry_measurable
+#check matrixExpScaledIntegrable_of_provider_finiteMeasure
+#check traceExpIntegrable_troppStateHistory_add_step_of_operatorNormBounds_finiteMeasure
+#check traceExpIntegrable_troppStateHistory_add_K_of_operatorNormBounds_finiteMeasure
+#check matrixExpSupportDomination_identity
+#check MatrixBernsteinConditioningTraceMGFProviderAssumptions
+#check MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions
+#check matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions
diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md
index 4427351..a55cfd0 100644
--- a/docs/RandomMatrixAPI.md
+++ b/docs/RandomMatrixAPI.md
@@ -109,21 +109,29 @@ Bernstein CFC chain:
 Log/order-to-`K` chain:
 
 - `operatorLogMonotoneOnPositiveMatrices_statement`
+- `operatorLogMonotoneOnPositiveMatrices`
 - `matrixExpLogDomainForSelfAdjoint_statement`
 - `matrixExpLogDomainForSelfAdjoint`
 - `matrixLog_le_of_le_matrixExp_statement`
 - `matrixLog_le_of_le_matrixExp`
 - `traceMatrixExp_mono_add_selfAdjoint_statement`
+- `traceMatrixExp_mono_add_selfAdjoint`
+- `troppLogExpComparisonToK_of_providerLogOrder`
 - `troppLogExpComparisonToK_of_logOrderKChain_statement`
 
 Tropp/Lieb/Golden-Thompson chain:
 
 - `liebTraceExpConcavity_statement`
+- `EpsteinAffineLineConcavity`
+- `liebTraceExpConcavity_of_epsteinAffineLine`
+- `liebJensenTraceExp_statement_of_epsteinAffineLine`
 - `liebJensenTraceExp_statement`
 - `goldenThompsonTraceExp_statement`
 - `matrixExpLogSelfAdjointNormalization_statement`
 - `matrixExpLogSelfAdjointNormalization`
 - `troppMasterTraceMGFStep_of_liebJensen_statement`
+- `troppMasterTraceMGFStep_of_epsteinAffineLine`
+- `troppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrder`
 
 Conditioning / independence chain:
 
@@ -132,12 +140,16 @@ Conditioning / independence chain:
 - `condExp_traceExp_history_add_independent_step_statement`
 - `troppConditionalStep_of_iIndepFun_statement`
 - `troppConditionalStep_of_iIndepFun`
+- `troppNaturalHistoryMeasurable_of_suffix_entry_measurable`
 
 Integrability provider chain:
 
 - `matrixExpScaledIntegrable_of_provider_statement`
+- `matrixExpScaledIntegrable_of_provider_finiteMeasure`
 - `traceExpIntegrable_troppStateHistory_add_step_statement`
+- `traceExpIntegrable_troppStateHistory_add_step_of_operatorNormBounds_finiteMeasure`
 - `traceExpIntegrable_troppStateHistory_add_K_statement`
+- `traceExpIntegrable_troppStateHistory_add_K_of_operatorNormBounds_finiteMeasure`
 - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement`
 
 Variance-proxy / centered-square chain:
@@ -185,6 +197,7 @@ Thin hardbone consumers:
 - `troppLogExpComparisonToK_of_logMonotone_traceExpMono`
 - `troppMasterTraceMGFStep_of_liebJensen`
 - `troppConditionalStep_of_iIndepFun`
+- `troppNaturalHistoryMeasurable_of_suffix_entry_measurable`
 - `troppMasterTraceMGFConditionalStep_of_conditioningBridge`
 - `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge`
 - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider`
@@ -197,6 +210,10 @@ Thin hardbone consumers:
 - `traceMatrixExp_excess_supportDim_exp_lambdaMax`
 - `traceMatrixExp_effectiveRank_bound`
 - `traceMatrixExp_effectiveRank_bound_of_ambientTraceCertificate`
+- `matrixExpSupportDomination_identity`
+- `MatrixBernsteinConditioningTraceMGFProviderAssumptions`
+- `MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions`
+- `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions`
 
 Hardbone status table:
 
@@ -204,14 +221,14 @@ Hardbone status table:
 |---|---|---|---|---|
 | Scalar Bernstein hardbone leaf | `scalarBernsteinExpQuadraticInequality_statement` | proven by `scalarBernsteinExpQuadraticInequality` | CFC-chain assumptions can reuse the proved scalar theorem | none for this scalar leaf |
 | Bernstein CFC | `bernsteinMatrixExp_le_quadratic_statement` | proven by `bernsteinMatrixExp_le_quadratic` | `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` documents the reusable composition | preferred `*_of_troppAssumptions` wrappers bypass pointwise CFC fields; explicit-CFC wrappers remain for compatibility |
-| Matrix log/order bridge | `matrixLog_le_of_le_matrixExp_statement` | proven by `matrixLog_le_of_le_matrixExp` | turns explicit log-monotonicity and `matrixExp` log-domain premises into `log M <= K` | `matrixExp` log-domain is supplied by `matrixExpLogDomainForSelfAdjoint`; operator-log monotonicity remains the external input |
+| Matrix log/order bridge | `matrixLog_le_of_le_matrixExp_statement` | proven by `matrixLog_le_of_le_matrixExp`; `operatorLogMonotoneOnPositiveMatrices` is now ported | turns explicit log-monotonicity and `matrixExp` log-domain premises into `log M <= K`; `troppLogExpComparisonToK_of_providerLogOrder` closes the deterministic log/trace-exp route | none for the deterministic provider leaf; downstream Lieb/conditioning assumptions remain separate |
 | Real-to-CStar bridge | `realMatrixToCStarMatrix` and transport statement targets | basic representation map, add/sub, and self-adjoint transport proved | exposes the CStar representation route for future operator-log monotonicity proofs | strict positivity/order/log-back transport from real matrices to `CStarMatrix` remains open |
-| Log/order-to-`K` | `troppLogExpComparisonToK_of_logOrderKChain_statement` | typed-prop | `troppLogExpComparisonToK_of_logMonotone_traceExpMono` | trace-exp monotonicity plus the explicit log/order bridge inputs |
-| Tropp/Lieb/GT one-step | `troppMasterTraceMGFStep_of_liebJensen_statement` | typed-prop | `troppMasterTraceMGFStep_of_liebJensen` | Lieb concavity, probability-measure Jensen, log-exp normalization; Golden-Thompson is separate |
+| Log/order-to-`K` | `troppLogExpComparisonToK_of_logOrderKChain_statement` | provider leaf proved by `troppLogExpComparisonToK_of_providerLogOrder` | `troppLogExpComparisonToK_of_logMonotone_traceExpMono`; direct provider wrapper available | no Lieb/Jensen/conditioning claim from this deterministic route |
+| Tropp/Lieb/GT one-step | `troppMasterTraceMGFStep_of_liebJensen_statement` | conditional provider route proved from explicit `EpsteinAffineLineConcavity` | `troppMasterTraceMGFStep_of_liebJensen`; `troppMasterTraceMGFStep_of_epsteinAffineLine`; `troppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrder` | unconditional Epstein/Lieb theorem remains open; Golden-Thompson is separate |
 | Conditioning / independence | `troppConditionalStep_of_iIndepFun_statement` | proven by `troppConditionalStep_of_iIndepFun` | `troppMasterTraceMGFConditionalStep_of_conditioningBridge`; `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge` composes this route into the finite-family trace-MGF bound | thin forwarder/composer only; generated histories, history/current-step independence, finite-family independence, conditional expectation reduction, integrability, and variance-proxy inputs remain explicit premises |
-| Trace-exp integrability | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement` | typed-prop with proved thin consumer | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider` | automatic absolute domination, Golden-Thompson/product, or boundedness provider |
+| Trace-exp integrability | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement` plus bounded S9/S10 provider fields | typed-prop with proved thin consumer; bounded finite-measure provider leaves ported | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider`; `MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions` | full-sum trace integrability still explicit; bounded provider leaves require finite measure and operator-norm bounds |
 | Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement`, `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion, finite-sum MatrixLE bookkeeping, PSD Loewner-to-operator-norm monotonicity, and centered rank-one second-moment comparison proved; typed-prop chain has proved thin consumers | `matrixSquare_centeredRandomMatrix_expectation_expansion`, `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment`, `centeredRankOneSquare_le_rankOneSecondMoment`, `varianceProxyNormBound_of_centeredSquareChain`, `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`, `varianceProxyNormBound_of_centeredSquareChain_of_normMono`, `varianceProxyNormBound_of_centeredSquareChain_expansion`, `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment`, `deterministicMatrixVarianceProxyNorm_sum_le_sum`, `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound`, `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, exact-row centered-square sample-covariance wrappers and bundles, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_products`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two`, `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` | full generic centered-square-chain providers, Tropp/Lieb, trace-MGF integrability, and full Matrix Bernstein remain explicit or open |
-| Dimension / support / effective rank | `traceMatrixExp_le_rank_exp_lambdaMax_statement`, `traceMatrixExp_le_supportDim_exp_lambdaMax_statement`, `traceMatrixExp_effectiveRank_bound_statement`, `matrixExpSupportDomination_identity_statement`, `traceMatrixExp_excess_supportDim_exp_lambdaMax_statement` | rank/support targets and effective-rank consumer proved under explicit support, PSD, lambda-max, and trace-certificate assumptions; ambient trace certificate and star-projection rank/PSD consumer proved; identity support provider target named only; excess trace bridge and supportDim consumer proved under explicit excess certificate | `traceMatrixExp_le_rank_exp_lambdaMax`, `traceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjection`, `traceMatrixExp_le_supportDim_exp_lambdaMax`, `traceMatrixExp_excess_supportDim_exp_lambdaMax`, `traceMatrixExp_effectiveRank_bound`, `traceMatrixExp_effectiveRank_bound_of_ambientTraceCertificate`; deterministic helpers include `MatrixExpSupportDomination`, `MatrixExpExcessSupportDomination`, `traceMatrixExp_le_card_add_trace_support_mul_exp_sub_one_of_excessSupportDomination`, `traceMatrixExp_eq_sum_exp_eigenvalues`, `traceMatrixExp_smul_le_card_add_trace_div_mul_exp_sub_one_of_psd_lambdaMax_le`, `matrixTrace_le_card_mul_of_isPSD_lambdaMaxOrdered_le`, `matrixTrace_eq_rank_of_isStarProjection`, `isPSDMatrix_of_isStarProjection` | identity/excess support-domination providers and support-construction certificates; true effective-rank trace certificate provider beyond ambient dimension |
+| Dimension / support / effective rank | `traceMatrixExp_le_rank_exp_lambdaMax_statement`, `traceMatrixExp_le_supportDim_exp_lambdaMax_statement`, `traceMatrixExp_effectiveRank_bound_statement`, `matrixExpSupportDomination_identity_statement`, `traceMatrixExp_excess_supportDim_exp_lambdaMax_statement` | rank/support targets and effective-rank consumer proved under explicit support, PSD, lambda-max, and trace-certificate assumptions; ambient trace certificate and star-projection rank/PSD consumer proved; identity support provider proved by `matrixExpSupportDomination_identity`; excess trace bridge and supportDim consumer proved under explicit excess certificate | `traceMatrixExp_le_rank_exp_lambdaMax`, `traceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjection`, `traceMatrixExp_le_supportDim_exp_lambdaMax`, `traceMatrixExp_excess_supportDim_exp_lambdaMax`, `traceMatrixExp_effectiveRank_bound`, `traceMatrixExp_effectiveRank_bound_of_ambientTraceCertificate`; deterministic helpers include `MatrixExpSupportDomination`, `MatrixExpExcessSupportDomination`, `traceMatrixExp_le_card_add_trace_support_mul_exp_sub_one_of_excessSupportDomination`, `traceMatrixExp_eq_sum_exp_eigenvalues`, `traceMatrixExp_smul_le_card_add_trace_div_mul_exp_sub_one_of_psd_lambdaMax_le`, `matrixTrace_le_card_mul_of_isPSD_lambdaMaxOrdered_le`, `matrixTrace_eq_rank_of_isStarProjection`, `isPSDMatrix_of_isStarProjection` | identity/excess support-domination providers and support-construction certificates; true effective-rank trace certificate provider beyond ambient dimension |
 | Thin consumers | `troppMasterTraceMGFConditionalStep_of_conditioningBridge`, `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge` | proven | source/test/judge checks | thin developer-facing wrappers only; no hard fact is discharged |
 
 Most hardbone declarations are typed `Prop` contracts, not hard theorem proofs.
diff --git a/docs/STATEMENTS.md b/docs/STATEMENTS.md
index 30e10b0..0f1b547 100644
--- a/docs/STATEMENTS.md
+++ b/docs/STATEMENTS.md
@@ -81,4 +81,196 @@ Non-goals for this consumer:
   independence conditioning, conditional-expectation reduction, trace-exp
   integrability propagation, strict positivity of matrix-exponential means,
   variance-proxy control, Lieb/Jensen, Golden-Thompson, theta optimization,
-  dimension/rank reduction, or full Matrix Bernstein.
\ No newline at end of file
+  dimension/rank reduction, or full Matrix Bernstein.
+
+## RM-LIEB-S11: provider-backed deterministic log/order and trace-exp monotonicity
+
+Consumer targets:
+
+- `operatorLogMonotoneOnPositiveMatrices_statement`
+- `traceMatrixExp_mono_add_selfAdjoint_statement`
+- `troppLogExpComparisonToK_statement`
+
+The sibling proof-provider repository `/workspace/projects/HighDimProbLiebProvider`
+contains provider proofs for the first two exact HighDimProb statement surfaces
+and a thin composition to the deterministic Tropp log/`K` comparison.  A
+HighDimProb theorem-push task may therefore advance past the old CStar transport
+and trace-exponential monotonicity blockers by importing or porting those
+provider facts, rather than treating them as open analytic assumptions.
+
+Provider facts consumed by the main-repo port:
+
+Main-repo port status (2026-06-26): these deterministic leaves are now exposed
+in `HighDimProb.RandomMatrix.LiebProvider` as
+`operatorLogMonotoneOnPositiveMatrices`,
+`traceMatrixExp_mono_add_selfAdjoint`, and
+`troppLogExpComparisonToK_of_providerLogOrder`.
+
+- `HighDimProbLiebProvider.operatorLogMonotoneOnPositiveMatrices`, discharging
+  `operatorLogMonotoneOnPositiveMatrices_statement` through real-to-`CStarMatrix`
+  strict-positivity, Loewner-order, and `CFC.log` transport.
+- `HighDimProbLiebProvider.traceMatrixExp_mono_add_selfAdjoint`, discharging
+  `traceMatrixExp_mono_add_selfAdjoint_statement` through the affine derivative
+  of trace exponential and PSD trace-product nonnegativity.
+- `HighDimProbLiebProvider.troppLogExpComparisonToK_of_providerLogOrder`, a
+  deterministic bridge from provider log/order plus provider trace-exp
+  monotonicity to `troppLogExpComparisonToK_statement`.
+
+Remaining assumptions and side conditions at this layer:
+
+- Matrix self-adjointness, strict positivity, and `MatrixLE` hypotheses remain
+  exactly those in the HighDimProb statement surfaces.
+- `matrixExpLogDomainForSelfAdjoint_statement` remains the local log-domain and
+  `CFC.log (matrixExp K) = K` normalization input for the log-to-`K` route.
+- The provider import boundary is resolved by porting the exact theorem bodies
+  into HighDimProb; no reverse Lake dependency on the provider repo is used.
+
+Non-goals for this provider-ingestion step:
+
+- It does not prove Lieb concavity, Epstein concavity, Jensen, Golden-Thompson,
+  conditional expectation, trace-MGF iteration, variance-proxy control, or full
+  Matrix Bernstein.
+- It should not rename deterministic log/order progress as a full Tropp/Lieb
+  matrix-MGF theorem.
+
+## RM-LIEB-S12: conditional Epstein affine-line route to Tropp one-step
+
+Consumer targets:
+
+- `liebTraceExpConcavity_statement`
+- `liebJensenTraceExp_statement`
+- `troppMasterTraceMGFStep_statement`
+- the one-step-to-`K` trace bound obtained by composing the Tropp one-step with
+  `troppLogExpComparisonToK_statement`
+
+The proof-provider repository has reduced the hard Lieb input to one explicit
+finite-dimensional affine-line hypothesis.  A theorem-push task may use this as
+the aggressive replacement for the older fully opaque Lieb/Jensen assumption,
+while keeping the affine-line analytic theorem visible in this ledger.
+
+Primary foundational assumption:
+
+- `EpsteinAffineLineConcavity`: for every finite dimension and self-adjoint
+  `H`, `A`, and `C`, if the affine segment `A + t • C` is strictly positive for
+  all `t ∈ [0, 1]`, then the scalar function
+  `t ↦ traceMatrixExp (H + CFC.log (A + t • C))` is concave on `[0, 1]`.
+
+Provider reductions consumed by the main-repo conditional port:
+
+Main-repo port status (2026-06-26): the explicit assumption and conditional
+wrappers are now exposed in `HighDimProb.RandomMatrix.LiebProvider` as
+`EpsteinAffineLineConcavity`, `liebTraceExpConcavity_of_epsteinAffineLine`,
+`liebJensenTraceExp_statement_of_epsteinAffineLine`,
+`troppMasterTraceMGFStep_of_epsteinAffineLine`, and
+`troppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrder`.
+
+- `HighDimProbLiebProvider.liebTraceExpConcavity_of_epsteinAffineLine`
+- `HighDimProbLiebProvider.liebJensenTraceExp_statement_of_epsteinAffineLine`
+- `HighDimProbLiebProvider.troppMasterTraceMGFStep_of_epsteinAffineLine`
+- `HighDimProbLiebProvider.troppMasterTraceMGFStep_trace_bound_of_epsteinAffineLine_and_providerLogOrder`
+
+Proof-facing refinements of the foundational assumption:
+
+- It is enough to prove linewise first and second derivative data on the open
+  interval, with second derivative nonpositive, as packaged by
+  `epsteinAffineLineConcavity_of_hasDerivAt2_nonpos` or
+  `epsteinAffineLineConcavity_of_hasDerivWithinAt2_nonpos`.
+- A still narrower route is to prove the `CFC.log` affine-line derivative and
+  scalar trace-derivative nonpositivity consumed by
+  `epsteinAffineLineConcavity_of_cfcLog_hasDerivAt_traceDerivative_nonpos`.
+
+Side conditions that remain explicit when this assumption is consumed by the
+Tropp one-step route:
+
+- `IsSelfAdjointMatrix H`.
+- `RandomSelfAdjointMatrix P Z`.
+- `IntegrableRealRandomVariable P (fun omega => traceMatrixExp (H + Z omega))`.
+- `IntegrableRandomMatrix P (fun omega => matrixExp (Z omega))`.
+- Self-adjointness and strict positivity of
+  `matrixExpect P (fun omega => matrixExp (Z omega))`.
+- For the trace-bound-to-`K` form, self-adjointness of `K` and the matrix-MGF
+  comparison
+  `MatrixLE (matrixExpect P (fun omega => matrixExp (Z omega))) (matrixExp K)`.
+
+Non-goals for this conditional Epstein route:
+
+- It does not prove unconditional Lieb concavity until
+  `EpsteinAffineLineConcavity` or an equivalent theorem is proved.
+- It does not prove Golden-Thompson, finite-family conditioning, independence,
+  integrability propagation, variance-proxy control, or full Matrix Bernstein.
+
+## RM-LIEB-S13: provider-backed S9/S10 assumption compression inputs
+
+Consumer targets:
+
+- `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge`
+- `MatrixBernsteinConditioningTraceMGFTailAssumptions`
+- `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions`
+
+The proof-provider repository has proved several bounded or conditional provider
+facts that can shrink the explicit assumption burden in the S9/S10 route.  These
+facts should be consumed as theorem-backed provider inputs, not marketed as
+unconditional Matrix Bernstein.
+
+Natural-history measurability input:
+
+Main-repo port status (2026-06-26): bounded provider facts are now exposed in
+`HighDimProb.RandomMatrix.LiebProvider`, and S10 has the compressed bundle
+`MatrixBernsteinConditioningTraceMGFProviderAssumptions` plus the converter
+`MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions` and
+tail wrapper
+`matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions`.
+
+- `HighDimProbLiebProvider.troppNaturalHistoryMeasurable_of_suffix_entry_measurable`
+  supplies `troppNaturalHistoryMeasurable_statement theta X K mHist` from
+  explicit suffix-entry measurability: for every history index `i`, every suffix
+  index `j` with `i.succ ≤ j`, and every matrix entry `r c`, the coordinate map
+  `fun omega => X j omega r c` is measurable with respect to `mHist i`.
+
+Bounded finite-measure integrability inputs:
+
+- `HighDimProbLiebProvider.matrixExpScaledIntegrable_of_provider_finiteMeasure`
+  supplies scaled matrix-exponential integrability from finite measure,
+  pointwise random-matrix measurability, self-adjoint summands, nonnegative
+  radius, and a uniform pointwise operator-norm bound.
+- `HighDimProbLiebProvider.traceExpIntegrable_troppStateHistory_add_step_of_operatorNormBounds_finiteMeasure`
+  supplies trace-exponential integrability of
+  `troppStateHistory theta X K i + troppCurrentRandomStep theta X i` from finite
+  measure, measurability, self-adjointness, and pointwise operator-norm bounds
+  on both terms.
+- `HighDimProbLiebProvider.traceExpIntegrable_troppStateHistory_add_K_of_operatorNormBounds_finiteMeasure`
+  supplies trace-exponential integrability of
+  `troppStateHistory theta X K i + K i` from finite measure, measurability,
+  self-adjointness, and pointwise operator-norm bounds on the random history and
+  deterministic comparison matrix.
+
+Support-side deterministic provider input:
+
+- `HighDimProbLiebProvider.matrixExpSupportDomination_identity` proves
+  `matrixExpSupportDomination_identity_statement`, giving the ambient identity
+  support certificate for self-adjoint matrices.  This is useful for provider
+  compression of dimension/support trace-exp bounds, but it only gives the
+  ambient cardinality route and no true low-rank/effective-rank provider.
+
+Remaining assumptions for an S9/S10 theorem-push after these provider inputs:
+
+- The exact independence bridge
+  `troppHistoryStepIndependent_of_iIndepFun_statement` still needs an honest
+  contract with the measurability or `AEMeasurable` hypotheses required by
+  Mathlib independence APIs.
+- The conditional-expectation bridge
+  `condExp_traceExp_history_add_independent_step_statement` still needs an
+  honest contract that includes independence of the history sigma-algebra from
+  the current step, not merely an unparameterized `IndepFun H Z P` premise.
+- The bounded integrability providers require a finite-measure instance and
+  explicit operator-norm bounds; if the exact HighDimProb target omits these,
+  add a bounded-provider wrapper instead of pretending the original target was
+  discharged.
+
+Non-goals for this S9/S10 compression step:
+
+- It does not prove the finite-family independence bridge, conditional
+  expectation reduction, Lieb/Epstein, Golden-Thompson, variance-proxy control,
+  theta optimization, or full Matrix Bernstein.
+- It should reduce explicit assumption burden only where the provider theorem
+  actually supplies a named premise.
diff --git a/docs/Status.md b/docs/Status.md
index 718e5b3..c41d261 100644
--- a/docs/Status.md
+++ b/docs/Status.md
@@ -366,6 +366,25 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact
   `RM-LIEB-S4-real-matrix-to-cstar-log-monotonicity-contract`, proving that Mathlib `CFC.log_le_log` is available on `CStarMatrix (Fin n) (Fin n) ℂ` while leaving real-matrix transport open.
 - Completed hardbone contract leaf:
   `RM-LIEB-S5-real-to-cstar-transport-api-contract`, proving the basic real-to-`CStarMatrix` transport shape in a probe, including entrywise, add/sub, and self-adjoint transport; positivity/order/log transport remains provider work, not a current main-repository completion.
+
+- Completed provider theorem-push leaf:
+  `RM-LIEB-S11-provider-log-order-trace-mono-ingestion`, porting the deterministic
+  operator-log monotonicity, trace-exponential monotonicity, and direct
+  `troppLogExpComparisonToK_of_providerLogOrder` leaves into
+  `HighDimProb.RandomMatrix.LiebProvider`. This does not prove Lieb/Jensen or
+  any conditioning theorem.
+- Completed conditional provider theorem-push leaf:
+  `RM-LIEB-S12-epstein-affine-line-conditional-tropp-step`, exposing
+  `EpsteinAffineLineConcavity` and conditional Lieb/Jensen/Tropp one-step
+  wrappers. The Epstein affine-line theorem remains an explicit assumption.
+- Completed provider-compression scaffold:
+  `RM-LIEB-S13-s9-s10-provider-assumption-compression`, adding bounded
+  finite-measure integrability providers, suffix-entry natural-history
+  measurability, identity support domination, and the compressed S10 bundle
+  `MatrixBernsteinConditioningTraceMGFProviderAssumptions`. Independence,
+  conditional expectation, variance proxy, full-sum trace integrability, and
+  tail-side assumptions remain explicit.
+
 - Progress-first hardbone scaffold:
   `RM-LIEB-S9-conditional-step-assumption-composition-contract`, adding `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge` as a finite-family trace-MGF consumer from explicit conditioning, natural-state, integrability, and variance-proxy assumptions. The hard assumptions consumed by the theorem are recorded in `docs/STATEMENTS.md`; this does not prove those assumptions.
 - Progress-first hardbone scaffold:
diff --git a/docs/TestPlan.md b/docs/TestPlan.md
index 257b073..0b9b008 100644
--- a/docs/TestPlan.md
+++ b/docs/TestPlan.md
@@ -35,6 +35,12 @@ git diff --check
   `HighDimProbTest/RandomMatrixTraceExpAPI.lean` and
   `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`; example modules, including the `StatementRoutes` statement-route index, are covered
   through `lake build HighDimProb.Examples`.
+- RandomMatrix provider-backed Lieb/Tropp ports are covered in
+  `HighDimProbTest/RandomMatrixLiebProviderAPI.lean` and
+  `HighDimProbJudge/RandomMatrix/LiebProviderUse.lean`, including S11
+  deterministic log/order and trace-exp monotonicity, S12 conditional
+  `EpsteinAffineLineConcavity` wrappers, and S13 bounded provider compression
+  bundle checks.
 - RandomMatrix hardbone statement-target checks, including the proved Bernstein
   CFC hardbone leaf, the proved matrix-exp/log normalization and log-domain leaves, the proved
   matrix log/order bridge leaf, the proved excess-support trace bridge leaf,