Expose natural-state provider tail route

HighDimProb/RandomMatrix/ConcentrationStatements.lean

@@ -5630,6 +5630,147 @@ theorem matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAss
       X K V theta R t mHist h.toTailAssumptions
 
 
+
+/-- Public-friendly natural-state S10 tail wrapper using the provider-compressed
+assumption route.
+
+This theorem exposes the assumptions that remain hard for the current WATCH
+contract while routing only the provider-backed natural-history and bounded
+integrability fields through
+`MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions`.
+It does not compress history/current independence, conditional expectation,
+variance-proxy normalization, full-sum trace integrability, or the tail-side
+measurability/subset assumptions. -/
+theorem matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions
+    {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 RH RZ RK RX : Real)
+    (mHist : Fin m -> MeasurableSpace Omega)
+    (hChain :
+      @troppConditionalStep_of_iIndepFun_statement Omega mOmega P m n
+        theta X K mHist)
+    (hSuffix :
+      forall i : Fin m,
+        forall j : Fin m,
+          ((i.succ : Fin (m + 1)) : Nat) <= (j : Nat) ->
+            forall r c,
+              @Measurable Omega Real (mHist i) inferInstance
+                (fun omega => X j omega r c))
+    (hHistoryStepIndependent :
+      @troppHistoryStepIndependent_of_iIndepFun_statement Omega mOmega P m n
+        theta X K)
+    (hConditionalExpectation :
+      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))
+    (hHistorySub : forall i, mHist i <= mOmega)
+    (hHistoryRandom :
+      forall i,
+        @IsRandomMatrix Omega mOmega n n P
+          (troppStateHistory theta X K i))
+    (hStepRandom :
+      forall i,
+        @IsRandomMatrix Omega mOmega n n P
+          (troppCurrentRandomStep theta X i))
+    (hHistorySelfAdjoint :
+      forall i omega, IsSelfAdjointMatrix (troppStateHistory theta X K i omega))
+    (hStepSelfAdjoint :
+      forall i,
+        @RandomSelfAdjointMatrix Omega mOmega n P
+          (troppCurrentRandomStep theta X i))
+    (hFiniteMeasure : IsFiniteMeasure P)
+    (hHistoryOperatorNormBound :
+      forall i omega,
+        operatorNorm (@troppStateHistory Omega mOmega m n theta X K i) omega <= RH)
+    (hStepOperatorNormBound :
+      forall i omega,
+        operatorNorm (@troppCurrentRandomStep Omega mOmega m n theta X i) omega <= RZ)
+    (hKOperatorNormBound :
+      forall i omega,
+        operatorNorm (fun _ : Omega => K i) omega <= RK)
+    (hSummandOperatorNormBound :
+      forall i omega, operatorNorm (X i) omega <= RX)
+    (hSummandRadiusNonneg : 0 <= RX)
+    (hExpMeanSelfAdjoint :
+      forall i,
+        IsSelfAdjointMatrix
+          (@matrixExpect Omega mOmega n n P
+            (fun omega => matrixExp (troppCurrentRandomStep theta X i omega))))
+    (hExpMeanStrictlyPositive :
+      forall i,
+        IsStrictlyPositive
+          (@matrixExpect Omega mOmega n n P
+            (fun omega => matrixExp (troppCurrentRandomStep theta X i omega))))
+    (hSigmaFiniteHistory : forall i, SigmaFinite (P.trim (hHistorySub i)))
+    (hRandomMatrix : forall i, IsRandomMatrix P (X i))
+    (hSelfAdjoint : forall i, RandomSelfAdjointMatrix P (X i))
+    (hIndependent : ProbabilityTheory.iIndepFun X P)
+    (hTraceIntegrable :
+      IntegrableRealRandomVariable P
+        (traceExpIntegrand (randomMatrixSum X) theta))
+    (hComparisonSelfAdjoint : forall i, IsSelfAdjointMatrix (K i))
+    (hVarianceProxySelfAdjoint : IsSelfAdjointMatrix V)
+    (hRadiusNonneg : 0 <= R)
+    (hThetaRange : abs theta * R < 3)
+    (hMGFComparison :
+      forall i,
+        MatrixLE
+          (matrixExpect P
+            (fun omega => matrixExp (SMul.smul theta (X i omega))))
+          (matrixExp (K i)))
+    (hVarianceProxyNormalization :
+      Finset.univ.sum (fun i : Fin m => K i) =
+        SMul.smul (bernsteinMGFCoeff theta R) V)
+    (hTailAEMeasurable :
+      AEMeasurable
+        (fun omega => ENNReal.ofReal
+          (traceExpIntegrand (randomMatrixSum X) theta omega)) P)
+    (hTailEventSubset :
+      quadraticFormUpperTailEvent (randomMatrixSum X) t ⊆
+        traceExpThresholdEvent (randomMatrixSum X) theta t) :
+    P (quadraticFormUpperTailEvent (randomMatrixSum X) t) <=
+      ENNReal.ofReal (Real.exp (-(theta * t))) *
+        ENNReal.ofReal
+          (traceMatrixExp (SMul.smul (bernsteinMGFCoeff theta R) V)) := by
+  exact
+    matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions
+      X K V theta R t RH RZ RK RX mHist
+      { chain := hChain
+        suffixEntryMeasurable := hSuffix
+        historyStepIndependent := hHistoryStepIndependent
+        conditionalExpectation := hConditionalExpectation
+        historySub := hHistorySub
+        historyRandom := hHistoryRandom
+        stepRandom := hStepRandom
+        historySelfAdjoint := hHistorySelfAdjoint
+        stepSelfAdjoint := hStepSelfAdjoint
+        finiteMeasure := hFiniteMeasure
+        historyOperatorNormBound := hHistoryOperatorNormBound
+        stepOperatorNormBound := hStepOperatorNormBound
+        kOperatorNormBound := hKOperatorNormBound
+        summandOperatorNormBound := hSummandOperatorNormBound
+        summandRadiusNonneg := hSummandRadiusNonneg
+        expMeanSelfAdjoint := hExpMeanSelfAdjoint
+        expMeanStrictlyPositive := hExpMeanStrictlyPositive
+        sigmaFiniteHistory := hSigmaFiniteHistory
+        randomMatrix := hRandomMatrix
+        selfAdjoint := hSelfAdjoint
+        independent := hIndependent
+        traceIntegrable := hTraceIntegrable
+        comparisonSelfAdjoint := hComparisonSelfAdjoint
+        varianceProxySelfAdjoint := hVarianceProxySelfAdjoint
+        radiusNonneg := hRadiusNonneg
+        thetaRange := hThetaRange
+        mgfComparison := hMGFComparison
+        varianceProxyNormalization := hVarianceProxyNormalization
+        tailAEMeasurable := hTailAEMeasurable
+        tailEventSubset := hTailEventSubset }
+
 /-- Typed target for the spectral-radius reduction for self-adjoint matrices.
 
 This records a future bridge between HighDimProb's deterministic L2 operator

