diff --git a/HighDimProb/RandomMatrix/Assumptions.lean b/HighDimProb/RandomMatrix/Assumptions.lean
index ef9e815..00c35ef 100644
--- a/HighDimProb/RandomMatrix/Assumptions.lean
+++ b/HighDimProb/RandomMatrix/Assumptions.lean
@@ -92,12 +92,49 @@ def BoundedOperatorNorm {Omega : Type*} [MeasurableSpace Omega] {m n : Nat}
     (A : RandomMatrix Omega m n) (R : Real) : Prop :=
   forall omega, operatorNorm A omega <= R
 
+/--
+A pointwise squared-vector-norm bound gives an operator-norm bound for the
+rank-one random matrix `omega |-> X(omega) X(omega)^T`.
+
+Formula reference: the deterministic ingredient is
+`||v v^T||op <= ||v||_2^2` for a rank-one outer product; see
+https://en.wikipedia.org/wiki/Outer_product and
+https://en.wikipedia.org/wiki/Operator_norm
+-/
+theorem BoundedOperatorNorm_rankOne_of_sqNorm_bound {Omega : Type*}
+    [MeasurableSpace Omega] {n : Nat}
+    (X : Omega -> Fin n -> Real) (R : Real)
+    (_hR : 0 <= R)
+    (hX : forall omega, vectorSqNorm (X omega) <= R) :
+    BoundedOperatorNorm (fun omega i j => X omega i * X omega j) R := by
+  intro omega
+  exact (rankOneOperatorNorm_le_vectorSqNorm (X omega)).trans (hX omega)
+
 /-- 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)
     (R : Real) : Prop :=
   forall i, BoundedOperatorNorm (A i) R
 
+/--
+Family version of the rank-one operator-norm bridge: if every vector sample has
+`vectorSqNorm <= R`, then the associated rank-one matrix family is pointwise
+operator-norm bounded by `R`.
+
+Formula reference: this packages the outer-product bound
+`||v v^T||op <= ||v||_2^2`; see
+https://en.wikipedia.org/wiki/Outer_product and
+https://en.wikipedia.org/wiki/Operator_norm
+-/
+theorem PointwiseOperatorNormBound_rankOne_of_sqNorm_bound {Omega : Type*}
+    [MeasurableSpace Omega] {I : Type*} {n : Nat}
+    (X : I -> Omega -> Fin n -> Real) (R : Real)
+    (hR : 0 <= R)
+    (hX : forall i omega, vectorSqNorm (X i omega) <= R) :
+    PointwiseOperatorNormBound (fun i omega a b => X i omega a * X i omega b) R := by
+  intro i
+  exact BoundedOperatorNorm_rankOne_of_sqNorm_bound (X i) R hR (hX i)
+
 /-- 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 9f92619..b2ac24a 100644
--- a/HighDimProb/RandomMatrix/OperatorNorm.lean
+++ b/HighDimProb/RandomMatrix/OperatorNorm.lean
@@ -82,6 +82,48 @@ theorem deterministicOperatorNorm_apply {m n : Nat}
     deterministicOperatorNorm A = norm A :=
   rfl
 
