diff --git a/HighDimProb/RandomMatrix/Assumptions.lean b/HighDimProb/RandomMatrix/Assumptions.lean
index 00c35ef..3a4298c 100644
--- a/HighDimProb/RandomMatrix/Assumptions.lean
+++ b/HighDimProb/RandomMatrix/Assumptions.lean
@@ -110,6 +110,41 @@ theorem BoundedOperatorNorm_rankOne_of_sqNorm_bound {Omega : Type*}
   intro omega
   exact (rankOneOperatorNorm_le_vectorSqNorm (X omega)).trans (hX omega)
 
+/--
+If a random matrix and its deterministic entrywise expectation have explicit
+operator-norm bounds, then the centered random matrix is bounded by the sum of
+those two bounds.
+
+This is only an algebraic triangle-inequality wrapper around the existing
+`matrixExpect` / `centeredRandomMatrix` vocabulary. It does not prove
+entrywise integrability, measurability, or any contraction theorem bounding
+`||E X||op` from the pointwise bound on `X`; the expectation norm bound is an
+explicit hypothesis.
+
+Formula reference: centering uses `X(omega) - E X`, and the proof is the
+operator-norm triangle inequality `||X(omega) - E X|| <= ||X(omega)|| +
+||E X||`; see https://en.wikipedia.org/wiki/Operator_norm and the sample
+covariance/expectation background at
+https://en.wikipedia.org/wiki/Sample_mean_and_covariance
+-/
+theorem BoundedOperatorNorm_centered_of_bound_expect_bound {Omega : Type*}
+    [MeasurableSpace Omega] {m n : Nat}
+    (P : Measure Omega) (X : RandomMatrix Omega m n) (R Rexp : Real)
+    (hX : BoundedOperatorNorm X R)
+    (hExp : deterministicOperatorNorm (matrixExpect P X) <= Rexp) :
+    BoundedOperatorNorm (centeredRandomMatrix P X) (R + Rexp) := by
+  intro omega
+  have hTri :
+      deterministicOperatorNorm (X omega - matrixExpect P X) <=
+        deterministicOperatorNorm (X omega) +
+          deterministicOperatorNorm (matrixExpect P X) :=
+    deterministicOperatorNorm_sub_le_add (X omega) (matrixExpect P X)
+  have hBound :
+      deterministicOperatorNorm (X omega) +
+          deterministicOperatorNorm (matrixExpect P X) <= R + Rexp :=
+    add_le_add (hX omega) hExp
+  exact hTri.trans hBound
+
 /-- Pointwise uniform operator-norm bound for a matrix family. -/
 def PointwiseOperatorNormBound {Omega : Type*} [MeasurableSpace Omega]
     {I : Type*} {m n : Nat} (A : I -> RandomMatrix Omega m n)
@@ -135,6 +170,47 @@ theorem PointwiseOperatorNormBound_rankOne_of_sqNorm_bound {Omega : Type*}
   intro i
   exact BoundedOperatorNorm_rankOne_of_sqNorm_bound (X i) R hR (hX i)
 
+/--
+Family version of the centered operator-norm bridge under an explicit bound on
+each deterministic expectation.
+
+This is the family form of the algebraic wrapper above. It intentionally keeps
+the expectation operator-norm bound as a hypothesis and does not establish
+integrability or expectation contraction.
+
+Formula reference: this packages the triangle-bound route
+`||X_i(omega) - E X_i|| <= ||X_i(omega)|| + ||E X_i||`; see
+https://en.wikipedia.org/wiki/Operator_norm and
+https://en.wikipedia.org/wiki/Sample_mean_and_covariance
+-/
+theorem PointwiseOperatorNormBound_centered_of_bound_expect_bound {Omega : Type*}
+    [MeasurableSpace Omega] {I : Type*} {m n : Nat}
+    (P : Measure Omega) (X : I -> RandomMatrix Omega m n) (R Rexp : Real)
+    (hX : PointwiseOperatorNormBound X R)
+    (hExp : forall i, deterministicOperatorNorm (matrixExpect P (X i)) <= Rexp) :
+    PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (X i)) (R + Rexp) := by
+  intro i
+  exact BoundedOperatorNorm_centered_of_bound_expect_bound P (X i) R Rexp
+    (hX i) (hExp i)
+
+/--
+Same-radius centered operator-norm wrapper: if both `X_i(omega)` and
+`E X_i` are bounded by `R`, then the centered family is bounded by `R + R`.
+
+This remains an explicit-bound wrapper; the hypothesis on `E X_i` is not
+derived from the pointwise bound on `X_i`.
+
+Formula reference: this is the special case `R_exp = R` of the operator-norm
+triangle inequality; see https://en.wikipedia.org/wiki/Operator_norm
+-/
+theorem PointwiseOperatorNormBound_centered_of_bound_expect_bound_same {Omega : Type*}
+    [MeasurableSpace Omega] {I : Type*} {m n : Nat}
+    (P : Measure Omega) (X : I -> RandomMatrix Omega m n) (R : Real)
+    (hX : PointwiseOperatorNormBound X R)
+    (hExp : forall i, deterministicOperatorNorm (matrixExpect P (X i)) <= R) :
+    PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (X i)) (R + R) := by
+  exact PointwiseOperatorNormBound_centered_of_bound_expect_bound P X R R hX hExp
+
 /-- Alias emphasizing that the uniform bound is pointwise, not a.e. -/
 abbrev UniformOperatorNormBound {Omega : Type*} [MeasurableSpace Omega]
     {I : Type*} {m n : Nat} (A : I -> RandomMatrix Omega m n)
