Expose centered-square provider blocker honestly

HighDimProb/RandomMatrix/HardboneStatements.lean

@@ -1,4 +1,5 @@
 import HighDimProb.RandomMatrix.TraceExp
+import HighDimProb.RandomMatrix.MatrixOrder
 import HighDimProb.RandomMatrix.Assumptions
 import HighDimProb.Analysis.RealInequalities
 
@@ -639,6 +640,61 @@ abbrev varianceProxyNormBound_of_centeredSquareChain_statement
         sigma2 ->
         MatrixVarianceProxyNormBound P (centeredRandomMatrixFamily P A) sigma2
 
+/-- Typed blocker for Loewner-to-operator-norm monotonicity of deterministic
+variance proxies.
+
+The centered-square provider can prove the finite-sum Loewner comparison from
+per-summand comparisons. Turning that comparison into a scalar operator-norm
+bound still requires a PSD/order-to-norm monotonicity theorem, kept explicit by
+this contract. -/
+abbrev deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement {n : Nat}
+    (U V : Matrix (Fin n) (Fin n) Real) : Prop :=
+  IsPSDMatrix U ->
+    MatrixLE U V ->
+      deterministicMatrixVarianceProxyNorm U <= deterministicMatrixVarianceProxyNorm V
+
+/-- Centered-square variance-proxy provider under an explicit norm-monotonicity
+contract.
+
+This theorem proves the available bookkeeping part of the generic
+centered-square chain: per-summand Loewner comparisons sum to a variance-proxy
+Loewner comparison. The remaining conversion from Loewner order to deterministic
+operator norm is exactly the `hNormMono` premise. -/
+theorem varianceProxyNormBound_of_centeredSquareChain_of_normMono
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P]
+    {I : Type*} [Fintype I] {n : Nat}
+    (A : I -> RandomMatrix Omega n n)
+    (V : I -> Matrix (Fin n) (Fin n) Real)
+    (sigma2 : Real)
+    (hNormMono :
+      deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement
+        (Finset.univ.sum fun i : I =>
+          matrixSecondMoment P (centeredRandomMatrix P (A i)))
+        (Finset.univ.sum fun i : I => V i))
+    (hPSD : IsPSDMatrix
+      (Finset.univ.sum fun i : I =>
+        matrixSecondMoment P (centeredRandomMatrix P (A i))))
+    (hLE : forall i,
+      MatrixLE (matrixSecondMoment P (centeredRandomMatrix P (A i))) (V i))
+    (hNorm : deterministicMatrixVarianceProxyNorm (Finset.univ.sum fun i => V i) <=
+      sigma2) :
+    MatrixVarianceProxyNormBound P (centeredRandomMatrixFamily P A) sigma2 := by
+  have hSumLE : MatrixLE
+      (Finset.univ.sum fun i : I =>
+        matrixSecondMoment P (centeredRandomMatrix P (A i)))
+      (Finset.univ.sum fun i : I => V i) :=
+    matrixLE_sum hLE
+  have hNormLe :
+      deterministicMatrixVarianceProxyNorm
+          (Finset.univ.sum fun i : I =>
+            matrixSecondMoment P (centeredRandomMatrix P (A i))) <=
+        deterministicMatrixVarianceProxyNorm (Finset.univ.sum fun i : I => V i) :=
+    hNormMono hPSD hSumLE
+  simpa [MatrixVarianceProxyNormBound, matrixVarianceProxyNorm,
+    deterministicMatrixVarianceProxyNorm, matrixVarianceProxy, centeredRandomMatrixFamily]
+    using hNormLe.trans hNorm
+
 /-- Thin consumer for the centered-square variance-proxy provider chain.
 
 This theorem only applies the explicit provider-chain statement. It does not

HighDimProb/RandomMatrix/MatrixOrder.lean

@@ -289,6 +289,24 @@ theorem matrixLE_add {n : Nat}
   rw [hEq]
   exact hsum
 