+/--
+Rank-one self-outer products have operator norm bounded by the squared
+Euclidean norm of the vector.
+
+Formula reference: for the outer product `v vᵀ`, multiplication sends
+`x` to `<v, x> v`; Cauchy--Schwarz gives
+`||<v, x> v||₂ <= ||v||₂^2 ||x||₂`, hence the induced operator-norm bound.
+See https://en.wikipedia.org/wiki/Outer_product and
+https://en.wikipedia.org/wiki/Operator_norm
+-/
+theorem rankOneOperatorNorm_le_vectorSqNorm {n : Nat}
+    (v : Fin n -> Real) :
+    deterministicOperatorNorm (fun i j : Fin n => v i * v j) <= vectorSqNorm v := by
+  rw [deterministicOperatorNorm, Matrix.l2_opNorm_def]
+  refine ContinuousLinearMap.opNorm_le_bound _ (vectorSqNorm_nonneg v) ?_
+  intro y
+  have happly :
+      (((Matrix.toEuclideanLin (𝕜 := Real) (m := Fin n) (n := Fin n)).trans
+            LinearMap.toContinuousLinearMap)
+          (fun i j : Fin n => v i * v j) y) =
+        (inner Real (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) y) •
+          (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) := by
+    ext i
+    simp [Matrix.toLpLin_apply, Matrix.mulVec, dotProduct, inner]
+    rw [Finset.sum_mul]
+    apply Finset.sum_congr rfl
+    intro j _
+    ring
+  rw [happly]
+  calc
+    ‖(inner Real (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) y) •
+          (WithLp.toLp 2 v : EuclideanSpace Real (Fin n))‖
+        = |inner Real (WithLp.toLp 2 v : EuclideanSpace Real (Fin n)) y| *
+            ‖(WithLp.toLp 2 v : EuclideanSpace Real (Fin n))‖ := by
+          rw [norm_smul, Real.norm_eq_abs]
+    _ <= ‖(WithLp.toLp 2 v : EuclideanSpace Real (Fin n))‖ * ‖y‖ *
+            ‖(WithLp.toLp 2 v : EuclideanSpace Real (Fin n))‖ := by
+          exact mul_le_mul_of_nonneg_right (abs_real_inner_le_norm _ _) (norm_nonneg _)
+    _ = vectorSqNorm v * ‖y‖ := by
+          rw [vectorSqNorm_eq_norm_sq_toLp]
+          ring
+
 /--
 Squared Euclidean norm of the deterministic matrix-vector product.
 
diff --git a/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean b/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean
index 5f64b42..15cae12 100644
--- a/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean
+++ b/HighDimProbJudge/RandomMatrix/OperatorNormUse.lean
@@ -1,6 +1,9 @@
 import HighDimProb.RandomMatrix
 
 #check HighDimProb.isRealRandomVariable_operatorNorm
+#check HighDimProb.rankOneOperatorNorm_le_vectorSqNorm
+#check HighDimProb.BoundedOperatorNorm_rankOne_of_sqNorm_bound
+#check HighDimProb.PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
 
 #check
   (HighDimProb.isRealRandomVariable_operatorNorm :
@@ -16,3 +19,16 @@ example {Omega : Type*} [MeasurableSpace Omega]
     (hA : HighDimProb.IsRandomMatrix P A) :
     HighDimProb.IsRealRandomVariable P (HighDimProb.operatorNorm A) := by
   exact HighDimProb.isRealRandomVariable_operatorNorm hA
+
+example {n : Nat} (v : Fin n -> Real) :
+    HighDimProb.deterministicOperatorNorm
+      (fun i j : Fin n => v i * v j) <= HighDimProb.vectorSqNorm v := by
+  exact HighDimProb.rankOneOperatorNorm_le_vectorSqNorm v
+
+example {Omega : Type*} [MeasurableSpace Omega] {I : Type*} {n : Nat}
+    (X : I -> Omega -> Fin n -> Real) (R : Real)
+    (hR : 0 <= R)
+    (hX : forall i omega, HighDimProb.vectorSqNorm (X i omega) <= R) :
+    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
diff --git a/HighDimProbTest/ExamplesAPI.lean b/HighDimProbTest/ExamplesAPI.lean
index 07bb022..e16238b 100644
--- a/HighDimProbTest/ExamplesAPI.lean
+++ b/HighDimProbTest/ExamplesAPI.lean
@@ -13,3 +13,12 @@ import HighDimProb.Examples.RandomMatrix.NTKGramDecompositionUsage
 import HighDimProb.Examples.RandomMatrix.NTKGramUsage
 import HighDimProb.Examples.RandomMatrix.RandomFeatureKernelUsage
 import HighDimProb.Examples.RandomMatrix.RankOnePSDUsage
+
+open HighDimProb
+open HighDimProb.Examples.RandomMatrix.RankOnePSDUsage
+
+variable {rankOneN : Nat}
+variable (rankOneV : RankOneVector rankOneN)
+
+#check (rankOneOperatorNorm_le_vectorSqNorm rankOneV :
+  deterministicOperatorNorm (rankOneOuter rankOneV) <= vectorSqNorm rankOneV)
diff --git a/HighDimProbTest/RandomMatrixAssumptionsAPI.lean b/HighDimProbTest/RandomMatrixAssumptionsAPI.lean
index 9bc77ae..d7f3646 100644
--- a/HighDimProbTest/RandomMatrixAssumptionsAPI.lean
+++ b/HighDimProbTest/RandomMatrixAssumptionsAPI.lean
@@ -5,9 +5,11 @@ open HighDimProb
 
 variable {Omega : Type*} [MeasurableSpace Omega]
 variable {P : Measure Omega} [IsProbabilityMeasure P]