diff --git a/HighDimProb/RandomMatrix/OperatorNorm.lean b/HighDimProb/RandomMatrix/OperatorNorm.lean
index b2ac24a..4f70edc 100644
--- a/HighDimProb/RandomMatrix/OperatorNorm.lean
+++ b/HighDimProb/RandomMatrix/OperatorNorm.lean
@@ -82,6 +82,21 @@ theorem deterministicOperatorNorm_apply {m n : Nat}
     deterministicOperatorNorm A = norm A :=
   rfl
 
+/--
+The deterministic operator norm satisfies the triangle inequality for
+subtraction.
+
+Formula reference: this is the norm triangle inequality
+`||A - B|| <= ||A|| + ||B||` for the matrix norm induced by the Euclidean
+operator norm; see https://en.wikipedia.org/wiki/Operator_norm and
+https://en.wikipedia.org/wiki/Matrix_norm
+-/
+theorem deterministicOperatorNorm_sub_le_add {m n : Nat}
+    (A B : Matrix (Fin m) (Fin n) Real) :
+    deterministicOperatorNorm (A - B) <=
+      deterministicOperatorNorm A + deterministicOperatorNorm B := by
+  simpa [deterministicOperatorNorm] using norm_sub_le A B
+
 /--
 Rank-one self-outer products have operator norm bounded by the squared
 Euclidean norm of the vector.
diff --git a/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean b/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean
index 15cae12..1dbb5a9 100644
--- a/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean
+++ b/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean
@@ -1,9 +1,13 @@
 import HighDimProb.RandomMatrix
 
 #check HighDimProb.isRealRandomVariable_operatorNorm
+#check HighDimProb.deterministicOperatorNorm_sub_le_add
 #check HighDimProb.rankOneOperatorNorm_le_vectorSqNorm
 #check HighDimProb.BoundedOperatorNorm_rankOne_of_sqNorm_bound
 #check HighDimProb.PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+#check HighDimProb.BoundedOperatorNorm_centered_of_bound_expect_bound
+#check HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound
+#check HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
 
 #check
   (HighDimProb.isRealRandomVariable_operatorNorm :
@@ -25,6 +29,11 @@ example {n : Nat} (v : Fin n -> Real) :
       (fun i j : Fin n => v i * v j) <= HighDimProb.vectorSqNorm v := by
   exact HighDimProb.rankOneOperatorNorm_le_vectorSqNorm v
 
+example {m n : Nat} (A B : Matrix (Fin m) (Fin n) Real) :
+    HighDimProb.deterministicOperatorNorm (A - B) <=
+      HighDimProb.deterministicOperatorNorm A + HighDimProb.deterministicOperatorNorm B := by
+  exact HighDimProb.deterministicOperatorNorm_sub_le_add A B
+
 example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {n : Nat}
     (X : I -> Omega -> Fin n -> Real) (R : Real)
     (hR : 0 <= R)
@@ -32,3 +41,14 @@ example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {n : Nat}
     HighDimProb.PointwiseOperatorNormBound
       (fun i omega a b => X i omega a * X i omega b) R := by
   exact HighDimProb.PointwiseOperatorNormBound_rankOne_of_sqNorm_bound X R hR hX
+
+example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {m n : Nat}
+    (P : MeasureTheory.Measure Omega) (X : I -> HighDimProb.RandomMatrix Omega m n)
+    (R Rexp : Real)
+    (hX : HighDimProb.PointwiseOperatorNormBound X R)
+    (hExp : forall i,
+      HighDimProb.deterministicOperatorNorm (HighDimProb.matrixExpect P (X i)) <= Rexp) :
+    HighDimProb.PointwiseOperatorNormBound
+      (fun i => HighDimProb.centeredRandomMatrix P (X i)) (R + Rexp) := by
+  exact HighDimProb.PointwiseOperatorNormBound_centered_of_bound_expect_bound
+    P X R Rexp hX hExp
diff --git a/HighDimProbTest/RandomMatrixAssumptionsAPI.lean b/HighDimProbTest/RandomMatrixAssumptionsAPI.lean
index d7f3646..7da526e 100644
--- a/HighDimProbTest/RandomMatrixAssumptionsAPI.lean
+++ b/HighDimProbTest/RandomMatrixAssumptionsAPI.lean
@@ -8,6 +8,7 @@ variable {P : Measure Omega} [IsProbabilityMeasure P]
 variable {I : Type*}
 variable {m n : Nat}
 variable (A : RandomMatrix Omega m n)
+variable (B : I -> RandomMatrix Omega m n)
 variable (X : I -> Omega -> Fin n -> Real)
 variable (K R : Real)
 
@@ -19,6 +20,9 @@ variable (K R : Real)
 #check CenteredEntries
 #check BoundedOperatorNorm_rankOne_of_sqNorm_bound
 #check PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+#check BoundedOperatorNorm_centered_of_bound_expect_bound
+#check PointwiseOperatorNormBound_centered_of_bound_expect_bound
+#check PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
 
 #check (SubGaussianEntriesOrlicz P A K : Prop)
 #check (SubGaussianEntriesTail P A K : Prop)
@@ -32,3 +36,18 @@ variable (K R : Real)
   (forall i omega, vectorSqNorm (X i omega) <= R) ->
   PointwiseOperatorNormBound
     (fun i omega a b => X i omega a * X i omega b) R)
