Package S10 tail assumptions for reusable callers

HighDimProb/RandomMatrix/ConcentrationStatements.lean

@@ -5163,6 +5163,110 @@ abbrev matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement
                 ENNReal.ofReal
                   (traceMatrixExp (SMul.smul (bernsteinMGFCoeff theta R) V))
 
+/-- Named assumption bundle for the S10 conditioning trace-MGF to tail route.
+
+This structure packages exactly the explicit S9 conditioning trace-MGF premises
+and the two tail-side bridge premises consumed by
+`matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge`. It is an
+assumption contract only: it does not prove conditioning, tail domination,
+integrability propagation, variance-proxy control, or an unconditional Matrix
+Bernstein theorem. -/
+structure MatrixBernsteinConditioningTraceMGFTailAssumptions
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P] {m n : Nat}
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (V : Matrix (Fin n) (Fin n) Real)
+    (theta R t : Real)
+    (mHist : Fin m -> MeasurableSpace Omega) : Prop where
+  chain :
+    @troppConditionalStep_of_iIndepFun_statement Omega mOmega P m n
+      theta X K mHist
+  historyMeasurable :
+    @troppNaturalHistoryMeasurable_statement Omega mOmega m n
+      theta X K mHist
+  historyStepIndependent :
+    @troppHistoryStepIndependent_of_iIndepFun_statement Omega mOmega P m n
+      theta X K
+  conditionalExpectation :
+    forall i,
+      @condExp_traceExp_history_add_independent_step_statement
+        Omega mOmega P n
+        (mHist i) (@troppStateHistory Omega mOmega m n theta X K i)
+        (@troppCurrentRandomStep Omega mOmega m n theta X i) (K i)
+  historySub : forall i, mHist i <= mOmega
+  historyRandom :
+    forall i,
+      @IsRandomMatrix Omega mOmega n n P
+        (troppStateHistory theta X K i)
+  stepRandom :
+    forall i,
+      @IsRandomMatrix Omega mOmega n n P
+        (troppCurrentRandomStep theta X i)
+  historySelfAdjoint :
+    forall i omega, IsSelfAdjointMatrix (troppStateHistory theta X K i omega)
+  stepSelfAdjoint :
+    forall i,
+      @RandomSelfAdjointMatrix Omega mOmega n P
+        (troppCurrentRandomStep theta X i)
+  conditionalTraceIntegrable :
+    forall i,
+      @IntegrableRealRandomVariable Omega mOmega P
+        (fun omega =>
+          traceMatrixExp
+            (troppStateHistory theta X K i omega +
+              troppCurrentRandomStep theta X i omega))
+  stepExpIntegrable :
+    forall i,
+      @IntegrableRandomMatrix Omega mOmega n n P
+        (fun omega => matrixExp (troppCurrentRandomStep theta X i omega))
+  expMeanSelfAdjoint :
+    forall i,
+      IsSelfAdjointMatrix
+        (@matrixExpect Omega mOmega n n P
+          (fun omega => matrixExp (troppCurrentRandomStep theta X i omega)))
+  expMeanStrictlyPositive :
+    forall i,
+      IsStrictlyPositive
+        (@matrixExpect Omega mOmega n n P
+          (fun omega => matrixExp (troppCurrentRandomStep theta X i omega)))
+  sigmaFiniteHistory : forall i, SigmaFinite (P.trim (historySub i))
+  rhsTraceIntegrable :
+    forall i,
+      @IntegrableRealRandomVariable Omega mOmega P
+        (fun omega =>
+          traceMatrixExp (troppStateHistory theta X K i omega + K i))
+  randomMatrix : forall i, IsRandomMatrix P (X i)
+  selfAdjoint : forall i, RandomSelfAdjointMatrix P (X i)
+  independent : ProbabilityTheory.iIndepFun X P
+  expIntegrable :
+    forall i,
+      IntegrableRandomMatrix P
+        (fun omega => matrixExp (SMul.smul theta (X i omega)))
+  traceIntegrable :
+    IntegrableRealRandomVariable P
+      (traceExpIntegrand (randomMatrixSum X) theta)
+  comparisonSelfAdjoint : forall i, IsSelfAdjointMatrix (K i)
+  varianceProxySelfAdjoint : IsSelfAdjointMatrix V
+  radiusNonneg : 0 <= R
+  thetaRange : abs theta * R < 3
+  mgfComparison :
+    forall i,
+      MatrixLE
+        (matrixExpect P
+          (fun omega => matrixExp (SMul.smul theta (X i omega))))
+        (matrixExp (K i))
+  varianceProxyNormalization :
+    Finset.univ.sum (fun i : Fin m => K i) =
+      SMul.smul (bernsteinMGFCoeff theta R) V
+  tailAEMeasurable :
+    AEMeasurable
+      (fun omega => ENNReal.ofReal
+        (traceExpIntegrand (randomMatrixSum X) theta omega)) P
+  tailEventSubset :
+    quadraticFormUpperTailEvent (randomMatrixSum X) t ⊆
+      traceExpThresholdEvent (randomMatrixSum X) theta t
+
 /-- Progress-first composition from the S9 conditioning trace-MGF bridge to the
 quadratic-form Laplace/tail bound.
 