HighDimProbJudge/RandomMatrix/LiebProviderUse.lean

@@ -14,3 +14,4 @@ import HighDimProb.RandomMatrix.ConcentrationStatements
 #check HighDimProb.matrixExpSupportDomination_identity
 #check HighDimProb.MatrixBernsteinConditioningTraceMGFProviderAssumptions
 #check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions
+#check HighDimProb.matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions

HighDimProbTest/RandomMatrixLiebProviderAPI.lean

@@ -21,3 +21,4 @@ open scoped MatrixOrder Matrix.Norms.Operator Matrix.Norms.L2Operator
 #check MatrixBernsteinConditioningTraceMGFProviderAssumptions
 #check MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions
 #check matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions
+#check matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions

docs/RandomMatrixAPI.md

@@ -214,6 +214,7 @@ Thin hardbone consumers:
 - `MatrixBernsteinConditioningTraceMGFProviderAssumptions`
 - `MatrixBernsteinConditioningTraceMGFProviderAssumptions.toTailAssumptions`
 - `matrixBernsteinQuadraticFormUpperTail_of_conditioningTraceMGFProviderAssumptions`
+- `matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions`
 
 Hardbone status table:
 

docs/STATEMENTS.md

@@ -274,3 +274,25 @@ Non-goals for this S9/S10 compression step:
   theta optimization, or full Matrix Bernstein.
 - It should reduce explicit assumption burden only where the provider theorem
   actually supplies a named premise.
+
+## RM-LIEB-S16: public-friendly natural-state provider tail route
+
+Consumer theorem:
+
+- `matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions`
+
+This wrapper is a public route over the S10 provider-compressed bundle. It
+constructs `MatrixBernsteinConditioningTraceMGFProviderAssumptions` internally
+and then uses `.toTailAssumptions`, so callers do not supply the provider-
+discharged natural-history measurability and bounded integrability fields as
+separate tail assumptions.
+
+WATCH boundary: the conditioning contract is unchanged. The wrapper still keeps
+`troppHistoryStepIndependent_of_iIndepFun_statement`, the per-index
+`condExp_traceExp_history_add_independent_step_statement`, finite-family
+`ProbabilityTheory.iIndepFun X P`, variance-proxy normalization and
+self-adjointness, full-sum trace integrability, theta/radius range, MGF
+comparison, and the tail AEMeasurability/subset assumptions explicit. A
+sigma-algebra independence bridge for the history/current step remains missing;
+this is not a full Matrix Bernstein theorem or an unconditional sample-covariance
+route.

docs/Status.md

@@ -384,6 +384,12 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact
   `MatrixBernsteinConditioningTraceMGFProviderAssumptions`. Independence,
   conditional expectation, variance proxy, full-sum trace integrability, and
   tail-side assumptions remain explicit.
+- Added S16 public-friendly WATCH route:
+  `matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions`.
+  It constructs the provider bundle internally and hides only the provider-
+  discharged natural-history and bounded-integrability tail fields; the
+  history/current independence and conditional-expectation contracts are still
+  explicit because the sigma-algebra independence bridge remains missing.
 
 - Progress-first hardbone scaffold:
   `RM-LIEB-S9-conditional-step-assumption-composition-contract`, adding `traceMGFBernsteinVarianceProxyBound_of_conditioningBridge` as a finite-family trace-MGF consumer from explicit conditioning, natural-state, integrability, and variance-proxy assumptions. The hard assumptions consumed by the theorem are recorded in `docs/STATEMENTS.md`; this does not prove those assumptions.

docs/TestPlan.md

@@ -87,3 +87,21 @@ example, test, and judge files.
 Keep this file short. Add new details only when they change what contributors
 must run or what CI enforces. Archive old stage-by-stage test history in
 `archive.md`.
+
+
+## RM-LIEB-S16-natural-state-tail-wrapper validation
+
+For changes to the public-friendly provider tail route, run:
+
+```bash
+lake build HighDimProb.RandomMatrix.ConcentrationStatements
+lake env lean HighDimProbTest/RandomMatrixLiebProviderAPI.lean
+lake env lean HighDimProbJudge/RandomMatrix/LiebProviderUse.lean
+python scripts/judge_policy_check.py
+python .github/scripts/check_text_quality.py
+git diff --check
+```
+
+The API and judge files should `#check`
+`matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptions` in
+addition to the provider bundle and `.toTailAssumptions` route.