+variable {I : Type*}
 variable {m n : Nat}
 variable (A : RandomMatrix Omega m n)
-variable (K : Real)
+variable (X : I -> Omega -> Fin n -> Real)
+variable (K R : Real)
 
 #check SubGaussianEntriesOrlicz
 #check SubGaussianEntriesTail
@@ -15,6 +17,8 @@ variable (K : Real)
 #check IsotropicRowsSecondMoment
 #check IsotropicRowsCovariance
 #check CenteredEntries
+#check BoundedOperatorNorm_rankOne_of_sqNorm_bound
+#check PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
 
 #check (SubGaussianEntriesOrlicz P A K : Prop)
 #check (SubGaussianEntriesTail P A K : Prop)
@@ -22,3 +26,9 @@ variable (K : Real)
 #check (IsotropicRowsSecondMoment P A : Prop)
 #check (IsotropicRowsCovariance P A : Prop)
 #check (CenteredEntries P A : Prop)
+#check (PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+  (X := X) (R := R) :
+  0 <= R ->
+  (forall i omega, vectorSqNorm (X i omega) <= R) ->
+  PointwiseOperatorNormBound
+    (fun i omega a b => X i omega a * X i omega b) R)
diff --git a/HighDimProbTest/RandomMatrixOperatorNormAPI.lean b/HighDimProbTest/RandomMatrixOperatorNormAPI.lean
index a159924..781f569 100644
--- a/HighDimProbTest/RandomMatrixOperatorNormAPI.lean
+++ b/HighDimProbTest/RandomMatrixOperatorNormAPI.lean
@@ -5,12 +5,15 @@ open HighDimProb
 
 variable {Omega : Type*} [MeasurableSpace Omega]
 variable {P : Measure Omega} [IsProbabilityMeasure P]
+variable {I : Type*}
 variable {m n : Nat}
 variable (A : RandomMatrix Omega m n)
 variable (B C : RandomMatrix Omega n n)
 variable (M : Matrix (Fin m) (Fin n) Real)
 variable (S T : Matrix (Fin n) (Fin n) Real)
 variable (x : Fin n -> Real)
+variable (v : Fin n -> Real)
+variable (X : I -> Omega -> Fin n -> Real)
 variable (L t bound : Real)
 variable (hA : IsRandomMatrix P A)
 
@@ -31,6 +34,7 @@ variable (hA : IsRandomMatrix P A)
 #check instOpensMeasurableSpaceMatrixL2Operator
 #check deterministicOperatorNorm
 #check deterministicOperatorNorm_apply
+#check rankOneOperatorNorm_le_vectorSqNorm
 #check matVecSqNorm
 #check matVecSqNorm_apply
 #check matVecSqNorm_nonneg