+#check (BoundedOperatorNorm_centered_of_bound_expect_bound
+  (P := P) (X := A) (R := R) (Rexp := K) :
+  BoundedOperatorNorm A R ->
+  deterministicOperatorNorm (matrixExpect P A) <= K ->
+  BoundedOperatorNorm (centeredRandomMatrix P A) (R + K))
+#check (PointwiseOperatorNormBound_centered_of_bound_expect_bound
+  (P := P) (X := B) (R := R) (Rexp := K) :
+  PointwiseOperatorNormBound B R ->
+  (forall i, deterministicOperatorNorm (matrixExpect P (B i)) <= K) ->
+  PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (B i)) (R + K))
+#check (PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
+  (P := P) (X := B) (R := R) :
+  PointwiseOperatorNormBound B R ->
+  (forall i, deterministicOperatorNorm (matrixExpect P (B i)) <= R) ->
+  PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (B i)) (R + R))
diff --git a/HighDimProbTest/RandomMatrixConcentrationAPI.lean b/HighDimProbTest/RandomMatrixConcentrationAPI.lean
index d9ddb84..2a58a31 100644
--- a/HighDimProbTest/RandomMatrixConcentrationAPI.lean
+++ b/HighDimProbTest/RandomMatrixConcentrationAPI.lean
@@ -126,6 +126,16 @@ variable (R sigma2 c c1 c2 t bound K : Real)
 #check (PointwiseOperatorNormBound B R : Prop)
 #check (UniformOperatorNormBound B R : Prop)
 #check (AeOperatorNormBound P B R : Prop)
+#check (BoundedOperatorNorm_centered_of_bound_expect_bound
+  (P := P) (X := A) (R := R) (Rexp := c) :
+  BoundedOperatorNorm A R ->
+  deterministicOperatorNorm (matrixExpect P A) <= c ->
+  BoundedOperatorNorm (centeredRandomMatrix P A) (R + c))
+#check (PointwiseOperatorNormBound_centered_of_bound_expect_bound
+  (P := P) (X := B) (R := R) (Rexp := c) :
+  PointwiseOperatorNormBound B R ->
+  (forall i, deterministicOperatorNorm (matrixExpect P (B i)) <= c) ->
+  PointwiseOperatorNormBound (fun i => centeredRandomMatrix P (B i)) (R + c))
 #check (randomMatrixSum B : RandomMatrix Omega n n)
 #check (MatrixVarianceProxy P B : Matrix (Fin n) (Fin n) Real)
 #check (matrixVarianceProxy P B : Matrix (Fin n) (Fin n) Real)
diff --git a/HighDimProbTest/RandomMatrixOperatorNormAPI.lean b/HighDimProbTest/RandomMatrixOperatorNormAPI.lean
index 781f569..8df975d 100644
--- a/HighDimProbTest/RandomMatrixOperatorNormAPI.lean
+++ b/HighDimProbTest/RandomMatrixOperatorNormAPI.lean
@@ -34,6 +34,7 @@ variable (hA : IsRandomMatrix P A)
 #check instOpensMeasurableSpaceMatrixL2Operator
 #check deterministicOperatorNorm
 #check deterministicOperatorNorm_apply
+#check deterministicOperatorNorm_sub_le_add
 #check rankOneOperatorNorm_le_vectorSqNorm
 #check matVecSqNorm
 #check matVecSqNorm_apply
@@ -65,6 +66,8 @@ variable (hA : IsRandomMatrix P A)
 #check (IsUnitVector x : Prop)
 #check (unitSphere n : Set (Fin n -> Real))
 #check (deterministicOperatorNorm M : Real)
+#check (deterministicOperatorNorm_sub_le_add M M :
+  deterministicOperatorNorm (M - M) <= deterministicOperatorNorm M + deterministicOperatorNorm M)
 #check (rankOneOperatorNorm_le_vectorSqNorm v :
   deterministicOperatorNorm (fun i j : Fin n => v i * v j) <= vectorSqNorm v)
 #check (matVecSqNorm M x : Real)
diff --git a/docs/AbstractionLog.md b/docs/AbstractionLog.md
index a61c968..f13a098 100644
--- a/docs/AbstractionLog.md
+++ b/docs/AbstractionLog.md
@@ -1216,3 +1216,20 @@
 - Future upgrade path: next add the centered operator-norm triangle wrapper;
   then handle vector-to-rank-one measurability/integrability and PSD nullspace
   converse as separate concept clusters.
+
+## RM centered operator-norm boundedness bridge
+
+- Concrete version chosen: prove the deterministic triangle inequality for the
+  existing `deterministicOperatorNorm`, then package it for `centeredRandomMatrix`
+  using an explicit bound on `matrixExpect P X`.
+- Assumption decision: the wrappers require both the pointwise bound on `X` and
+  the deterministic operator-norm bound on `E X`; they do not infer expectation
+  contraction from boundedness.
+- Layering decision: this remains an algebraic boundedness bridge over the
+  current entrywise expectation vocabulary.  It deliberately does not prove
+  entrywise integrability or vector-to-rank-one measurability.
+- Review decision: independent code review approved the change; architectural
+  review flagged the risk that centered APIs can look analytically stronger than
+  they are, so Lean comments and docs now state the explicit-bound-only boundary.
+- Future upgrade path: next handle vector-to-rank-one matrix measurability /
+  integrability as a separate concept cluster, then PSD nullspace converse.
diff --git a/docs/BookProgress.md b/docs/BookProgress.md
index 3db8740..595ff75 100644
--- a/docs/BookProgress.md
+++ b/docs/BookProgress.md
@@ -993,4 +993,25 @@ squared-norm bounds into `BoundedOperatorNorm` and
 
 This is not a centered summand bound, not a vector-to-matrix
 measurability/integrability bridge, not a PSD nullspace converse, and not a