+/-- Finite sums preserve the explicit Loewner-style matrix comparison. -/
+theorem matrixLE_sum {I : Type*} [Fintype I] {n : Nat}
+    {A B : I -> Matrix (Fin n) (Fin n) Real}
+    (hAB : forall i, MatrixLE (A i) (B i)) :
+    MatrixLE (Finset.univ.sum fun i : I => A i)
+      (Finset.univ.sum fun i : I => B i) := by
+  unfold MatrixLE at *
+  have hsum : IsPSDMatrix (Finset.univ.sum fun i : I => B i - A i) :=
+    isPSDMatrix_sum hAB
+  have hEq :
+      (Finset.univ.sum fun i : I => B i) -
+          (Finset.univ.sum fun i : I => A i) =
+        Finset.univ.sum fun i : I => B i - A i := by
+    ext r c
+    simp [Matrix.sub_apply, Matrix.sum_apply, Finset.sum_sub_distrib]
+  rw [hEq]
+  exact hsum
+
 /-- Adding the same matrix on the left preserves `MatrixLE`. -/
 theorem matrixLE_add_left {n : Nat}
     (C : Matrix (Fin n) (Fin n) Real)

HighDimProbJudge/RandomMatrix/TraceExpUse.lean

@@ -127,6 +127,8 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #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.deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement
+#check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_of_normMono
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain
 #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_expansion
 #check HighDimProb.traceMatrixExp_le_rank_exp_lambdaMax_statement

HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean

@@ -54,6 +54,7 @@ import HighDimProb.RandomMatrix
 #check HighDimProb.matrixLE_sub_right_of_isPSD
 #check HighDimProb.matrixLE_trans
 #check HighDimProb.matrixLE_add
+#check HighDimProb.matrixLE_sum
 #check HighDimProb.matrixLE_add_left
 #check HighDimProb.matrixLE_add_right
 #check HighDimProb.matrixLE_smul_of_nonneg

HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean

@@ -54,6 +54,8 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #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 deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement
+#check varianceProxyNormBound_of_centeredSquareChain_of_normMono
 #check traceMatrixExp_le_rank_exp_lambdaMax_statement
 #check traceMatrixExp_le_supportDim_exp_lambdaMax_statement
 #check matrixExpSupportDomination_identity_statement

HighDimProbTest/RandomMatrixVarianceProxyAPI.lean

@@ -65,6 +65,7 @@ variable (hRnonneg : 0 <= R)
 #check matrixLE_sub_right_of_isPSD
 #check matrixLE_trans
 #check matrixLE_add
+#check matrixLE_sum
 #check matrixLE_add_left
 #check matrixLE_add_right
 #check matrixLE_smul_of_nonneg

docs/JudgeSystem.md

@@ -65,7 +65,8 @@ theorems or typed statements without relying on local test internals.
   nonnegativity bridges, random self-adjoint trace-exp moment nonnegativity,
   real/lintegral bridge theorem, natural-state Tropp/trace-MGF route checks,
   the hardbone matrix-exp/log normalization theorem, the proved matrix log/order
-  bridge, and remaining typed statement APIs.
+  bridge, centered-square provider/norm-monotonicity contract APIs, and
+  remaining typed statement APIs.
 - `HighDimProbJudge/RandomMatrix/LaplaceUse.lean`: matrix Laplace RHS and
   lintegral RHS vocabulary, trace-exp threshold events, MB-S5 conditional
   Markov/Laplace bridge APIs, MB-S6 explicit-dominance conditional wrappers,
@@ -256,7 +257,7 @@ MB-S9-matrixle-algebra-proof adds variance-proxy judge checks for
 `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_trans`, `matrixLE_add`, `matrixLE_sum`, `matrixLE_add_left`,
 `matrixLE_add_right`, and `matrixLE_smul_of_nonneg`. The examples use only
 explicit MatrixLE/PSD hypotheses and do not claim the single-summand MGF
 theorem, Bernstein CFC proof, trace-mgf provider, Golden-Thompson, Lieb, or