@@ -61,6 +65,8 @@ variable (hA : IsRandomMatrix P A)
 #check (IsUnitVector x : Prop)
 #check (unitSphere n : Set (Fin n -> Real))
 #check (deterministicOperatorNorm M : Real)
+#check (rankOneOperatorNorm_le_vectorSqNorm v :
+  deterministicOperatorNorm (fun i j : Fin n => v i * v j) <= vectorSqNorm v)
 #check (matVecSqNorm M x : Real)
 #check (randomMatVecSqNorm A x : RealRandomVariable Omega)
 #check (sqNorm_matVec_eq_matVecSqNorm A x : forall omega, sqNorm (matVec A x) omega = matVecSqNorm (A omega) x)
@@ -77,6 +83,12 @@ variable (hA : IsRandomMatrix P A)
 #check (operatorNorm_le_of_operatorNormBoundSqStatement M L : Prop)
 #check (operatorNormBoundSq_of_operatorNorm_leStatement M L : Prop)
 #check (operatorNormMeasurabilityStatement P A : Prop)
+#check (PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+  (X := X) (R := L) :
+  0 <= L ->
+  (forall i omega, vectorSqNorm (X i omega) <= L) ->
+  PointwiseOperatorNormBound
+    (fun i omega a b => X i omega a * X i omega b) L)
 #check (matrixQuadraticForm_sub T S x :
   matrixQuadraticForm (T - S) x = matrixQuadraticForm T x - matrixQuadraticForm S x)
 #check (quadraticForm_le_of_matrixLE (A := S) (B := T) : MatrixLE S T -> forall x, matrixQuadraticForm S x <= matrixQuadraticForm T x)
diff --git a/docs/AbstractionLog.md b/docs/AbstractionLog.md
index 008cd87..a61c968 100644
--- a/docs/AbstractionLog.md
+++ b/docs/AbstractionLog.md
@@ -1199,3 +1199,20 @@
 - Remaining upgrade path: prove matrix Laplace / trace-mgf inequalities and
   spectral/operator-norm tail reductions using this trace-exp positivity
   bridge as infrastructure.
+
+## RM rank-one operator-norm boundedness bridge
+
+- Concrete version chosen: prove the rank-one self-outer-product bound directly
+  against `deterministicOperatorNorm` instead of introducing a new rank-one
+  matrix object or changing the matrix norm convention.
+- Proof-pattern decision: view `v vᵀ` as the linear map `x ↦ <v, x> v` and use
+  Cauchy--Schwarz plus `ContinuousLinearMap.opNorm_le_bound` under Mathlib's
+  scoped L2 operator norm.
+- Assumption decision: the random wrappers consume an explicit pointwise
+  `vectorSqNorm <= R` hypothesis and keep the nonnegative-radius argument
+  visible, rather than inferring expectation or centered bounds.
+- Comment/source decision: Lean comments include public operator-norm and outer
+  product URLs so readers can verify the mathematical formula.
+- 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.
diff --git a/docs/BookProgress.md b/docs/BookProgress.md
index 108c10d..3db8740 100644
--- a/docs/BookProgress.md
+++ b/docs/BookProgress.md
@@ -973,3 +973,24 @@ finite-family Tropp typed primitive into the high-level bounded trace-MGF
 statement. The finite-family Tropp primitive, Bernstein CFC primitive, Lieb,
 Golden-Thompson, and Matrix Bernstein tail theorem remain unproved.
 Next safe task: MB-S9-trace-mgf-to-laplace-tail-contract.
