From f1ed86198fe0b1ac2c6943a0def0a344cf93bd5a Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Sat, 20 Jun 2026 08:07:02 +0000 Subject: [PATCH] Discharge deterministic variance-proxy norm monotonicity Constraint: The bridge is only deterministic PSD Loewner-to-operator-norm monotonicity, not a Tropp/Lieb or centered-square-chain proof. Rejected: Proving a broader Matrix Bernstein wrapper here | would hide unrelated analytic and trace-MGF blockers. Confidence: high Scope-risk: narrow Directive: Reuse deterministicMatrixVarianceProxyNorm_mono_of_matrixLE as the contract witness; keep remaining centered-square and Tropp assumptions explicit. Tested: python .github/scripts/check_text_quality.py; python scripts/judge_policy_check.py; git diff --check; lake build HighDimProbJudge; lake test; lake build Not-tested: GitHub CI not run locally. --- .../RandomMatrix/HardboneStatements.lean | 38 ++++++++++ HighDimProb/RandomMatrix/MatrixOrder.lean | 32 ++++++++- HighDimProb/RandomMatrix/Spectral.lean | 70 ++++++++++++++----- .../RandomMatrix/TraceExpUse.lean | 1 + .../RandomMatrix/VarianceProxyUse.lean | 3 + .../RandomMatrixHardboneStatementsAPI.lean | 1 + .../RandomMatrixVarianceProxyAPI.lean | 3 + docs/JudgeSystem.md | 5 +- docs/RandomMatrixAPI.md | 3 +- docs/Status.md | 14 ++-- docs/TODO.md | 7 +- docs/TestPlan.md | 5 +- docs/TheoremAtlas.md | 10 +-- 13 files changed, 153 insertions(+), 39 deletions(-) diff --git a/HighDimProb/RandomMatrix/HardboneStatements.lean b/HighDimProb/RandomMatrix/HardboneStatements.lean index 59a0f36..ad89601 100644 --- a/HighDimProb/RandomMatrix/HardboneStatements.lean +++ b/HighDimProb/RandomMatrix/HardboneStatements.lean @@ -653,6 +653,44 @@ abbrev deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement {n : Nat} MatrixLE U V -> deterministicMatrixVarianceProxyNorm U <= deterministicMatrixVarianceProxyNorm V +/-- Deterministic PSD Loewner monotonicity for the variance-proxy norm. + +This discharges the local HighDimProb-to-Mathlib order bridge only: `U` is +assumed PSD in the explicit HighDimProb predicate, `U <= V` is assumed via the +explicit `MatrixLE` predicate, and the conclusion is the corresponding +operator-norm monotonicity for deterministic variance proxies. -/ +theorem deterministicMatrixVarianceProxyNorm_mono_of_matrixLE {n : Nat} + (U V : Matrix (Fin n) (Fin n) Real) : + deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement U V := by + intro hU hUV + cases n with + | zero => + have hUzero : U = 0 := by + ext i + exact Fin.elim0 i + have hVzero : V = 0 := by + ext i + exact Fin.elim0 i + simp [hUzero, hVzero, deterministicMatrixVarianceProxyNorm, + deterministicOperatorNorm] + | succ n => + have hUself : IsSelfAdjointMatrix U := + (posSemidef_of_isPSDMatrix hU).1 + rcases exists_unitVector_abs_matrixQuadraticForm_eq_deterministicOperatorNorm + hUself with ⟨x, hx, hnorm⟩ + have hUquad_nonneg : 0 <= matrixQuadraticForm U x := hU.2 x + have hnormU_eq : + deterministicMatrixVarianceProxyNorm U = matrixQuadraticForm U x := by + rw [deterministicMatrixVarianceProxyNorm, ← hnorm, + abs_of_nonneg hUquad_nonneg] + calc + deterministicMatrixVarianceProxyNorm U + = matrixQuadraticForm U x := hnormU_eq + _ <= matrixQuadraticForm V x := quadraticForm_le_of_matrixLE hUV x + _ <= deterministicMatrixVarianceProxyNorm V := by + simpa [deterministicMatrixVarianceProxyNorm] using + matrixQuadraticForm_le_deterministicOperatorNorm V hx + /-- Centered-square variance-proxy provider under an explicit norm-monotonicity contract. diff --git a/HighDimProb/RandomMatrix/MatrixOrder.lean b/HighDimProb/RandomMatrix/MatrixOrder.lean index 2b19c09..4244e42 100644 --- a/HighDimProb/RandomMatrix/MatrixOrder.lean +++ b/HighDimProb/RandomMatrix/MatrixOrder.lean @@ -1,3 +1,4 @@ +import Mathlib.Analysis.Matrix.Order import HighDimProb.RandomMatrix.Algebra import HighDimProb.RandomMatrix.SelfAdjoint @@ -19,7 +20,7 @@ form. `MatrixLE A B` is the corresponding Loewner-style predicate namespace HighDimProb open MeasureTheory -open scoped BigOperators +open scoped BigOperators MatrixOrder noncomputable section @@ -42,6 +43,20 @@ symmetric plus nonnegative quadratic form. -/ def IsPSDMatrix {n : Nat} (A : Matrix (Fin n) (Fin n) Real) : Prop := IsSymmetricMatrix A /\ forall x : Fin n -> Real, 0 <= matrixQuadraticForm A x +/-- HighDimProb's explicit real PSD predicate implies Mathlib's +`Matrix.PosSemidef` predicate. -/ +theorem posSemidef_of_isPSDMatrix {n : Nat} + {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) : + A.PosSemidef := by + classical + refine ⟨?_, ?_⟩ + · apply Matrix.IsHermitian.ext + intro i j + simpa using isSymmetricMatrix_apply hA.1 i j + · intro x + have hquad := hA.2 (fun i : Fin n => x i) + simpa [matrixQuadraticForm, Finsupp.sum_fintype] using hquad + /-- Pointwise PSD random square matrix. -/ def RandomPSDMatrix {Omega : Type*} [MeasurableSpace Omega] {n : Nat} (_P : Measure Omega) (A : RandomMatrix Omega n n) : Prop := @@ -87,6 +102,21 @@ theorem randomPSDMatrix_rankOneRandomMatrix {Omega : Type*} def MatrixLE {n : Nat} (A B : Matrix (Fin n) (Fin n) Real) : Prop := IsPSDMatrix (B - A) +/-- HighDimProb's explicit PSD predicate gives nonnegativity in Mathlib's +scoped matrix Loewner order. -/ +theorem matrix_nonneg_of_isPSDMatrix {n : Nat} + {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) : + (0 : Matrix (Fin n) (Fin n) Real) <= A := + Matrix.PosSemidef.nonneg (posSemidef_of_isPSDMatrix hA) + +/-- HighDimProb's explicit `MatrixLE` predicate gives Mathlib's scoped matrix +Loewner order. -/ +theorem matrix_le_of_matrixLE {n : Nat} + {A B : Matrix (Fin n) (Fin n) Real} (hAB : MatrixLE A B) : + A <= B := by + rw [Matrix.le_iff] + exact posSemidef_of_isPSDMatrix hAB + theorem matrixQuadraticForm_sub {n : Nat} (B A : Matrix (Fin n) (Fin n) Real) (x : Fin n -> Real) : matrixQuadraticForm (B - A) x = diff --git a/HighDimProb/RandomMatrix/Spectral.lean b/HighDimProb/RandomMatrix/Spectral.lean index 18b9f06..fb9bd4f 100644 --- a/HighDimProb/RandomMatrix/Spectral.lean +++ b/HighDimProb/RandomMatrix/Spectral.lean @@ -380,25 +380,6 @@ theorem matrixQuadraticForm_nonneg_of_posSemidef {n : Nat} simpa [matrixQuadraticForm, dotProduct, Matrix.mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc] using h -/-- HighDimProb's explicit PSD predicate gives Mathlib positive -semidefiniteness. - -Formula reference: positive semidefinite real matrices are characterized by a -nonnegative quadratic form; see https://en.wikipedia.org/wiki/Definite_matrix . -This bridge keeps the explicit HighDimProb assumptions visible while exposing -Mathlib's `Matrix.PosSemidef` API. -/ -theorem posSemidef_of_isPSDMatrix {n : Nat} - {A : Matrix (Fin n) (Fin n) Real} (hA : IsPSDMatrix A) : - A.PosSemidef := by - apply Matrix.PosSemidef.of_dotProduct_mulVec_nonneg - · apply Matrix.IsHermitian.ext - intro i j - simpa using Matrix.IsSymm.apply hA.1 i j - · intro x - have hx := hA.2 x - simpa [matrixQuadraticForm, dotProduct, Matrix.mulVec, - Finset.mul_sum, Finset.sum_mul, mul_assoc] using hx - /-- PSD nullspace converse in HighDimProb's explicit quadratic-form vocabulary. Formula reference: for a positive semidefinite matrix, a zero quadratic form @@ -577,6 +558,57 @@ theorem lambdaMaxOrdered_rayleighUpperBound rayleighUpperBound_of_spectralUpperBound (lambdaMaxOrdered_spectralUpperBound hA) +/-- The absolute explicit quadratic form of a unit vector is bounded by the +deterministic L2 operator norm. -/ +theorem abs_matrixQuadraticForm_le_deterministicOperatorNorm {n : Nat} + (A : Matrix (Fin n) (Fin n) Real) {x : Fin n -> Real} + (hx : IsUnitVector x) : + abs (matrixQuadraticForm A x) <= deterministicOperatorNorm A := by + have hxnorm : + norm (WithLp.toLp 2 x : EuclideanSpace Real (Fin n)) = 1 := + norm_toLp_eq_one_of_isUnitVector hx + have hmul := + Matrix.l2_opNorm_mulVec A (WithLp.toLp 2 x : EuclideanSpace Real (Fin n)) + have hmul' : + norm ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) : + EuclideanSpace Real (Fin n)) <= norm A := by + simpa [hxnorm] using hmul + have hinner : + matrixQuadraticForm A x = + inner Real + ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) : + EuclideanSpace Real (Fin n)) + (WithLp.toLp 2 x : EuclideanSpace Real (Fin n)) := by + simp [matrixQuadraticForm, Matrix.mulVec, dotProduct, inner, mul_assoc] + apply Finset.sum_congr rfl + intro i _ + rw [← Finset.mul_sum] + calc + abs (matrixQuadraticForm A x) + = abs (inner Real + ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) : + EuclideanSpace Real (Fin n)) + (WithLp.toLp 2 x : EuclideanSpace Real (Fin n))) := by rw [hinner] + _ <= norm ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) : + EuclideanSpace Real (Fin n)) * + norm (WithLp.toLp 2 x : EuclideanSpace Real (Fin n)) := + abs_real_inner_le_norm _ _ + _ = norm ((EuclideanSpace.equiv (Fin n) Real).symm (Matrix.mulVec A x) : + EuclideanSpace Real (Fin n)) * 1 := by rw [hxnorm] + _ <= norm A * 1 := by + exact mul_le_mul_of_nonneg_right hmul' zero_le_one + _ = deterministicOperatorNorm A := by + simp [deterministicOperatorNorm] + +/-- The explicit quadratic form of a unit vector is bounded above by the +deterministic L2 operator norm. -/ +theorem matrixQuadraticForm_le_deterministicOperatorNorm {n : Nat} + (A : Matrix (Fin n) (Fin n) Real) {x : Fin n -> Real} + (hx : IsUnitVector x) : + matrixQuadraticForm A x <= deterministicOperatorNorm A := + (le_abs_self (matrixQuadraticForm A x)).trans + (abs_matrixQuadraticForm_le_deterministicOperatorNorm A hx) + /-- The ordered lambda-max endpoint is attained by an explicit unit eigenvector in HighDimProb's quadratic-form convention. -/ private theorem exists_unitVector_matrixQuadraticForm_eq_lambdaMaxOrdered diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index 928e4b7..f34459e 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean @@ -129,6 +129,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_statement #check HighDimProb.deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_of_normMono +#check HighDimProb.deterministicMatrixVarianceProxyNorm_mono_of_matrixLE #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain #check HighDimProb.varianceProxyNormBound_of_centeredSquareChain_expansion #check HighDimProb.traceMatrixExp_le_rank_exp_lambdaMax_statement diff --git a/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean b/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean index b6fda6e..b8db47a 100644 --- a/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean +++ b/HighDimProbJudge/RandomMatrix/VarianceProxyUse.lean @@ -58,6 +58,9 @@ import HighDimProb.RandomMatrix #check HighDimProb.matrixLE_add_left #check HighDimProb.matrixLE_add_right #check HighDimProb.matrixLE_smul_of_nonneg +#check HighDimProb.posSemidef_of_isPSDMatrix +#check HighDimProb.matrix_nonneg_of_isPSDMatrix +#check HighDimProb.matrix_le_of_matrixLE #check HighDimProb.isSelfAdjointMatrix_matrixSquare_of_isSelfAdjointMatrix #check HighDimProb.matrixQuadraticForm_matrixSquare_eq_matVecSqNorm_of_selfAdjoint #check HighDimProb.isPSD_matrixSquare_of_selfAdjoint diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index adbdb80..f7240f5 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean @@ -56,6 +56,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega) #check varianceProxyNormBound_of_centeredSquareChain_statement #check deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement #check varianceProxyNormBound_of_centeredSquareChain_of_normMono +#check deterministicMatrixVarianceProxyNorm_mono_of_matrixLE #check traceMatrixExp_le_rank_exp_lambdaMax_statement #check traceMatrixExp_le_supportDim_exp_lambdaMax_statement #check matrixExpSupportDomination_identity_statement diff --git a/HighDimProbTest/RandomMatrixVarianceProxyAPI.lean b/HighDimProbTest/RandomMatrixVarianceProxyAPI.lean index 6f81172..a444f1d 100644 --- a/HighDimProbTest/RandomMatrixVarianceProxyAPI.lean +++ b/HighDimProbTest/RandomMatrixVarianceProxyAPI.lean @@ -69,6 +69,9 @@ variable (hRnonneg : 0 <= R) #check matrixLE_add_left #check matrixLE_add_right #check matrixLE_smul_of_nonneg +#check posSemidef_of_isPSDMatrix +#check matrix_nonneg_of_isPSDMatrix +#check matrix_le_of_matrixLE #check randomMatrixSquare #check randomMatrixSquare_apply #check randomMatrixSquare_neg diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index e5c5b7e..b182f2d 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -65,8 +65,9 @@ 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, centered-square provider/norm-monotonicity contract APIs, and - remaining typed statement APIs. + bridge, centered-square provider/norm-monotonicity contract APIs including + `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`, 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, diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index def7ad3..b31a78c 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -123,6 +123,7 @@ Variance-proxy / centered-square chain: - `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two` - `varianceProxyNormBound_of_centeredSquareChain_statement` - `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` +- `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE` - `varianceProxyNormBound_of_centeredSquareChain_of_normMono` - `varianceProxyNormBound_of_centeredSquareChain_expansion` @@ -174,7 +175,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`, `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 | +| Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement`, `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement`, `matrixSquare_centeredRandomMatrix_expectation_expansion_statement`, `centeredRankOneSquare_le_rankOneSecondMoment_statement` | centered-square expectation expansion, finite-sum MatrixLE bookkeeping, PSD Loewner-to-operator-norm monotonicity, and centered rank-one second-moment comparison proved; typed-prop chain has proved thin consumers | `matrixSquare_centeredRandomMatrix_expectation_expansion`, `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment`, `centeredRankOneSquare_le_rankOneSecondMoment`, `varianceProxyNormBound_of_centeredSquareChain`, `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`, `varianceProxyNormBound_of_centeredSquareChain_of_normMono`, `varianceProxyNormBound_of_centeredSquareChain_expansion`, `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSecondMoment`, `deterministicMatrixVarianceProxyNorm_sum_le_sum`, `deterministicMatrixVarianceProxyNorm_matrixSecondMoment_rankOneRandomMatrix_le_sq_of_sqNorm_bound`, `deterministicMatrixVarianceProxyNorm_sum_matrixSecondMoment_rankOneRandomMatrix_le_sum_sq_of_sqNorm_bound`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_two`, `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChain`, `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 explicit at the call sites; the deterministic PSD norm-monotonicity provider is proved, while wrappers/bundles still require Tropp/Lieb, centered-square comparisons, 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 | diff --git a/docs/Status.md b/docs/Status.md index 3ecacc9..3d119ea 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -119,6 +119,7 @@ Hardbone proved leaves, deterministic bridges, statement targets, and thin consu - `matrixSquare_centeredRandomMatrix_expectation_expansion` - `matrixLE_sum` - `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` +- `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE` - `varianceProxyNormBound_of_centeredSquareChain_of_normMono` - `varianceProxyNormBound_of_centeredSquareChain_expansion` - `matrixTrace_smul` @@ -219,13 +220,14 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact variance-proxy norm theorem. The variance-proxy provider-chain consumer is 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 + `varianceProxyNormBound_of_centeredSquareChain_of_normMono` proves the + finite-sum Loewner bookkeeping with `matrixLE_sum`, and the deterministic + PSD Loewner-to-operator-norm bridge is now proved as + `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`. 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 + comparison and deterministic norm-control assumptions at the wrapper boundary. + 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 diff --git a/docs/TODO.md b/docs/TODO.md index bfdfafc..3211ce7 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -17,9 +17,10 @@ This is the active short list. Old completed task logs were collapsed into Matrix Bernstein proofs. - Prefer shared RandomMatrix APIs over unfolded formulas in examples, tests, judge files, and docs. -- Current RandomMatrix hardbone branch: centered-square provider contract - `RM-VP-centered-square-chain-provider-contract`, splitting finite-sum - Loewner bookkeeping from the remaining norm-monotonicity blocker. +- Current RandomMatrix hardbone branch: PSD Loewner operator-norm monotonicity + `RM-VP-psd-loewner-operator-norm-monotonicity-contract`, discharging the + deterministic norm-monotonicity provider while leaving Tropp/Lieb, trace-MGF, + and centered-square comparison assumptions explicit. - The centered-square-chain wrapper variants are available for both the positive-side quadratic-form route and the two-sided/operator-norm route; natural assumption bundles now package those exact-row routes without diff --git a/docs/TestPlan.md b/docs/TestPlan.md index e81c835..b88d07e 100644 --- a/docs/TestPlan.md +++ b/docs/TestPlan.md @@ -57,8 +57,9 @@ git diff --check second-moment norm providers, the rank-one square-integrability four-product, `MemLp 4`, bounded-row, centered-family providers, the row-specific exact-row sample-covariance hardbone consumer, the finite-sum `matrixLE_sum` order - helper, the explicit norm-monotonicity blocker surface, and the - generic-centered-square-chain exact-row bridge in + helper, the proved PSD Loewner norm-monotonicity provider, the explicit + norm-monotonicity statement surface, and the generic-centered-square-chain + exact-row bridge in `RandomMatrixVarianceProxyAPI`, `RandomMatrixHardboneStatementsAPI`, and the corresponding judge/example surfaces. diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index a71b00c..24c1f96 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -56,11 +56,11 @@ variance-proxy centered-square-chain consumers `varianceProxyNormBound_of_centeredSquareChain_of_normMono`, and `varianceProxyNormBound_of_centeredSquareChain_expansion` are proved. The `of_normMono` route proves the finite-sum Loewner bookkeeping via -`matrixLE_sum`, but keeps Loewner-to-operator-norm monotonicity as the explicit -`deterministicMatrixVarianceProxyNorm_mono_of_matrixLE_statement` blocker; the -expansion route removes the explicit expansion premise but still requires -Loewner comparison and deterministic norm-control assumptions. The centered rank-one second-moment -comparison is proved by `centeredRankOneSquare_le_rankOneSecondMoment`, using +`matrixLE_sum`; the deterministic PSD Loewner-to-operator-norm bridge is proved +as `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`. The expansion route +removes the explicit expansion premise but still requires Loewner comparison +and deterministic norm-control assumptions at the wrapper boundary. The centered +rank-one second-moment comparison is proved by `centeredRankOneSquare_le_rankOneSecondMoment`, using `matrixSecondMoment_centeredRandomMatrix_le_matrixSecondMoment` and `matrixLE_sub_right_of_isPSD`. The sample-covariance consumer `sampleCovarianceVarianceProxy_sharp_of_rankOneSecondMoment` supplies that