docs/RandomMatrixAPI.md

@@ -122,6 +122,8 @@ Variance-proxy / centered-square chain:
 - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions`
 - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`
 - `varianceProxyNormBound_of_centeredSquareChain_statement`
+- `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement`
+- `varianceProxyNormBound_of_centeredSquareChain_of_normMono`
 - `varianceProxyNormBound_of_centeredSquareChain_expansion`
 
 Dimension / rank / effective-rank chain:
@@ -153,6 +155,7 @@ Thin hardbone consumers:
 - `troppMasterTraceMGFConditionalStep_of_conditioningBridge`
 - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider`
 - `varianceProxyNormBound_of_centeredSquareChain`
+- `varianceProxyNormBound_of_centeredSquareChain_of_normMono`
 - `traceMatrixExp_le_rank_exp_lambdaMax`
 - `traceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjection`
 - `traceMatrixExp_le_supportDim_exp_lambdaMax`
@@ -171,7 +174,7 @@ Hardbone status table:
 | Tropp/Lieb/GT one-step | `troppMasterTraceMGFStep_of_liebJensen_statement` | typed-prop | `troppMasterTraceMGFStep_of_liebJensen` | Lieb concavity, probability-measure Jensen, log-exp normalization; Golden-Thompson is separate |
 | Conditioning / independence | `troppConditionalStep_of_iIndepFun_statement` | proven by `troppConditionalStep_of_iIndepFun` | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | thin forwarder only; generated histories, history/current-step independence, finite-family independence, and conditional expectation reduction remain explicit premises |
 | Trace-exp integrability | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement` | typed-prop with proved thin consumer | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider` | automatic absolute domination, Golden-Thompson/product, or boundedness provider |
-| Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion and centered rank-one second-moment comparison proved; typed-prop chain has proved thin consumers | `matrixSquare_centeredRandomMatrix_expectation_expansion`, `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment`, `centeredRankOneSquare_le_rankOneSecondMoment`, `varianceProxyNormBound_of_centeredSquareChain`, `varianceProxyNormBound_of_centeredSquareChain_expansion`, `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment`, `deterministicMatrixVarianceProxyNorm_sum_le_sum`, `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound`, `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives`, `SampleCovarianceExactRowCenteredSquareTroppAssumptions`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions`, `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_products`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two`, `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` | full generic centered-square-chain proof remains external; wrappers and bundles still require Tropp/Lieb and analytic integrability premises |
+| Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement`, `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion, finite-sum MatrixLE bookkeeping, and centered rank-one second-moment comparison proved; typed-prop chain has proved thin consumers | `matrixSquare_centeredRandomMatrix_expectation_expansion`, `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment`, `centeredRankOneSquare_le_rankOneSecondMoment`, `varianceProxyNormBound_of_centeredSquareChain`, `varianceProxyNormBound_of_centeredSquareChain_of_normMono`, `varianceProxyNormBound_of_centeredSquareChain_expansion`, `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment`, `deterministicMatrixVarianceProxyNorm_sum_le_sum`, `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound`, `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitive`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives`, `SampleCovarianceExactRowCenteredSquareTroppAssumptions`, `sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions`, `SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_integrable_four_products`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four`, `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two`, `MatrixVarianceProxyNormBound_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two` | full generic centered-square-chain proof remains external; the norm-monotonicity provider is an explicit blocker, and wrappers/bundles still require Tropp/Lieb and analytic integrability premises |
 | Dimension / support / effective rank | `traceMatrixExp_le_rank_exp_lambdaMax_statement`, `traceMatrixExp_le_supportDim_exp_lambdaMax_statement`, `traceMatrixExp_effectiveRank_bound_statement`, `matrixExpSupportDomination_identity_statement`, `traceMatrixExp_excess_supportDim_exp_lambdaMax_statement` | rank/support targets and effective-rank consumer proved under explicit support, PSD, lambda-max, and trace-certificate assumptions; ambient trace certificate and star-projection rank/PSD consumer proved; identity support provider target named only; excess trace bridge and supportDim consumer proved under explicit excess certificate | `traceMatrixExp_le_rank_exp_lambdaMax`, `traceMatrixExp_le_rank_exp_lambdaMax_of_isStarProjection`, `traceMatrixExp_le_supportDim_exp_lambdaMax`, `traceMatrixExp_excess_supportDim_exp_lambdaMax`, `traceMatrixExp_effectiveRank_bound`, `traceMatrixExp_effectiveRank_bound_of_ambientTraceCertificate`; deterministic helpers include `MatrixExpSupportDomination`, `MatrixExpExcessSupportDomination`, `traceMatrixExp_le_card_add_trace_support_mul_exp_sub_one_of_excessSupportDomination`, `traceMatrixExp_eq_sum_exp_eigenvalues`, `traceMatrixExp_smul_le_card_add_trace_div_mul_exp_sub_one_of_psd_lambdaMax_le`, `matrixTrace_le_card_mul_of_isPSD_lambdaMaxOrdered_le`, `matrixTrace_eq_rank_of_isStarProjection`, `isPSDMatrix_of_isStarProjection` | identity/excess support-domination providers and support-construction certificates; true effective-rank trace certificate provider beyond ambient dimension |
 | Thin consumers | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | proven | public API/test/judge/example checks | thin wrapper only; no hard fact is discharged |
 
@@ -325,6 +328,7 @@ and they are not tail wrappers by themselves.
 - `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_memLp_four`
 - `integrableRandomMatrix_randomMatrixSquare_centeredRankOneRandomMatrixFamily_of_sqNorm_bound_memLp_two`
 - `matrixSecondMoment_centeredRandomMatrix`
+- `matrixLE_sum`
 - `deterministicMatrixVarianceProxyNorm_sum_le_sum`
 - `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound`
 - `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound`

docs/Status.md

@@ -117,6 +117,9 @@ Hardbone proved leaves, deterministic bridges, statement targets, and thin consu
 - `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider`
 - `varianceProxyNormBound_of_centeredSquareChain`
 - `matrixSquare_centeredRandomMatrix_expectation_expansion`
+- `matrixLE_sum`
+- `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement`
+- `varianceProxyNormBound_of_centeredSquareChain_of_normMono`
 - `varianceProxyNormBound_of_centeredSquareChain_expansion`
 - `matrixTrace_smul`
 - `matrixTrace_le_of_matrixLE`
@@ -215,10 +218,14 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact
   hardbone-consumer providers only; they do not duplicate the crude
   variance-proxy norm theorem. The
   variance-proxy provider-chain consumer is
-  proved as `varianceProxyNormBound_of_centeredSquareChain`; the newer
-  `varianceProxyNormBound_of_centeredSquareChain_expansion` removes the explicit
-  centered-square expansion argument but still requires Loewner comparison and
-  deterministic norm-control assumptions. The rank/support trace-bound bridge is now proved through
+  proved as `varianceProxyNormBound_of_centeredSquareChain`. The provider route
+  `varianceProxyNormBound_of_centeredSquareChain_of_normMono` now proves the
+  finite-sum Loewner bookkeeping with `matrixLE_sum`, while keeping
+  Loewner-to-deterministic-operator-norm monotonicity as the explicit
+  `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` blocker. The
+  newer `varianceProxyNormBound_of_centeredSquareChain_expansion` removes the
+  explicit centered-square expansion argument but still requires Loewner
+  comparison and deterministic norm-control assumptions. The rank/support trace-bound bridge is now proved through
   `traceMatrixExp_le_trace_support_exp_lambdaMax_of_supportDomination`
   and the `traceMatrixExp_le_rank_exp_lambdaMax` /
   `traceMatrixExp_le_supportDim_exp_lambdaMax` consumers. Explicit