+
+## RM rank-one operator-norm prerequisite progress
+
+The first rank-one prerequisite slice for covariance-style RandomMatrix examples
+is proved:
+
+```lean
+rankOneOperatorNorm_le_vectorSqNorm
+BoundedOperatorNorm_rankOne_of_sqNorm_bound
+PointwiseOperatorNormBound_rankOne_of_sqNorm_bound
+```
+
+The deterministic lemma proves the finite-dimensional bound
+`||v vᵀ||op <= ||v||₂²` using the existing `deterministicOperatorNorm` /
+Mathlib L2 operator-norm convention. The wrappers turn pointwise vector
+squared-norm bounds into `BoundedOperatorNorm` and
+`PointwiseOperatorNormBound` for rank-one random matrices.
+
+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.
diff --git a/docs/MatrixBernsteinProofPlan.md b/docs/MatrixBernsteinProofPlan.md
index 73b2c39..9514860 100644
--- a/docs/MatrixBernsteinProofPlan.md
+++ b/docs/MatrixBernsteinProofPlan.md
@@ -41,7 +41,7 @@ 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: `MB-S9-lambda-max-operator-norm-bridge-contract`.
+Next safe task: `RM-centered-operator-norm-bound`.
 ## Target Theorem
 
 For a finite family of independent centered self-adjoint random matrices
diff --git a/docs/MatrixConcentrationPlan.md b/docs/MatrixConcentrationPlan.md
index 4bded30..d571a2e 100644
--- a/docs/MatrixConcentrationPlan.md
+++ b/docs/MatrixConcentrationPlan.md
@@ -22,7 +22,7 @@ compatibility APIs around the bounded-Bernstein lintegral Laplace route:
 `matrixBernsteinTraceMGFToLaplaceContract_statement` and
 `matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement`.
 
-Next safe task: `MB-S9-lambda-max-operator-norm-bridge-contract`.
+Next safe task: `RM-centered-operator-norm-bound`.
 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 01fe17e..5719546 100644
--- a/docs/RandomMatrixAPI.md
+++ b/docs/RandomMatrixAPI.md
@@ -39,7 +39,11 @@ mainline. It is documentation only; theorem status is not upgraded here.
 - Its RHS is:
   `ENNReal.ofReal ((n + 1 : Real) * Real.exp (-(t ^ 2 / (2 * sigmaSq + (2 / 3) * R * t))))`.
 - Lambda-max/operator-norm Matrix Bernstein tail theorem remains unproved.