-Matrix Bernstein tail theorem. Next safe task: RM-centered-operator-norm-bound.
+Matrix Bernstein tail theorem. Next safe task: RM-vector-to-matrix-measurability-integrability.
+
+## RM centered operator-norm prerequisite progress
+
+The centered boundedness slice for covariance-style RandomMatrix examples is
+proved:
+
+```lean
+deterministicOperatorNorm_sub_le_add
+BoundedOperatorNorm_centered_of_bound_expect_bound
+PointwiseOperatorNormBound_centered_of_bound_expect_bound
+PointwiseOperatorNormBound_centered_of_bound_expect_bound_same
+```
+
+The deterministic lemma packages the matrix operator-norm triangle inequality
+`||A - B||op <= ||A||op + ||B||op`.  The random-matrix wrappers apply this to
+`centeredRandomMatrix P X` under an explicit bound on
+`deterministicOperatorNorm (matrixExpect P X)`.  This is not an expectation
+contraction theorem and does not prove entrywise integrability or
+vector-to-rank-one measurability.
+
+Next safe task: RM-vector-to-matrix-measurability-integrability.
diff --git a/docs/MatrixBernsteinProofPlan.md b/docs/MatrixBernsteinProofPlan.md
index 9514860..2c7c3d4 100644
--- a/docs/MatrixBernsteinProofPlan.md
+++ b/docs/MatrixBernsteinProofPlan.md
@@ -41,7 +41,13 @@ Tropp/Lieb, Golden-Thompson, the Bernstein CFC primitive, the `t = 0` endpoint
 for the optimized wrapper, lambda-max/operator-norm Matrix Bernstein tails, or
 the full Matrix Bernstein tail theorem.
 
-Next safe task: `RM-centered-operator-norm-bound`.
+Next safe task: `RM-vector-to-matrix-measurability-integrability`.
+
+RM prerequisite update: the centered operator-norm bridge is now proved via
+`deterministicOperatorNorm_sub_le_add` and the explicit-expectation-bound
+wrappers in `Assumptions.lean`.  It does not prove vector-to-matrix
+measurability/integrability, PSD nullspace converse, or expectation contraction.
+
 ## Target Theorem
 
 For a finite family of independent centered self-adjoint random matrices
diff --git a/docs/MatrixConcentrationPlan.md b/docs/MatrixConcentrationPlan.md
index d571a2e..9a9a2a8 100644
--- a/docs/MatrixConcentrationPlan.md
+++ b/docs/MatrixConcentrationPlan.md
@@ -22,7 +22,13 @@ compatibility APIs around the bounded-Bernstein lintegral Laplace route:
 `matrixBernsteinTraceMGFToLaplaceContract_statement` and
 `matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement`.
 
-Next safe task: `RM-centered-operator-norm-bound`.
+Next safe task: `RM-vector-to-matrix-measurability-integrability`.
+
+RM prerequisite update: the centered operator-norm bridge is now proved via
+`deterministicOperatorNorm_sub_le_add` and the explicit-expectation-bound
+wrappers in `Assumptions.lean`.  It does not prove vector-to-matrix
+measurability/integrability, PSD nullspace converse, or expectation contraction.
+
 Stage MC1 starts the matrix concentration branch after the scalar concentration
 closeout. It adds the assumption vocabulary, explicit matrix order vocabulary,
 matrix expectation wrappers, and typed theorem-statement layer needed before
diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md
index 5719546..d8f0c20 100644
--- a/docs/RandomMatrixAPI.md
+++ b/docs/RandomMatrixAPI.md
@@ -43,7 +43,13 @@ mainline. It is documentation only; theorem status is not upgraded here.
   `rankOneOperatorNorm_le_vectorSqNorm`,
   `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and
   `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`.
-- Next safe task: `RM-centered-operator-norm-bound`.
+- Proved centered operator-norm prerequisite bridge under an explicit expectation
+  operator-norm bound:
+  `deterministicOperatorNorm_sub_le_add`,
+  `BoundedOperatorNorm_centered_of_bound_expect_bound`,
+  `PointwiseOperatorNormBound_centered_of_bound_expect_bound`, and
+  `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same`.
+- Next safe task: `RM-vector-to-matrix-measurability-integrability`.
 
 ## `HighDimProb/RandomMatrix/SelfAdjoint.lean`
 
@@ -101,6 +107,7 @@ mainline. It is documentation only; theorem status is not upgraded here.
 - `deterministicOperatorNorm`: def, deterministic matrix operator norm using the
   same scoped L2 convention.
 - `deterministicOperatorNorm_apply`: theorem, definitional bridge.
+- `deterministicOperatorNorm_sub_le_add`: theorem, deterministic triangle bound.
 - `rankOneOperatorNorm_le_vectorSqNorm`: theorem, `||v vᵀ||op <= ||v||₂²`.
 - `matVecSqNorm`: def.
 - `randomMatVecSqNorm`: def.
@@ -115,9 +122,16 @@ mainline. It is documentation only; theorem status is not upgraded here.
   matrix.
 - `BoundedOperatorNorm_rankOne_of_sqNorm_bound`: theorem, rank-one pointwise
   wrapper from vector squared-norm bounds.
+- `BoundedOperatorNorm_centered_of_bound_expect_bound`: theorem, centered
+  wrapper from a pointwise bound plus an explicit expectation operator-norm
+  bound.
 - `PointwiseOperatorNormBound`: def, indexed pointwise operator-norm bound.
 - `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`: theorem, indexed
   rank-one wrapper from vector squared-norm bounds.
+- `PointwiseOperatorNormBound_centered_of_bound_expect_bound`: theorem, indexed
+  centered wrapper with explicit expectation bound.
+- `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same`: theorem,
+  same-radius centered wrapper.
 - `UniformOperatorNormBound`: abbrev.
 - `AeOperatorNormBound`: def.
 
@@ -386,10 +400,7 @@ mainline. It is documentation only; theorem status is not upgraded here.
 
 ## Next Safe Task
 
-RM-centered-operator-norm-bound: plan the bridge from the proved
-one-sided optimized quadratic-form under-primitives tail to lambda-max and then
-operator-norm Matrix Bernstein tails. Do not prove Tropp/Lieb, Bernstein CFC,
-Golden-Thompson, or the full Matrix Bernstein theorem in that contract stage.
+RM-vector-to-matrix-measurability-integrability: next prove or isolate the entrywise measurability / integrability bridge from vector random variables to rank-one random matrices. Do not prove PSD nullspace converse, lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, Bernstein CFC, Golden-Thompson, or the full Matrix Bernstein theorem in that stage.
 
 ## MB-S9 Matrix Bernstein Trace-MGF Under Primitives API
 
@@ -413,4 +424,4 @@ Golden-Thompson, or the full Matrix Bernstein theorem in that contract stage.
   proved in `ConcentrationStatements.lean`, with exponential-add RHS.
 - The theta-optimized scalar-RHS quadratic-form wrapper under primitives is now
   proved in `ConcentrationStatements.lean`, with Bernstein denominator RHS.
-- Next safe task: RM-centered-operator-norm-bound.
+- Next safe task: RM-vector-to-matrix-measurability-integrability.
diff --git a/docs/Status.md b/docs/Status.md
index 1a036eb..d313951 100644
--- a/docs/Status.md
+++ b/docs/Status.md
@@ -8,17 +8,22 @@ RandomMatrix / Matrix Bernstein mainline: MB-S9 now includes the bounded
 trace-MGF theorem under explicit primitives, the bounded real-to-lintegral
 trace-MGF bridge, the explicit-theta quadratic-form upper-tail wrappers, the
 dimension/norm scalar RHS reduction, and the theta-optimized scalar Bernstein
-denominator wrapper. The current prerequisite cleanup also adds the first
-rank-one operator-norm bridge for covariance-style examples.
+denominator wrapper. The current prerequisite cleanup also adds rank-one and
+centered operator-norm bridges for covariance-style examples.
 
 The latest proved public theorem is:
 
-- `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`
-
-Supporting proved API also includes `rankOneOperatorNorm_le_vectorSqNorm` and
-`BoundedOperatorNorm_rankOne_of_sqNorm_bound`. These are deterministic /
-pointwise boundedness bridges only: they do not prove centered summand
-boundedness, vector-to-rank-one matrix measurability or integrability, the PSD
+- `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same`
+
+Supporting proved API also includes `deterministicOperatorNorm_sub_le_add`,
+`BoundedOperatorNorm_centered_of_bound_expect_bound`,
+`PointwiseOperatorNormBound_centered_of_bound_expect_bound`, the earlier
+rank-one bridge `rankOneOperatorNorm_le_vectorSqNorm`,
+`BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and
+`PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`. These are deterministic /
+pointwise boundedness bridges only: the centered bridge requires an explicit
+operator-norm bound on `matrixExpect P X` and does not prove expectation
+contraction, vector-to-rank-one matrix measurability or integrability, the PSD
 nullspace converse, lambda-max/operator-norm Matrix Bernstein tails,
 Tropp/Lieb, the Bernstein CFC primitive, Golden-Thompson, the `t = 0` endpoint
 for the optimized wrapper, or the final full Matrix Bernstein tail theorem.
@@ -28,7 +33,7 @@ under explicit primitive assumptions.
 
 ## Next Safe Task
 
-- `RM-centered-operator-norm-bound`
+- `RM-vector-to-matrix-measurability-integrability`
 
 ## Public Milestone Summary
 