@@ -5291,6 +5395,38 @@ theorem matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge
     quadraticFormUpperTail_laplace_bound_of_traceMGFBernsteinVarianceProxyBoundLIntegral
       (randomMatrixSum X) V theta t R hTailMeas hTailSubset hLInt
 
+/-- Bundle-based S10 wrapper for the conditioning trace-MGF to tail route.
+
+This is only a field-access wrapper around
+`matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge`; the
+bundle name records that the assumptions are still tail/conditioning premises,
+not a full or unconditional Matrix Bernstein theorem. -/
+theorem matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : Measure Omega} [IsProbabilityMeasure P] {m n : Nat}
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (V : Matrix (Fin n) (Fin n) Real)
+    (theta R t : Real)
+    (mHist : Fin m -> MeasurableSpace Omega)
+    (h : MatrixBernsteinConditioningTraceMGFTailAssumptions
+      (P := P) X K V theta R t mHist) :
+    P (quadraticFormUpperTailEvent (randomMatrixSum X) t) <=
+      ENNReal.ofReal (Real.exp (-(theta * t))) *
+        ENNReal.ofReal
+          (traceMatrixExp (SMul.smul (bernsteinMGFCoeff theta R) V)) := by
+  exact
+    matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge
+      X K V theta R t mHist
+      h.chain h.historyMeasurable h.historyStepIndependent
+      h.conditionalExpectation h.historySub h.historyRandom h.stepRandom
+      h.historySelfAdjoint h.stepSelfAdjoint h.conditionalTraceIntegrable
+      h.stepExpIntegrable h.expMeanSelfAdjoint h.expMeanStrictlyPositive
+      h.sigmaFiniteHistory h.rhsTraceIntegrable h.randomMatrix h.selfAdjoint
+      h.independent h.expIntegrable h.traceIntegrable h.comparisonSelfAdjoint
+      h.varianceProxySelfAdjoint h.radiusNonneg h.thetaRange h.mgfComparison
+      h.varianceProxyNormalization h.tailAEMeasurable h.tailEventSubset
+
 /-- Typed target for the spectral-radius reduction for self-adjoint matrices.
 
 This records a future bridge between HighDimProb's deterministic L2 operator

HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean

@@ -14,6 +14,8 @@ open HighDimProb
 #check HighDimProb.matrixBernsteinTraceMGFToLaplaceContract_statement
 #check HighDimProb.matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement
 #check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge
+#check HighDimProb.MatrixBernsteinConditioningTraceMGFTailAssumptions
+#check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions
 #check HighDimProb.matrixBernsteinQuadraticFormUpperTailWithBernsteinCoeff_under_primitives
 #check HighDimProb.traceMatrixExp_bernsteinMGFCoeff_matrixVarianceProxy_le_card_exp
 #check HighDimProb.matrixBernsteinQuadraticFormUpperTailScalarRHSWithBernsteinCoeff_under_primitives

HighDimProbTest/RandomMatrixConcentrationAPI.lean

@@ -119,6 +119,8 @@ variable (R theta sigma2 c c1 c2 t bound K : Real)
 #check matrixBernsteinTraceMGFWithBernsteinCoeff_negRandomMatrixFamily
 #check matrixBernsteinTraceMGFWithBernsteinCoeff_under_primitives
 #check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge
+#check HighDimProb.MatrixBernsteinConditioningTraceMGFTailAssumptions
+#check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions
 #check matrixBernsteinTraceMGFWithBernsteinCoeff_under_troppPrimitive
 #check matrixBernsteinTraceMGFToLaplaceContract_statement
 #check matrixBernsteinTraceMGFToLaplaceContract_under_primitives_statement