-- Next safe task: `MB-S9-lambda-max-operator-norm-bridge-contract`.
+- Proved rank-one operator-norm prerequisite bridge:
+  `rankOneOperatorNorm_le_vectorSqNorm`,
+  `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and
+  `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`.
+- Next safe task: `RM-centered-operator-norm-bound`.
 
 ## `HighDimProb/RandomMatrix/SelfAdjoint.lean`
 
@@ -91,6 +95,32 @@ mainline. It is documentation only; theorem status is not upgraded here.
 - `lambdaMax_le_iff_quadraticForm_le_statement`: typed statement.
 - `operatorNorm_eq_max_abs_lambda_statement`: typed statement.
 
+## `HighDimProb/RandomMatrix/OperatorNorm.lean`
+
+- `operatorNorm`: def, random-matrix operator norm as a real random variable.
+- `deterministicOperatorNorm`: def, deterministic matrix operator norm using the
+  same scoped L2 convention.
+- `deterministicOperatorNorm_apply`: theorem, definitional bridge.
+- `rankOneOperatorNorm_le_vectorSqNorm`: theorem, `||v vᵀ||op <= ||v||₂²`.
+- `matVecSqNorm`: def.
+- `randomMatVecSqNorm`: def.
+- `OperatorNormBoundSq`: def.
+- `operatorNorm_le_of_operatorNormBoundSq`: theorem.
+- `operatorNormBoundSq_of_operatorNorm_le`: theorem.
+- `isRealRandomVariable_operatorNorm`: theorem.
+
+## `HighDimProb/RandomMatrix/Assumptions.lean`
+
+- `BoundedOperatorNorm`: def, pointwise operator-norm bound for one random
+  matrix.
+- `BoundedOperatorNorm_rankOne_of_sqNorm_bound`: theorem, rank-one pointwise
+  wrapper from vector squared-norm bounds.
+- `PointwiseOperatorNormBound`: def, indexed pointwise operator-norm bound.
+- `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`: theorem, indexed
+  rank-one wrapper from vector squared-norm bounds.
+- `UniformOperatorNormBound`: abbrev.
+- `AeOperatorNormBound`: def.
+
 ## `HighDimProb/RandomMatrix/MatrixOrder.lean`
 
 - `matrixQuadraticForm`: def.
@@ -356,7 +386,7 @@ mainline. It is documentation only; theorem status is not upgraded here.
 
 ## Next Safe Task
 
-MB-S9-lambda-max-operator-norm-bridge-contract: plan the bridge from the proved
+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.
@@ -383,4 +413,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: MB-S9-lambda-max-operator-norm-bridge-contract.
+- Next safe task: RM-centered-operator-norm-bound.
diff --git a/docs/Status.md b/docs/Status.md
index af54b8c..1a036eb 100644
--- a/docs/Status.md
+++ b/docs/Status.md
@@ -8,27 +8,27 @@ 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 newest layer chooses
-`theta = t / (sigmaSq + R * t / 3)` via `bernsteinThetaChoice` and proves the
-conservative exponent form
-`-(t ^ 2 / (2 * sigmaSq + (2 / 3) * R * t))`.
+denominator wrapper. The current prerequisite cleanup also adds the first
+rank-one operator-norm bridge for covariance-style examples.
 
 The latest proved public theorem is:
 
-- `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`
+- `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`
 
-The wrapper proves a one-sided nonempty-dimensional quadratic-form upper-tail
-bound under explicit primitive assumptions, with RHS:
-`ENNReal.ofReal ((n + 1 : Real) * Real.exp (-(t ^ 2 / (2 * sigmaSq + (2 / 3) * R * t))))`.
-Supporting scalar API includes `bernsteinThetaChoice`,
-`bernsteinThetaChoice_range`, and `bernsteinThetaChoice_exponent_eq`. It still
-does not prove 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.
+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
+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.
+The previous optimized quadratic-form theorem remains
+`matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`
+under explicit primitive assumptions.
 
 ## Next Safe Task
 
-- `MB-S9-lambda-max-operator-norm-bridge-contract`
+- `RM-centered-operator-norm-bound`
 
 ## Public Milestone Summary
 
@@ -140,6 +140,7 @@ Last known test status:
 - Stage V1 Lean path visualization infrastructure
 - Stage J1 HighDimProb compile-time OJ / judge suite
 - Stage J2 expanded HighDimProb judge coverage
+- Stage RM-rank-one operator-norm bound for covariance-style rank-one matrices
 
 Stage 1A implemented:
 - probability-space convention
diff --git a/docs/TODO.md b/docs/TODO.md
index 3bbb79c..d86a76f 100644
--- a/docs/TODO.md
+++ b/docs/TODO.md
@@ -12,14 +12,19 @@
 - Done: MB-S9 theta optimization contract proved `bernsteinThetaChoice`,
   `bernsteinThetaChoice_range`, `bernsteinThetaChoice_exponent_eq`, and
   `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`.
+- Done: rank-one operator-norm prerequisite slice added
+  `rankOneOperatorNorm_le_vectorSqNorm`,
+  `BoundedOperatorNorm_rankOne_of_sqNorm_bound`, and
+  `PointwiseOperatorNormBound_rankOne_of_sqNorm_bound`.
 - The optimized theorem remains one-sided, quadratic-form, and under explicit
   `troppMasterTraceMGFFiniteFamily_statement` plus pointwise
   `bernsteinMatrixExp_le_quadratic_statement` assumptions.
-- Not proved: 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: MB-S9-lambda-max-operator-norm-bridge-contract.
+- Not proved: centered summand operator-norm bound, 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.
 ## Stage M3 Scalar Closeout TODO Audit
 
 The forward scalar subGaussian proof spine is closed as an experimental
@@ -194,8 +199,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: MB-S9-lambda-max-operator-norm-bridge-contract. |
-| 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: MB-S9-lambda-max-operator-norm-bridge-contract. |
+| 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. |
 ## MB-S9 Tropp Shape Refactor Follow-Up
 
 The trace-exp layer now exposes `troppMasterTraceMGFFiniteFamily_statement`,
@@ -210,7 +215,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: MB-S9-lambda-max-operator-norm-bridge-contract.
+- Next safe task: RM-centered-operator-norm-bound.
 
 ## MB-S9 Matrix Bernstein Trace-MGF Under Primitives Follow-Up
 
@@ -219,4 +224,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: MB-S9-lambda-max-operator-norm-bridge-contract.
+- Next safe task: RM-centered-operator-norm-bound.
diff --git a/docs/TermMap.md b/docs/TermMap.md
index fa970b4..d418ab5 100644
--- a/docs/TermMap.md
+++ b/docs/TermMap.md
@@ -130,6 +130,8 @@ Note: some declarations exist as scaffolds, but the corresponding concept is not
 | Matrix-vector squared norm | Operator-norm bridge prerequisites | Squared Euclidean norm of `A x` using explicit matrix-vector finite sums. | `Finset.univ.sum`, `matVec` normal form, `Matrix.mulVec`, `EuclideanSpace` L2 norm | `matVecSqNorm`, `randomMatVecSqNorm`, `sqNorm_matVec_eq_matVecSqNorm`, `isRealRandomVariable_randomMatVecSqNorm`, `matVecSqNorm_eq_norm_sq_toLp_mulVec`, `norm_sq_toLp_mulVec_eq_matVecSqNorm` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | implemented/proven experimental API | Provides a theorem-friendly finite-sum normal form and an exact bridge to the Mathlib L2 norm of `A x`. |
 | Squared operator-norm bound predicate | Matrix concentration prerequisites | Pointwise squared matrix-vector bound over all explicit unit vectors. | `IsUnitVector`, `matVecSqNorm`, `Matrix.Norms.L2Operator` | `OperatorNormBoundSq`, `RandomOperatorNormBoundSq`, `matVecSqNorm_le_of_operatorNormBoundSq`, `operatorNorm_le_of_operatorNormBoundSq`, `operatorNormBoundSq_of_operatorNorm_le` | `HighDimProb/RandomMatrix/OperatorNorm.lean` | implemented/proven experimental API | The explicit predicate is retained for theorem statements and is now bridged in both directions with `deterministicOperatorNorm` under the visible nonnegative-scale hypotheses. |
 | 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. |
 | 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 ee1f826..ffdcb8d 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: `MB-S9-lambda-max-operator-norm-bridge-contract`.
+Next safe task: `RM-centered-operator-norm-bound`.
 ## 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
-  MB-S9-lambda-max-operator-norm-bridge-contract.
+  RM-centered-operator-norm-bound.
 
 ## 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 MB-S9-lambda-max-operator-norm-bridge-contract.
+- Priority: next safe task is RM-centered-operator-norm-bound.
 
 ## 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 MB-S9-lambda-max-operator-norm-bridge-contract.
+- Priority: next safe task is RM-centered-operator-norm-bound.
 
 ## 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 MB-S9-lambda-max-operator-norm-bridge-contract.
+- Priority: next safe task is RM-centered-operator-norm-bound.
 
 
 
@@ -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 MB-S9-lambda-max-operator-norm-bridge-contract.
+- Priority: next safe task is RM-centered-operator-norm-bound.
 
 ## Matrix Bernstein Trace-MGF to Laplace/Tail Contract (MB-S9)
 
@@ -1986,4 +1986,4 @@ 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 MB-S9-lambda-max-operator-norm-bridge-contract.
+- Priority: next safe task is RM-centered-operator-norm-bound.