From c215c12b456aeb976515d59ed190caf162f55771 Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Fri, 19 Jun 2026 07:36:00 +0000 Subject: [PATCH] Discharge the explicit rank/support trace-exp leaf Prove the local trace-exponential dimension-factor bounds from explicit support certificates and expose the witnesses through API, judge, example, and status docs without broadening the hardbone boundary. Constraint: Keep Tropp/Lieb, Golden-Thompson, trace-exp integrability, variance-proxy, support construction, effective-rank, full Matrix Bernstein, and unconditional concentration outside this leaf. Rejected: Cherry-picking later worker auto-checkpoints | they duplicated the leader-integrated proof/coverage and conflicted after canonical validation. Confidence: high Scope-risk: narrow Directive: Treat these theorems as support-certificate consumers only; do not cite them as support construction or effective-rank proofs. Tested: lake build HighDimProb.RandomMatrix.HardboneStatements; lake env lean HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean; lake env lean HighDimProbJudge/RandomMatrix/TraceExpUse.lean; lake env lean HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean; lake build HighDimProbJudge; lake build HighDimProb.Examples; lake test; lake build; python scripts/judge_policy_check.py; python .github/scripts/check_text_quality.py; git diff --check Not-tested: GitHub PR checks; PR creation/push intentionally not performed. --- .../HardboneStatementAtlasUsage.lean | 14 ++++ .../RandomMatrix/HardboneStatements.lean | 66 +++++++++++++++++++ .../RandomMatrix/TraceExpUse.lean | 2 + .../RandomMatrixHardboneStatementsAPI.lean | 16 +++++ docs/RandomMatrixAPI.md | 14 ++-- docs/Status.md | 19 ++++-- docs/TestPlan.md | 2 +- docs/TheoremAtlas.md | 12 ++-- 8 files changed, 131 insertions(+), 14 deletions(-) diff --git a/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean b/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean index 1e037cc..50603cd 100644 --- a/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean +++ b/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean @@ -89,4 +89,18 @@ example {n : Nat} (A support : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) (rankBound : Nat) : Prop := traceMatrixExp_le_rank_exp_lambdaMax_statement A support rankBound +example {n : Nat} (A support : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) + (supportDim : Nat) : Prop := + traceMatrixExp_le_supportDim_exp_lambdaMax_statement A support supportDim + +example {n : Nat} (A support : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) + (rankBound : Nat) : + traceMatrixExp_le_rank_exp_lambdaMax_statement A support rankBound := + traceMatrixExp_le_rank_exp_lambdaMax A support rankBound + +example {n : Nat} (A support : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) + (supportDim : Nat) : + traceMatrixExp_le_supportDim_exp_lambdaMax_statement A support supportDim := + traceMatrixExp_le_supportDim_exp_lambdaMax A support supportDim + end HighDimProb.Examples.RandomMatrix.HardboneStatementAtlasUsage diff --git a/HighDimProb/RandomMatrix/HardboneStatements.lean b/HighDimProb/RandomMatrix/HardboneStatements.lean index ab29cf2..82b89a3 100644 --- a/HighDimProb/RandomMatrix/HardboneStatements.lean +++ b/HighDimProb/RandomMatrix/HardboneStatements.lean @@ -537,6 +537,72 @@ abbrev traceMatrixExp_le_supportDim_exp_lambdaMax_statement {n : Nat} traceMatrixExp A <= (supportDim : Real) * Real.exp (lambdaMaxOrdered A hA) +/-- Proved rank-refined trace-exponential bound from an explicit support +certificate. + +This is a local support-certificate leaf: it only converts the explicit +Loewner support comparison into a trace bound. It does not construct the +support certificate or prove an effective-rank theorem. -/ +theorem traceMatrixExp_le_rank_exp_lambdaMax {n : Nat} + (A support : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) + (rankBound : Nat) : + traceMatrixExp_le_rank_exp_lambdaMax_statement A support rankBound := by + intro _hRankPos _hRankLe _hSupportPSD hTraceSupport hA hSupport + unfold traceMatrixExp + unfold MatrixLE at hSupport + have hTraceDiffNonneg : + 0 <= matrixTrace + ((Real.exp (lambdaMaxOrdered A hA) • support) - matrixExp A) := by + exact matrixTrace_nonneg_of_posSemidef + (posSemidef_of_isPSDMatrix hSupport) + unfold matrixTrace at hTraceDiffNonneg hTraceSupport ⊢ + have hTraceLe : + Matrix.trace (matrixExp A) <= + Matrix.trace (Real.exp (lambdaMaxOrdered A hA) • support) := by + rw [Matrix.trace_sub] at hTraceDiffNonneg + linarith + calc + Matrix.trace (matrixExp A) + <= Matrix.trace (Real.exp (lambdaMaxOrdered A hA) • support) := hTraceLe + _ = Real.exp (lambdaMaxOrdered A hA) * Matrix.trace support := by + simp [Matrix.trace_smul] + _ <= Real.exp (lambdaMaxOrdered A hA) * (rankBound : Real) := by + exact mul_le_mul_of_nonneg_left hTraceSupport (Real.exp_nonneg _) + _ = (rankBound : Real) * Real.exp (lambdaMaxOrdered A hA) := by ring + +/-- Proved support-dimension trace-exponential bound from an explicit support +certificate. + +This is the same support-certificate leaf as +`traceMatrixExp_le_rank_exp_lambdaMax`, with the dimension parameter named for +the support-dimension formulation. -/ +theorem traceMatrixExp_le_supportDim_exp_lambdaMax {n : Nat} + (A support : Matrix (Fin (n + 1)) (Fin (n + 1)) Real) + (supportDim : Nat) : + traceMatrixExp_le_supportDim_exp_lambdaMax_statement A support supportDim := by + intro _hDimPos _hDimLe _hSupportPSD hTraceSupport hA hSupport + unfold traceMatrixExp + unfold MatrixLE at hSupport + have hTraceDiffNonneg : + 0 <= matrixTrace + ((Real.exp (lambdaMaxOrdered A hA) • support) - matrixExp A) := by + exact matrixTrace_nonneg_of_posSemidef + (posSemidef_of_isPSDMatrix hSupport) + unfold matrixTrace at hTraceDiffNonneg hTraceSupport ⊢ + have hTraceLe : + Matrix.trace (matrixExp A) <= + Matrix.trace (Real.exp (lambdaMaxOrdered A hA) • support) := by + rw [Matrix.trace_sub] at hTraceDiffNonneg + linarith + calc + Matrix.trace (matrixExp A) + <= Matrix.trace (Real.exp (lambdaMaxOrdered A hA) • support) := hTraceLe + _ = Real.exp (lambdaMaxOrdered A hA) * Matrix.trace support := by + simp [Matrix.trace_smul] + _ <= Real.exp (lambdaMaxOrdered A hA) * (supportDim : Real) := by + exact mul_le_mul_of_nonneg_left hTraceSupport (Real.exp_nonneg _) + _ = (supportDim : Real) * Real.exp (lambdaMaxOrdered A hA) := by ring + /-- Effective-rank trace-exponential target for variance-proxy style matrices. The local assumption `matrixTrace V <= effectiveRank * sigmaSq` records the diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index dd0bb70..c6923e6 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean @@ -115,6 +115,8 @@ open scoped MatrixOrder Matrix.Norms.Operator #check HighDimProb.traceMatrixExp_le_rank_exp_lambdaMax_statement #check HighDimProb.traceMatrixExp_le_supportDim_exp_lambdaMax_statement #check HighDimProb.traceMatrixExp_effectiveRank_bound_statement +#check HighDimProb.traceMatrixExp_le_rank_exp_lambdaMax +#check HighDimProb.traceMatrixExp_le_supportDim_exp_lambdaMax #check HighDimProb.bernsteinMatrixExp_le_quadratic_of_cfcChain #check HighDimProb.selfAdjointSpectrumBoundedByOperatorNorm #check HighDimProb.bernsteinCFCExpressionNormalization diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index 95686d5..19cef48 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean @@ -48,6 +48,8 @@ variable (mHist : Fin m -> MeasurableSpace Omega) #check traceMatrixExp_le_rank_exp_lambdaMax_statement #check traceMatrixExp_le_supportDim_exp_lambdaMax_statement #check traceMatrixExp_effectiveRank_bound_statement +#check traceMatrixExp_le_rank_exp_lambdaMax +#check traceMatrixExp_le_supportDim_exp_lambdaMax #check bernsteinMatrixExp_le_quadratic_of_cfcChain #check selfAdjointSpectrumBoundedByOperatorNorm #check bernsteinCFCExpressionNormalization @@ -114,3 +116,17 @@ example : example : bernsteinMatrixExp_le_quadratic_statement A theta R := bernsteinMatrixExp_le_quadratic A theta R + +-- Proved rank/support trace-exp leaves: the statement targets now have +-- theorem witnesses, but they do not discharge effective-rank or Tropp/Lieb +-- matrix concentration claims. +#check @traceMatrixExp_le_rank_exp_lambdaMax +#check @traceMatrixExp_le_supportDim_exp_lambdaMax + +example : + traceMatrixExp_le_rank_exp_lambdaMax_statement B S rankBound := + traceMatrixExp_le_rank_exp_lambdaMax B S rankBound + +example : + traceMatrixExp_le_supportDim_exp_lambdaMax_statement B S supportDim := + traceMatrixExp_le_supportDim_exp_lambdaMax B S supportDim diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index f0bcfd9..fbaaae2 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -110,6 +110,8 @@ Dimension / rank / effective-rank chain: - `traceMatrixExp_le_rank_exp_lambdaMax_statement` - `traceMatrixExp_le_supportDim_exp_lambdaMax_statement` - `traceMatrixExp_effectiveRank_bound_statement` +- `traceMatrixExp_le_rank_exp_lambdaMax` +- `traceMatrixExp_le_supportDim_exp_lambdaMax` Thin hardbone consumers: @@ -131,15 +133,19 @@ Hardbone status table: | Conditioning / independence | `troppConditionalStep_of_iIndepFun_statement` | typed-prop | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | generated histories, history-step independence, conditional expectation reduction | | Trace-exp integrability | `traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement` | typed-prop | none yet | absolute domination, Golden-Thompson/product, or boundedness provider | | Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement` | typed-prop | none yet | centered-square expansion, rank-one comparison, order/norm bookkeeping | -| Dimension / support / effective rank | `traceMatrixExp_effectiveRank_bound_statement` | typed-prop | none yet | rank/support/effective-rank core theory | +| Rank/support trace-exp dimension factor | `traceMatrixExp_le_rank_exp_lambdaMax_statement`, `traceMatrixExp_le_supportDim_exp_lambdaMax_statement` | proven by `traceMatrixExp_le_rank_exp_lambdaMax`, `traceMatrixExp_le_supportDim_exp_lambdaMax` | public API/test/judge/example checks | support certificate remains explicit; no support construction or effective-rank theorem is claimed | +| Effective-rank trace-exp refinement | `traceMatrixExp_effectiveRank_bound_statement` | typed-prop | none yet | effective-rank core theory and variance-proxy support bookkeeping | | Thin consumers | `troppMasterTraceMGFConditionalStep_of_conditioningBridge` | proven | public API/test/judge/example checks | thin wrapper only; no hard fact is discharged | Most hardbone declarations are typed `Prop` contracts, not hard theorem proofs. The Bernstein CFC chain is now proved by `bernsteinMatrixExp_le_quadratic` after splitting out scalar Bernstein, spectrum localization, CFC order -transfer, and expression normalization. The remaining log/order, Tropp/Lieb, -conditioning, integrability, variance-proxy, and dimension/rank blockers stay -split into named leaves. The rank and effective-rank trace-exp +transfer, and expression normalization. The local rank/support trace-exp +dimension-factor leaf is proved from an explicit support certificate by +`traceMatrixExp_le_rank_exp_lambdaMax` and +`traceMatrixExp_le_supportDim_exp_lambdaMax`. The remaining log/order, +Tropp/Lieb, conditioning, integrability, variance-proxy, and effective-rank +blockers stay split into named leaves. The rank and effective-rank trace-exp targets keep support or ambient-identity terms explicit, so zero directions are not accidentally treated as free. The thin consumers only apply explicit statement-chain assumptions; they do not prove Lieb/Jensen, conditioning, diff --git a/docs/Status.md b/docs/Status.md index ab5c807..e97d73c 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -86,6 +86,11 @@ Hardbone Bernstein CFC leaf: - `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` - `bernsteinMatrixExp_le_quadratic` +Hardbone rank/support trace-exp leaf: + +- `traceMatrixExp_le_rank_exp_lambdaMax` +- `traceMatrixExp_le_supportDim_exp_lambdaMax` + Example-layer wrappers: - `sampleCovariance_quadraticForm_tail_usage` @@ -110,11 +115,15 @@ Example modules: - RandomMatrix / Matrix Bernstein remains experimental. - The hardbone statement atlas names CFC, log/order, Tropp/Lieb, - conditioning, integrability, variance-proxy, and dimension/rank blockers as - typed statement targets. The Bernstein CFC route is now proved through - `bernsteinMatrixExp_le_quadratic`, reusing scalar Bernstein, spectrum - localization, Bernstein-specific CFC order transfer, and CFC expression - normalization. The preferred optimized Matrix Bernstein assumption bundles + conditioning, integrability, variance-proxy, and dimension/rank blockers. The + Bernstein CFC route is now proved through `bernsteinMatrixExp_le_quadratic`, + reusing scalar Bernstein, spectrum localization, Bernstein-specific CFC order + transfer, and CFC expression normalization. The local rank/support trace-exp + dimension-factor route is proved through + `traceMatrixExp_le_rank_exp_lambdaMax` and + `traceMatrixExp_le_supportDim_exp_lambdaMax` from an explicit support + certificate; it does not construct support certificates or prove the + effective-rank target. The preferred optimized Matrix Bernstein assumption bundles are now `MatrixBernsteinPositiveSideTroppAssumptions` and `MatrixBernsteinNegativeSideTroppAssumptions`, which expose Tropp/Lieb primitives but not pointwise CFC fields. The older explicit-CFC bundles and diff --git a/docs/TestPlan.md b/docs/TestPlan.md index 9d51701..7413786 100644 --- a/docs/TestPlan.md +++ b/docs/TestPlan.md @@ -34,7 +34,7 @@ git diff --check `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`; example modules are covered through `lake build HighDimProb.Examples`. - RandomMatrix hardbone statement-target checks, including the proved Bernstein - CFC hardbone leaf, are covered in + CFC hardbone leaf and the rank/support trace-exp leaf, are covered in `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`, `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`, and the `HardboneStatementAtlasUsage` example. diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 5f1dc87..3f1c6b1 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -39,8 +39,12 @@ variance-proxy, and dimension/rank blockers as `typed-prop` targets. Selected consumer wrappers are proven thin applications of those targets; they do not close the hard theorem families. The Bernstein CFC route is now proved as `bernsteinMatrixExp_le_quadratic`, via scalar Bernstein, spectrum localization, -Bernstein-specific CFC order transfer, and expression normalization. The -trace-MGF provider surface includes +Bernstein-specific CFC order transfer, and expression normalization. The local +rank/support trace-exp dimension-factor route is now proved by +`traceMatrixExp_le_rank_exp_lambdaMax` and +`traceMatrixExp_le_supportDim_exp_lambdaMax` from an explicit support +certificate; it does not construct that certificate or prove the effective-rank +refinement. The trace-MGF provider surface includes `matrixBernsteinTraceMGFWithBernsteinCoeff_under_troppPrimitive`, which reuses that CFC proof while keeping Tropp/Lieb and integrability assumptions explicit. The preferred optimized Matrix Bernstein wrappers use @@ -59,8 +63,8 @@ assumptions explicit. - Natural history measurability, independence conditioning, and trace-exp integrability propagation for the conditional-step Tropp route. - Proofs of the remaining hardbone statement targets for log/order, - Tropp/Lieb, conditioning, integrability, variance-proxy sharpening, and - dimension/rank refinements. + Tropp/Lieb, conditioning, integrability, variance-proxy sharpening, + support construction, and effective-rank refinements. - A public-friendly Matrix Bernstein wrapper directly over the natural-state route.