docs/README.md

@@ -1,6 +1,6 @@
 # Documentation
 
-The Lean source, tests, judge files, and root `README.md` are the source of truth. This directory is intentionally small-facing: it gives route maps, current status, and contribution policy, not a duplicate theorem database.
+The Lean source, tests, judge files, and root `README.md` are the source of truth. This directory is intentionally user-facing: it gives route maps, current status, and contribution policy, not a duplicate theorem database.
 
 Start here:
 
@@ -9,7 +9,7 @@ Start here:
 - `RandomMatrixAPI.md`: RandomMatrix and Matrix Bernstein public names.
 - `TermMap.md`: compact concept-to-source map.
 - `TheoremAtlas.md`: theorem-family status without full signatures.
-- `STATEMENTS.md`: explicit hard assumptions consumed by progress-first contracts.
+- `STATEMENTS.md`: developer-facing hardbone statement ledger for provider targets.
 - `TestPlan.md`: checks contributors should run.
 - `Workflow.md`: contribution and cleanup rules.
 - `TODO.md`: short active task list.
@@ -24,4 +24,10 @@ Developer references:
 - `BookProgress.md`: short milestone index.
 - `archive.md`: why old detailed docs were removed; use git history for exact old wording.
 
-Avoid adding new long progress logs. Put stable API facts in source/docs, proof-frontier evidence in `external/validation`, and usage demonstrations in examples.
+Avoid adding new long progress logs. Put stable API facts in source/docs, proof-frontier evidence in `external/validation`, and usage demonstrations in examples.
+
+`STATEMENTS.md` is the exception to the user-facing rule: it is a developer
+ledger for precise hard assumptions that independent provider work is expected
+to discharge later. Downstream users should prefer `APIOverview.md`,
+`RandomMatrixAPI.md`, and examples; names recorded only in `STATEMENTS.md` are
+not promoted as stable caller-facing API.

docs/RandomMatrixAPI.md

@@ -67,6 +67,8 @@ only consumes an explicitly supplied log-back equality.
 - `matrixBernsteinTraceMGFWithBernsteinCoeff_under_troppPrimitive`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`
 - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge`
+- `MatrixBernsteinConditioningTraceMGFTailAssumptions`
+- `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_assumptions`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_troppAssumptions`
 - `matrixBernsteinTwoSidedQuadraticFormTailOptimizedScalarRHSWithBernsteinCoeff_under_primitives`
@@ -83,9 +85,12 @@ public surface is the `*_of_troppAssumptions` family, which uses
 `MatrixBernsteinNegativeSideTroppAssumptions` to expose Tropp/Lieb and
 bookkeeping assumptions without a user-supplied CFC field. The older
 `*_of_assumptions` and `_under_primitives` names remain compatibility surfaces.
-The route still does not prove Tropp/Lieb, Golden-Thompson, trace-exp
-integrability, variance-proxy control, tail event domination, or a full unconditional Matrix
-Bernstein theorem. The conditioning-to-tail wrapper
+The S10 conditioning-to-tail route also exposes
+`MatrixBernsteinConditioningTraceMGFTailAssumptions` and the thin
+`matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions`
+wrapper for reusable assumption passing. The route still does not prove
+Tropp/Lieb, Golden-Thompson, trace-exp integrability, variance-proxy control,
+tail event domination, or a full unconditional Matrix Bernstein theorem. The conditioning-to-tail wrapper
 `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge` is a thin
 composition from the S9 conditioning trace-MGF consumer to the existing
 quadratic-form Laplace route under an explicit tail-event subset assumption.

docs/STATEMENTS.md

@@ -2,7 +2,15 @@
 
 This file lists hard analytic assumptions that progress-first RandomMatrix
 contracts are allowed to consume explicitly while separate provider work fills
-them in.  Entries here are not claims that the assumptions are proved.
+them in. Entries here are not claims that the assumptions are proved.
+
+This is a developer-facing hardbone ledger, not a downstream API reference.
+The strategy is to make hard proof frontiers precise enough that independent
+provider work can discharge them while HighDimProb remains deliverable and
+extensible. Composition theorems recorded here may be useful scaffolds for
+type-checking the route, but they should not be treated as the preferred
+user-facing surface. Once provider theorems are imported, these scaffolds should
+be collapsed, deprecated, or hidden behind smaller stable wrappers.
 
 ## RM-LIEB-S8: Tropp one-step `K` bound from explicit Lieb/log-order inputs
 
@@ -71,7 +79,7 @@ premises:
   full-sum trace-exponential integrability, self-adjoint comparison matrices,
   self-adjoint variance proxy, nonnegative radius, Bernstein theta range,
   per-index MGF Loewner comparison, and the variance-proxy normalization
-  `sum K_i = bernsteinMGFCoeff theta R • V`.
+  `sum K_i = SMul.smul (bernsteinMGFCoeff theta R) V`.
 
 Non-goals for this consumer:
 
@@ -83,9 +91,12 @@ Non-goals for this consumer:
 
 ## RM-LIEB-S10: conditioning trace-MGF to explicit Laplace/tail route
 
-Consumer theorem:
+Consumer theorems:
 
 - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge`
