Prove trace-exp rank/support hardbone leaf

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

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

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

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

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,

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

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.

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.