Bridge exact-row variance proxies to centered-square wrappers

HighDimProb/RandomMatrix/HardboneStatements.lean

@@ -616,6 +616,7 @@ theorem sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two
         integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two
           (P := P) (X := X i) (R := R i) (hLp i) (hSq i))
       hSq hR)
+
 /-- Generic provider-chain target from centered-square comparisons to a
 variance-proxy norm bound.
 
@@ -686,6 +687,98 @@ theorem varianceProxyNormBound_of_centeredSquareChain_expansion
   hChain
     (fun i => matrixSquare_centeredRandomMatrix_expectation_expansion (P := P) (A i))
     hLE hNorm
+/-- Exact-row sample-covariance sharp-chain statement provider from the generic
+centered-square variance-proxy chain.
+
+This bridges the generic `varianceProxyNormBound_of_centeredSquareChain_statement`
+for the rank-one row family to the sample-covariance-specific
+`sampleCovarianceVarianceProxy_sharp_statement`. The concrete row assumptions
+only discharge the integrability premises needed by the centered rank-one
+second-moment comparison. The generic centered-square chain remains explicit;
+this theorem does not prove Matrix Bernstein, Tropp/Lieb, trace-MGF iteration,
+or an unconditional sample-covariance tail bound. -/
+theorem sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    {m n : Nat}
+    (X : Fin m -> RandomVector Omega n)
+    (R : Fin m -> Real)
+    (hChain : @varianceProxyNormBound_of_centeredSquareChain_statement
+      Omega mOmega P _ (Fin m) _ n (rankOneRandomMatrixFamily X)
+      (fun i => matrixSecondMoment P (rankOneRandomMatrix (X i)))
+      (rowSqNormVarianceProxyNormRHS R))
+    (hMeas : forall i, IsRandomVector P (X i))
+    (hLp : forall i, forall j : Fin n,
+      MemLpRealRandomVariable P (coord (X i) j) 2)
+    (hSq : forall i omega, vectorSqNorm (X i omega) <= R i) :
+    @sampleCovarianceVarianceProxy_sharp_statement
+      Omega mOmega P _ m n X
+      (fun i => matrixSecondMoment P (rankOneRandomMatrix (X i)))
+      (rowSqNormVarianceProxyNormRHS R) := by
+  intro hCentered hSecond hNorm
+  have hResult : MatrixVarianceProxyNormBound P
+      (centeredRandomMatrixFamily P (rankOneRandomMatrixFamily X))
+      (rowSqNormVarianceProxyNormRHS R) := by
+    apply hChain
+    · intro i
+      exact matrixSquare_centeredRandomMatrix_expectation_expansion
+        (P := P) ((rankOneRandomMatrixFamily X) i)
+    · intro i
+      have hRankSq : IntegrableRandomMatrix P
+          (randomMatrixSquare (rankOneRandomMatrix (X i))) :=
+        integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two
+          (P := P) (X := X i) (R := R i) (hLp i) (hSq i)
+      have hRankInt : IntegrableRandomMatrix P (rankOneRandomMatrix (X i)) :=
+        integrableRandomMatrix_rankOneRandomMatrix_of_memLp_two
+          (P := P) (X := X i) (hLp i)
+      have hCenteredSq : IntegrableRandomMatrix P
+          (randomMatrixSquare (centeredRankOneRandomMatrix P (X i))) := by
+        simpa [centeredRankOneRandomMatrix] using
+          integrableRandomMatrix_randomMatrixSquare_centeredRandomMatrix
+            (P := P) (A := rankOneRandomMatrix (X i)) hRankInt hRankSq
+      have hCenteredLE : MatrixLE
+          (matrixSecondMoment P (centeredRankOneRandomMatrix P (X i)))
+          (matrixSecondMoment P (rankOneRandomMatrix (X i))) :=
+        hCentered i (hMeas i) (hLp i) hCenteredSq hRankSq
+      have hLE : MatrixLE
+          (matrixSecondMoment P (centeredRankOneRandomMatrix P (X i)))
+          (matrixSecondMoment P (rankOneRandomMatrix (X i))) := hCenteredLE
+      simpa [rankOneRandomMatrixFamily, centeredRankOneRandomMatrix] using
+        matrixLE_trans hLE (hSecond i)
+    · simpa [rankOneRandomMatrixFamily] using hNorm
+  simpa [centeredRankOneRandomMatrixFamily] using hResult
+
+/-- Exact-row sample-covariance variance-proxy consumer from the generic
+centered-square chain.
+
+Compared with `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`,
+this theorem replaces the sample-specific sharp-chain premise by the generic
+centered-square chain plus concrete row measurability, `MemLp 2`, and exact row
+squared-norm witnesses. The row-specific deterministic norm control remains the
+existing `rowSqNormVarianceProxyNormRHS R` route. -/
+theorem sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    {m n : Nat}
+    (X : Fin m -> RandomVector Omega n)
+    (R : Fin m -> Real)
+    (hChain : @varianceProxyNormBound_of_centeredSquareChain_statement
+      Omega mOmega P _ (Fin m) _ n (rankOneRandomMatrixFamily X)
+      (fun i => matrixSecondMoment P (rankOneRandomMatrix (X i)))
+      (rowSqNormVarianceProxyNormRHS R))
+    (hMeas : forall i, IsRandomVector P (X i))
+    (hLp : forall i, forall j : Fin n,
+      MemLpRealRandomVariable P (coord (X i) j) 2)
+    (hSq : forall i omega, vectorSqNorm (X i omega) <= R i)
+    (hR : forall i, 0 <= R i) :
+    MatrixVarianceProxyNormBound P
+      (centeredRankOneRandomMatrixFamily P X)
+      (rowSqNormVarianceProxyNormRHS R) :=
+  sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two
+    (P := P) X R
+    (sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two
+      (P := P) X R hChain hMeas hLp hSq)
+    hLp hSq hR
 /-! ## Dimension, support, and effective-rank hardbone statement chain -/
 
 /-- Rank-refined trace-exponential dimension-factor target with an explicit

HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean

@@ -45,6 +45,7 @@ open HighDimProb
 #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound
 #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive
 #check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive
+#check HighDimProb.sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive
 #check HighDimProb.sampleCovariance_selfAdjointOperatorNormTailEvent_subset_centeredRowRankOneSum
 #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_under_explicit_variance_proxy
 #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_nonempty_under_explicit_variance_proxy
@@ -54,6 +55,8 @@ open HighDimProb
 #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters_of_troppPrimitives
 #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters
 #check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives
+#check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives
+#check HighDimProb.sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives
 #check HighDimProb.negRandomMatrixFamily
 #check HighDimProb.matrixExpScaledFamily_negRandomMatrixFamily
 #check HighDimProb.integrableRandomMatrix_matrixExpScaledFamily_negRandomMatrixFamily
@@ -84,6 +87,7 @@ open HighDimProb
 #check HighDimProb.centeredSampleCovarianceRowRankOneFamilyNeg_expIntegrable_of_expIntegrable_neg_theta
 #check HighDimProb.centeredSampleCovarianceRowRankOneSumNeg_traceExpIntegrable_of_traceExpIntegrable_neg_theta
 #check HighDimProb.centeredSampleCovarianceRowRankOneFamilyNeg_cfcPrimitive_of_cfcPrimitive_neg_theta
+#check HighDimProb.MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two
 #check HighDimProb.matrixVarianceProxyNorm
 #check HighDimProb.PointwiseOperatorNormBound
 #check HighDimProb.IndependentSelfAdjointRandomMatrices

HighDimProbJudge/RandomMatrix/TraceExpUse.lean

@@ -124,6 +124,8 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #check HighDimProb.sampleCovarianceVarianceProxy_sharp_statement
 #check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment
 #check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment
+#check HighDimProb.sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two
+#check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_statement
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_expansion

HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean

@@ -40,6 +40,8 @@ import HighDimProb.RandomMatrix
 #check HighDimProb.MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound
 #check HighDimProb.MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two
 #check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two
+#check HighDimProb.sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two
+#check HighDimProb.sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain
 #check HighDimProb.matrixQuadraticForm_sum
 #check HighDimProb.matrixQuadraticForm_add
 #check HighDimProb.matrixQuadraticForm_smul

HighDimProbTest/RandomMatrixConcentrationAPI.lean

@@ -159,6 +159,7 @@ variable (R theta sigma2 c c1 c2 t bound K : Real)
 #check sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound
 #check sampleCovariance_quadraticForm_tail_optimized_under_rowSqNorm_bound_of_troppPrimitive
 #check sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitive
+#check sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive
 #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_under_explicit_variance_proxy
 #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_nonempty_under_explicit_variance_proxy
 #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_explicit_variance_proxy
@@ -167,6 +168,8 @@ variable (R theta sigma2 c c1 c2 t bound K : Real)
 #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_adapters_of_troppPrimitives
 #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters
 #check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives
+#check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives
+#check sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives
 #check centeredSampleCovarianceRowRankOneFamilyNeg
 #check centeredSampleCovarianceRowRankOneSumNeg
 #check isRandomMatrix_negRandomMatrixFamily
@@ -185,6 +188,7 @@ variable (R theta sigma2 c c1 c2 t bound K : Real)
 #check centeredSampleCovarianceRowRankOneFamilyNeg_expIntegrable_of_expIntegrable_neg_theta
 #check centeredSampleCovarianceRowRankOneSumNeg_traceExpIntegrable_of_traceExpIntegrable_neg_theta
 #check centeredSampleCovarianceRowRankOneFamilyNeg_cfcPrimitive_of_cfcPrimitive_neg_theta
+#check MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two
 #check operatorNorm_eq_spectralRadius_of_selfAdjointStatement
 #check HighProbabilityBound
 #check highProbabilityBound

HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean

@@ -51,6 +51,8 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #check sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment
 #check sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment
 #check sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two