+- `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions`,
+  which is only a field-access wrapper around the named assumption bundle
+  `MatrixBernsteinConditioningTraceMGFTailAssumptions`.
 
 This theorem composes the S9 conditioning trace-MGF consumer with the existing
 quadratic-form Laplace route. It requires all S9 assumptions listed above, plus

docs/Status.md

@@ -59,6 +59,8 @@ Core Matrix Bernstein helpers:
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_assumptions`
 - `matrixBernsteinQuadraticFormUpperTailOptimizedScalarRHSWithBernsteinCoeff_of_troppAssumptions`
 - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge`
+- `MatrixBernsteinConditioningTraceMGFTailAssumptions`
+- `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions`
 - `matrixBernsteinTwoSidedQuadraticFormTailOptimizedScalarRHSWithBernsteinCoeff_of_assumptions`
 - `matrixBernsteinTwoSidedQuadraticFormTailOptimizedScalarRHSWithBernsteinCoeff_of_troppAssumptions`
 - `matrixBernsteinSelfAdjointOperatorNormTailOptimizedScalarRHSWithBernsteinCoeff_arbitrary_of_assumptions`

docs/TODO.md

@@ -25,6 +25,9 @@ This is the active short list. Old completed task logs were collapsed into
   transfer, and PSD Loewner norm monotonicity are bridge-layer infrastructure for
   future provider compression; the compact bounded-row sample-covariance route
   remains the reader-facing surface.
+- S10 now has a reusable tail/conditioning assumption bundle; future work can
+  compress providers into that bundle or build a public-friendly natural-state
+  wrapper without changing theorem strength.
 - Next RandomMatrix hardbone task: select the next provider-compression or
   public-friendly Matrix Bernstein natural-state wrapper after S10.
 - Current strategy is progress-first: if a hard analytic ingredient is missing,

docs/TestPlan.md

@@ -40,8 +40,9 @@ git diff --check
   matrix log/order bridge leaf, the proved excess-support trace bridge leaf,
   the proved centered-square expectation bridge leaf, and the proved
   real-to-`CStarMatrix` complexified positivity/order transport leaf, and the
-  progress-first Tropp/Lieb one-step assumption-composition consumer and the
-  conditional finite-family trace-MGF assumption-composition consumer are covered in
+  progress-first Tropp/Lieb one-step assumption-composition consumer, the
+  conditional finite-family trace-MGF assumption-composition consumer, and the
+  S10 tail/conditioning assumption bundle wrapper are covered in
   `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`,
   `HighDimProbTest/RandomMatrixConcentrationAPI.lean`,
   `HighDimProbTest/RandomMatrixCStarBridgeAPI.lean`,

docs/TheoremAtlas.md

@@ -136,8 +136,11 @@ natural-state, integrability, MGF, and variance-proxy assumptions recorded in
 `docs/STATEMENTS.md`. The S10 wrapper
 `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFBridge` threads
 that trace-MGF conclusion into the quadratic-form Laplace/tail route under an
-explicit trace-exp threshold event subset assumption; it is not a full Matrix
-Bernstein theorem.
+explicit trace-exp threshold event subset assumption. Its reusable assumption
+bundle `MatrixBernsteinConditioningTraceMGFTailAssumptions` and thin wrapper
+`matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFTailAssumptions`
+package the same tail/conditioning assumptions without proving new hard facts;
+this is not a full Matrix Bernstein theorem.
 
 ## Not Yet Proved