diff --git a/docs/TODO.md b/docs/TODO.md
index d86a76f..2d94895 100644
--- a/docs/TODO.md
+++ b/docs/TODO.md
@@ -16,15 +16,20 @@
   `rankOneOperatorNorm_le_vectorSqNorm`,
   `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and
   `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`.
+- Done: centered operator-norm prerequisite slice added
+  `deterministicOperatorNorm_sub_le_add`,
+  `BoundedOperatorNorm_centered_of_bound_expect_bound`,
+  `PointwiseOperatorNormBound_centered_of_bound_expect_bound`, and
+  `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same`.
 - The optimized theorem remains one-sided, quadratic-form, and under explicit
   `troppMasterTraceMGFFiniteFamily_statement` plus pointwise
   `bernsteinMatrixExp_le_quadratic_statement` assumptions.
-- Not proved: centered summand operator-norm bound, vector-to-rank-one matrix
-  measurability/integrability, PSD nullspace converse, lambda-max/operator-norm
+- Not proved: vector-to-rank-one matrix measurability/integrability,
+  PSD nullspace converse, lambda-max/operator-norm
   tail bridge, optimized `t = 0` endpoint, functional-calculus proof /
   Bernstein CFC primitive, full CFC-free single-summand MGF theorem, Lieb
   concavity, Golden-Thompson, and the full Matrix Bernstein tail theorem.
-- Next: RM-centered-operator-norm-bound.
+- Next: RM-vector-to-matrix-measurability-integrability.
 ## Stage M3 Scalar Closeout TODO Audit
 
 The forward scalar subGaussian proof spine is closed as an experimental
@@ -199,8 +204,8 @@ Stage H0 Rademacher/Hoeffding branch update:
 | Concrete trace-exp dominance assembly | Use the `lambdaMaxOrdered` spectral and trace-exp providers to prove `TraceExpDominatesQuadraticFormUpperTail` for random self-adjoint matrices. | `lambdaMaxOrdered_rayleighUpperBound`, `lambdaMaxOrdered_traceExpDominatesUpperBound`, `traceExpDominatesQuadraticFormUpperTail_of_rayleighUpperBound_of_traceExpDominatesUpperBound`, `RandomSelfAdjointMatrix` | done | Implemented in MB-S7C-assemble-dominance as `traceExpDominatesQuadraticFormUpperTail_of_randomSelfAdjoint`. This did not prove full matrix Laplace, trace-mgf, Golden-Thompson, Lieb, or Matrix Bernstein. |
 | Conditional matrix Laplace assembly | Use concrete random self-adjoint dominance with the existing conditional Laplace wrappers to prove the matrix Laplace upper-tail theorem. | `traceExpDominatesQuadraticFormUpperTail_of_randomSelfAdjoint`, `matrixLaplaceTransformLIntegral_of_traceExpDominatesQuadraticFormUpperTail`, explicit measurability/integrability hypotheses | done | Implemented in MB-S8-laplace-assembly as `matrixLaplaceTransformLIntegralDiv_of_randomSelfAdjoint` and `matrixLaplaceTransformLIntegral_of_randomSelfAdjoint`. This did not prove the real RHS bridge, trace-mgf, Golden-Thompson, Lieb, or Matrix Bernstein. |
 | Matrix Laplace real RHS bridge | Connect the lintegral matrix Laplace theorem to the existing real trace-exp moment/RHS vocabulary. | `matrixLaplaceTransformLIntegral_of_randomSelfAdjoint`, `traceExpMomentLIntegral_eq_ofReal_traceExpMoment`, explicit integrability and nonnegativity hypotheses | hard | Future task after the current trace-mgf provider contract decision; do not prove trace-mgf, Golden-Thompson, Lieb, or Matrix Bernstein in that bridge stage. |
-| Matrix trace-mgf foundation/provider contract | Audit the route for proving the semantic bounded Matrix Bernstein trace-mgf target. | `TraceMGFBound`, `TraceMGFBernsteinVarianceProxyBound`, `matrixBernsteinTraceMGFWithBernsteinCoeff_statement`, matrix-valued independence, variance proxy, Golden-Thompson/Lieb or equivalent matrix-mgf machinery | hard | MB-S9-foundation added only semantic predicates and typed targets; MB-S9 follow-up stages isolated and resolved expectation, MatrixLE algebra, coefficient, lower-bound, provider-under-CFC, and RHS-normalization blockers while leaving Tropp/Lieb and Bernstein CFC primitives typed only. `matrixBernsteinTraceMGF_statement` remains a `theta ^ 2 / 2` compatibility target, not the bounded Bernstein denominator target. Current next safe task: RM-centered-operator-norm-bound. |
-| Matrix exponential lower bound for Bernstein coefficient | Audit/prove the deterministic bridge `MatrixLE (1 + c smul V) (matrixExp (c smul V))` after `bernsteinCoefficient_nonneg`. | `bernsteinCoefficient_nonneg`, `MatrixLE`, `matrixExp`, PSD/self-adjoint variance proxy hypotheses, CFC or spectral exponential lower APIs | done | MB-S9-exp-lower-bound-proof implements this deterministic lower-bound family as `matrixLE_one_add_self_le_matrixExp_of_selfAdjoint` and `matrixLE_one_add_smul_le_matrixExp_smul_of_selfAdjoint`. MB-S9-single-summand-provider-under-cfc then uses it in `singleSummandMatrixMGFVarianceProxy_of_bernsteinMatrixExp_le_quadratic`. MB-S9-rhs-normalization-proof names the denominator coefficient as `bernsteinMGFCoeff` and adds bounded trace-mgf targets. The Bernstein CFC proof, trace-mgf provider, Golden-Thompson, Lieb, and Matrix Bernstein remain unproved. Next safe task: RM-centered-operator-norm-bound. |
+| Matrix trace-mgf foundation/provider contract | Audit the route for proving the semantic bounded Matrix Bernstein trace-mgf target. | `TraceMGFBound`, `TraceMGFBernsteinVarianceProxyBound`, `matrixBernsteinTraceMGFWithBernsteinCoeff_statement`, matrix-valued independence, variance proxy, Golden-Thompson/Lieb or equivalent matrix-mgf machinery | hard | MB-S9-foundation added only semantic predicates and typed targets; MB-S9 follow-up stages isolated and resolved expectation, MatrixLE algebra, coefficient, lower-bound, provider-under-CFC, and RHS-normalization blockers while leaving Tropp/Lieb and Bernstein CFC primitives typed only. `matrixBernsteinTraceMGF_statement` remains a `theta ^ 2 / 2` compatibility target, not the bounded Bernstein denominator target. Current next safe task: RM-vector-to-matrix-measurability-integrability. |
+| Matrix exponential lower bound for Bernstein coefficient | Audit/prove the deterministic bridge `MatrixLE (1 + c smul V) (matrixExp (c smul V))` after `bernsteinCoefficient_nonneg`. | `bernsteinCoefficient_nonneg`, `MatrixLE`, `matrixExp`, PSD/self-adjoint variance proxy hypotheses, CFC or spectral exponential lower APIs | done | MB-S9-exp-lower-bound-proof implements this deterministic lower-bound family as `matrixLE_one_add_self_le_matrixExp_of_selfAdjoint` and `matrixLE_one_add_smul_le_matrixExp_smul_of_selfAdjoint`. MB-S9-single-summand-provider-under-cfc then uses it in `singleSummandMatrixMGFVarianceProxy_of_bernsteinMatrixExp_le_quadratic`. MB-S9-rhs-normalization-proof names the denominator coefficient as `bernsteinMGFCoeff` and adds bounded trace-mgf targets. The Bernstein CFC proof, trace-mgf provider, Golden-Thompson, Lieb, and Matrix Bernstein remain unproved. Next safe task: RM-vector-to-matrix-measurability-integrability. |
 ## MB-S9 Tropp Shape Refactor Follow-Up
 
 The trace-exp layer now exposes `troppMasterTraceMGFFiniteFamily_statement`,
@@ -215,7 +220,7 @@ safe task: MB-S9-trace-mgf-to-laplace-tail-contract.
 - Still unproved: the finite-family Tropp/Lieb primitive itself.
 - Still unproved: the Bernstein CFC primitive.
 - Still unproved: Lieb, Golden-Thompson, and the Matrix Bernstein tail theorem.
-- Next safe task: RM-centered-operator-norm-bound.
+- Next safe task: RM-vector-to-matrix-measurability-integrability.
 
 ## MB-S9 Matrix Bernstein Trace-MGF Under Primitives Follow-Up
 
@@ -224,4 +229,4 @@ safe task: MB-S9-trace-mgf-to-laplace-tail-contract.
   and pointwise `bernsteinMatrixExp_le_quadratic_statement`.
 - Still unproved: finite-family Tropp/Lieb primitive, Bernstein CFC primitive,
   Lieb, Golden-Thompson, and Matrix Bernstein tail theorem.
-- Next safe task: RM-centered-operator-norm-bound.
+- Next safe task: RM-vector-to-matrix-measurability-integrability.
diff --git a/docs/TermMap.md b/docs/TermMap.md
index d418ab5..bd0d93e 100644
--- a/docs/TermMap.md
+++ b/docs/TermMap.md
@@ -132,6 +132,7 @@ Note: some declarations exist as scaffolds, but the corresponding concept is not
 | Exact operator-norm bridge targets | Matrix concentration prerequisites | Typed targets and proved bridges connecting explicit squared unit-vector bounds to Mathlib's scoped L2 matrix norm and measurability. | `Matrix.Norms.L2Operator`, product measurable spaces, `measurable_norm` | `operatorNorm_le_of_operatorNormBoundSqStatement`, `operatorNormBoundSq_of_operatorNorm_leStatement`, `operatorNormMeasurabilityStatement`, `operatorNorm_le_of_operatorNormBoundSq`, `operatorNormBoundSq_of_operatorNorm_le`, `instOpensMeasurableSpaceMatrixL2Operator`, `isRealRandomVariable_operatorNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | proven bridge plus typed-prop compatibility targets | Stage MC2-fix proves the exact comparison directions and operator-norm measurability; the statement-only targets remain as API signposts. |
 | Rank-one operator-norm bound | Rank-one covariance and matrix-concentration prerequisites | The self-outer product `v vᵀ` has induced L2 operator norm bounded by `||v||₂²`. | `Matrix.Norms.L2Operator`, `ContinuousLinearMap.opNorm_le_bound`, Cauchy-Schwarz | `rankOneOperatorNorm_le_vectorSqNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | proven experimental API | The proof uses the existing `deterministicOperatorNorm` convention and does not introduce new rank-one vocabulary. |
 | Rank-one pointwise operator-norm bound | Matrix Bernstein boundedness prerequisites | A pointwise squared-vector-norm bound implies a pointwise operator-norm bound for `omega |-> X omega X omegaᵀ` and indexed families. | `operatorNorm`, `vectorSqNorm`, `PointwiseOperatorNormBound` | `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound` | `HighDimProb/RandomMatrix/Assumptions.lean` | proven experimental API | This is a boundedness bridge only; centered expectation bounds, measurability/integrability bridges, and PSD nullspace converse remain separate tasks. |
+| Centered operator-norm bound | Matrix Bernstein boundedness prerequisites | Centering satisfies `||X(ω) - E X||op <= ||X(ω)||op + ||E X||op`; a pointwise bound plus explicit expectation bound yields a bound on `centeredRandomMatrix`. | `norm_sub_le`, `matrixExpect`, `centeredRandomMatrix`, `PointwiseOperatorNormBound` | `deterministicOperatorNorm_sub_le_add`, `BoundedOperatorNorm_centered_of_bound_expect_bound`, `PointwiseOperatorNormBound_centered_of_bound_expect_bound`, `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same` | `HighDimProb/RandomMatrix/OperatorNorm.lean`, `HighDimProb/RandomMatrix/Assumptions.lean` | proven experimental API | Algebraic explicit-bound wrapper only; it does not prove entrywise integrability, vector-to-rank-one measurability, or expectation operator-norm contraction. |
 | Matrix symmetry/self-adjointness | Matrix Bernstein prerequisites | Pointwise real symmetric/self-adjoint matrix predicates and random-matrix wrappers. | `Matrix.IsSymm`, `Matrix.IsHermitian` | `IsSymmetricMatrix`, `IsSelfAdjointMatrix`, `RandomSymmetricMatrix`, `RandomSelfAdjointMatrix` | `HighDimProb/RandomMatrix/SelfAdjoint.lean` | implemented experimental API | Stage MC1 keeps the vocabulary explicit and does not prove spectral theorems. |
 | PSD and Loewner-style order | Matrix Bernstein and covariance prerequisites | PSD means symmetric plus nonnegative quadratic forms; `MatrixLE A B` means `B - A` is PSD. | finite sums, explicit quadratic forms | `matrixQuadraticForm`, `IsPSDMatrix`, `RandomPSDMatrix`, `MatrixLE`, `quadraticForm_le_of_matrixLE` | `HighDimProb/RandomMatrix/MatrixOrder.lean` | implemented/proven experimental API | No global matrix order instance is installed. Stage MC2 proves the quadratic-form monotonicity bridge for the explicit Loewner-style order. |
 | MatrixLE / PSD algebra | Matrix Bernstein single-summand MGF route | Small algebra for explicit PSD and Loewner-style order: addition, nonnegative scalar multiplication, reflexivity, equality, transitivity, and add/smul monotonicity. | explicit quadratic forms, matrix add/sub/smul | `matrixQuadraticForm_add`, `matrixQuadraticForm_smul`, `isPSDMatrix_zero`, `isPSDMatrix_add`, `isPSDMatrix_smul_of_nonneg`, `matrixLE_refl`, `matrixLE_of_eq`, `matrixLE_trans`, `matrixLE_add`, `matrixLE_add_left`, `matrixLE_add_right`, `matrixLE_smul_of_nonneg` | `HighDimProb/RandomMatrix/MatrixOrder.lean` | proven experimental API | MB-S9-matrixle-algebra-proof closes the MatrixLE algebra/RHS-normalization blocker; the Bernstein CFC proof, single-summand MGF provider, trace-mgf provider, and Matrix Bernstein remain unproved. |
diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md
index ffdcb8d..d24521f 100644
--- a/docs/TheoremAtlas.md
+++ b/docs/TheoremAtlas.md
@@ -30,7 +30,7 @@ statement APIs connecting bounded Bernstein lintegral trace-MGF bounds to the
 existing Laplace/tail layer without claiming the missing real-to-lintegral,
 Tropp/Lieb, CFC, or Matrix Bernstein proofs.
 
-Next safe task: `RM-centered-operator-norm-bound`.
+Next safe task: `RM-vector-to-matrix-measurability-integrability`.
 ## Milestone 3 scalar implication closeout
 
 This audit separates proved theorem families from typed statements and blocked
@@ -1247,7 +1247,7 @@ future directions.
   `HighDimProbTest/RandomMatrixLaplaceAPI.lean`, and
   `HighDimProbTest/RandomMatrixConcentrationAPI.lean`.
 - Priority: Stage MB-S2 through MB-S9-foundation complete; next task is
-  RM-centered-operator-norm-bound.
+  RM-vector-to-matrix-measurability-integrability.
 
 ## Trace-Exponential Positivity Bridge (MB-S3/MB-S4)
 
@@ -1645,7 +1645,7 @@ future directions.
   `HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean`,
   `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`, and
   `HighDimProbJudge/RandomMatrix/StatementUse.lean`.
-- Priority: next safe task is RM-centered-operator-norm-bound.
+- Priority: next safe task is RM-vector-to-matrix-measurability-integrability.
 
 ## PSD of Matrix Square / Second Moment / Variance Proxy (MB-S1)
 
@@ -1821,7 +1821,7 @@ future directions.
 - Target module: `HighDimProb/RandomMatrix/TraceExp.lean`
 - Test module: `HighDimProbTest/RandomMatrixTraceExpAPI.lean`
 - Judge module: `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`
-- Priority: next safe task is RM-centered-operator-norm-bound.
+- Priority: next safe task is RM-vector-to-matrix-measurability-integrability.
 
 ## Matrix Exponential Lower Bound (MB-S9-exp-lower-bound-proof)
 
@@ -1948,7 +1948,7 @@ future directions.
 - Blocker: the finite-family Tropp primitive itself remains typed only; the
   Bernstein CFC primitive remains typed only; Lieb, Golden-Thompson, and the
   Matrix Bernstein tail theorem remain unproved.
-- Priority: next safe task is RM-centered-operator-norm-bound.
+- Priority: next safe task is RM-vector-to-matrix-measurability-integrability.
 
 
 
@@ -1966,7 +1966,7 @@ future directions.
 - Blocker: the result is still one-sided and quadratic-form under explicit
   Tropp/Lieb and Bernstein CFC primitives; lambda-max/operator-norm tail
   bridges and the full Matrix Bernstein theorem remain unproved.
-- Priority: next safe task is RM-centered-operator-norm-bound.
+- Priority: next safe task is RM-vector-to-matrix-measurability-integrability.
 
 ## Matrix Bernstein Trace-MGF to Laplace/Tail Contract (MB-S9)
 
@@ -1986,4 +1986,21 @@ future directions.
 - Blocker: prove or sharpen the real trace-MGF to lintegral bridge; keep the
   event-subset, Tropp/Lieb, Bernstein CFC, Golden-Thompson, and Matrix
   Bernstein tail theorem gaps explicit.
-- Priority: next safe task is RM-centered-operator-norm-bound.
+- Priority: next safe task is RM-vector-to-matrix-measurability-integrability.
+
+## RM Centered Operator-Norm Bound
+
+- Informal statement: if a random matrix family has pointwise operator-norm
+  bound `R` and each entrywise expectation matrix has deterministic
+  operator-norm bound `Rexp`, then the centered family is pointwise bounded by
+  `R + Rexp`.
+- Target Lean declarations:
+  `deterministicOperatorNorm_sub_le_add`,
+  `BoundedOperatorNorm_centered_of_bound_expect_bound`,
+  `PointwiseOperatorNormBound_centered_of_bound_expect_bound`, and
+  `PointwiseOperatorNormBound_centered_of_bound_expect_bound_same`.
+- Status: proven, API-tested, and judge-tested.
+- Blocker: this is only an algebraic explicit-bound wrapper.  It does not prove
+  vector-to-rank-one matrix measurability/integrability, expectation
+  contraction, PSD nullspace converse, or Matrix Bernstein tails.
+- Priority: next safe task is RM-vector-to-matrix-measurability-integrability.