+#check sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two
+#check sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain
 #check varianceProxyNormBound_of_centeredSquareChain_statement
 #check traceMatrixExp_le_rank_exp_lambdaMax_statement
 #check traceMatrixExp_le_supportDim_exp_lambdaMax_statement

docs/JudgeSystem.md

@@ -52,9 +52,9 @@ theorems or typed statements without relying on local test internals.
   PSD and quadratic-form nonnegativity APIs.
 - `HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean`: matrix square, second
   moment, variance proxy, semantic variance-proxy bounds,
-  variance-proxy norm, self-adjointness lemmas, matrix expectation PSD/order
-  and add/smul/zero/constant normalization lemmas, PSD typed targets, and
-  matrix Bernstein statement surface.
+  variance-proxy norm, self-adjointness lemmas, exact-row generic-centered-square
+  chain bridge visibility, matrix expectation PSD/order and add/smul/zero/constant
+  normalization lemmas, PSD typed targets, and matrix Bernstein statement surface.
 - `HighDimProbJudge/RandomMatrix/SpectralUse.lean`: lambda-max wrappers,
   ordered endpoint wrappers, quadratic-form bound predicates, monotonicity
   lemmas, two-sided tail events, and spectral tail event APIs.
@@ -73,8 +73,9 @@ theorems or typed statements without relying on local test internals.
   Laplace/Chernoff/operator-norm Laplace statement APIs.
 - `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`: proof-ready matrix
   Bernstein statement surface, `matrixBernsteinLaplacePrerequisitesStatement`,
-  `matrixBernsteinTraceMGF_statement`, and its main structural/analytic
-  dependencies.
+  `matrixBernsteinTraceMGF_statement`, sample-covariance exact-row and centered-square-chain wrapper visibility,
+  negative exact-row variance-proxy provider visibility, and their main
+  structural/analytic dependencies.
 
 ## How It Differs From Normal Tests
 

docs/LeafPlan.md

@@ -35,10 +35,11 @@
   - Stage M-real-1: real-exponent `SubGaussianMoment` bridge
   - Stage M-real-2: real-exponent `SubExponentialMoment` bridge
   - Stage SC-final-update: scalar closeout refreshed after both moment bridges
-  - Current repository next task:
-    RM-VP-negative-exact-row-variance-proxy-provider-contract. Natural-state
-    assumption bundling, negative trace-MGF provider cleanup, Matrix Bernstein,
-    Hanson-Wright, and WLLN/SLLN remain separate future directions.
+  - Current repository closeout:
+    PR/check review for RM-VP-centered-square-chain-wrapper-integration-contract.
+    Natural-state assumption bundling, negative trace-MGF provider cleanup,
+    Matrix Bernstein, Hanson-Wright, and WLLN/SLLN remain separate future
+    directions.
 - OrliczToTail
 - TailToOrlicz
 - MomentImplications
@@ -236,7 +237,35 @@
 - Boundary preserved: this does not prove the hardbone sharp-chain provider,
   Tropp/Lieb, Golden-Thompson, Bernstein CFC, two-sided control, operator-norm
   control, or Matrix Bernstein.
-- Next safe leaf: `RM-VP-negative-exact-row-variance-proxy-provider-contract`.
+- Follow-up completed proof leaf:
+  `RM-VP-negative-exact-row-variance-proxy-provider-contract`, adding
+  `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`
+  as the negative-side exact-row variance-proxy provider by transferring the
+  positive row-specific bound through `matrixVarianceProxy_negRandomMatrixFamily`.
+- Boundary preserved: this does not prove two-sided/operator-norm wrapper
+  integration, concrete row-moment evaluation, Tropp/Lieb, Golden-Thompson,
+  Bernstein CFC, or Matrix Bernstein.
+- Follow-up completed proof leaf:
+  `RM-VP-two-sided-operator-norm-exact-row-wrapper-integration-contract`, adding
+  `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives` as the CFC-free operator-norm wrapper over positive and negative
+  row-specific exact-row variance-proxy RHS values.
+- Boundary preserved: this does not prove concrete row-moment evaluation, new
+  hardbone sharp-chain providers, Tropp/Lieb, Golden-Thompson, Bernstein CFC,
+  or Matrix Bernstein.
+- Follow-up completed proof leaf:
+  `RM-VP-concrete-row-moment-evaluation-contract`, adding
+  `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two`
+  and
+  `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain`
+  as the exact-row bridge from the generic centered-square variance-proxy chain
+  to the sample-specific sharp-chain statement and consumer.
+- Follow-up completed proof leaf:
+  `RM-VP-centered-square-chain-wrapper-integration-contract`, adding
+  positive-side quadratic-form and two-sided/operator-norm wrappers that consume
+  generic centered-square variance-proxy chains over the row-rank-one family.
+- Boundary preserved: this does not prove the generic centered-square chain,
+  Tropp/Lieb, Golden-Thompson, Bernstein CFC, or Matrix Bernstein.
+- Next safe leaf: PR/check closeout, then select the next RandomMatrix leaf.
 
 ## Process