Thread explicit Tropp assumptions forward

HighDimProb/RandomMatrix/HardboneStatements.lean

@@ -1448,6 +1448,58 @@ theorem troppMasterTraceMGFStep_of_liebJensen {Omega : Type*}
     troppMasterTraceMGFStep_statement (P := P) H Z :=
   hChain hJensen hNormalize
 
+/-- Progress-first composition of the Lieb/Jensen one-step chain with the
+log/order-to-`K` chain.
+
+This theorem deliberately consumes the hard analytic assumptions explicitly:
+Lieb/Jensen, log-exp normalization, operator-log/log-domain comparison, and
+trace-exp monotonicity are premises.  It does not prove those facts, nor
+Golden-Thompson, conditional expectation, integrability propagation, variance
+proxy control, or full Matrix Bernstein. -/
+theorem troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder {Omega : Type*}
+    [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega}
+    [MeasureTheory.IsProbabilityMeasure P] {n : Nat}
+    (H K : Matrix (Fin n) (Fin n) Real)
+    (Z : RandomMatrix Omega n n)
+    (hStepChain : troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Z)
+    (hJensen :
+      liebJensenTraceExp_statement (P := P) H
+        (fun omega => matrixExp (Z omega)))
+    (hNormalize :
+      forall omega, matrixExpLogSelfAdjointNormalization_statement (Z omega))
+    (hLogChain :
+      troppLogExpComparisonToK_of_logOrderKChain_statement H
+        (matrixExpect P (fun omega => matrixExp (Z omega))) K)
+    (hLog : matrixLog_le_of_le_matrixExp_statement
+      (matrixExpect P (fun omega => matrixExp (Z omega))) K)
+    (hTrace : traceMatrixExp_mono_add_selfAdjoint_statement H
+      (CFC.log (matrixExpect P (fun omega => matrixExp (Z omega)))) K)
+    (hH : IsSelfAdjointMatrix H)
+    (hZ : RandomSelfAdjointMatrix P Z)
+    (hTraceInt :
+      IntegrableRealRandomVariable P
+        (fun omega => traceMatrixExp (H + Z omega)))
+    (hExpInt : IntegrableRandomMatrix P (fun omega => matrixExp (Z omega)))
+    (hExpMeanSA :
+      IsSelfAdjointMatrix
+        (matrixExpect P (fun omega => matrixExp (Z omega))))
+    (hExpMeanPos :
+      IsStrictlyPositive
+        (matrixExpect P (fun omega => matrixExp (Z omega))))
+    (hKSA : IsSelfAdjointMatrix K)
+    (hMGF :
+      MatrixLE
+        (matrixExpect P (fun omega => matrixExp (Z omega)))
+        (matrixExp K)) :
+    expect P (fun omega => traceMatrixExp (H + Z omega)) <=
+      traceMatrixExp (H + K) :=
+  troppMasterTraceMGFStep_trace_bound_of_logExpComparisonToK H K Z
+    (troppMasterTraceMGFStep_of_liebJensen H Z hStepChain hJensen hNormalize)
+    (troppLogExpComparisonToK_of_logMonotone_traceExpMono H
+      (matrixExpect P (fun omega => matrixExp (Z omega))) K
+      hLogChain hLog hTrace)
+    hH hZ hTraceInt hExpInt hExpMeanSA hExpMeanPos hKSA hMGF
+
 /-- Thin witness for the finite-family conditioning hardbone chain.
 
 This theorem does not prove natural history measurability, history/current-step

HighDimProbJudge/RandomMatrix/TraceExpUse.lean

@@ -140,6 +140,7 @@ example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
 #check HighDimProb.matrixExpLogSelfAdjointNormalization_statement
 #check HighDimProb.matrixExpLogSelfAdjointNormalization
 #check HighDimProb.troppMasterTraceMGFStep_of_liebJensen_statement
+#check HighDimProb.troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder
 #check HighDimProb.troppNaturalHistoryMeasurable_statement
 #check HighDimProb.troppHistoryStepIndependent_of_iIndepFun_statement
 #check HighDimProb.condExp_traceExp_history_add_independent_step_statement

HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean

@@ -89,6 +89,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #check troppLogExpComparisonToK_of_logMonotone_traceExpMono
 #check matrixExpLogSelfAdjointNormalization
 #check troppMasterTraceMGFStep_of_liebJensen
+#check troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder
 #check troppMasterTraceMGFConditionalStep_of_conditioningBridge
 #check traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider
 #check varianceProxyNormBound_of_centeredSquareChain
@@ -148,6 +149,43 @@ example
 example : Prop :=
   troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Y
 
+example
+    (hStepChain : troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Y)
+    (hJensen :
+      liebJensenTraceExp_statement (P := P) H
+        (fun omega => matrixExp (Y omega)))
+    (hNormalize :
+      forall omega, matrixExpLogSelfAdjointNormalization_statement (Y omega))
+    (hLogChain :
+      troppLogExpComparisonToK_of_logOrderKChain_statement H
+        (matrixExpect P (fun omega => matrixExp (Y omega))) K)
+    (hLog : matrixLog_le_of_le_matrixExp_statement
+      (matrixExpect P (fun omega => matrixExp (Y omega))) K)
+    (hTrace : traceMatrixExp_mono_add_selfAdjoint_statement H
+      (CFC.log (matrixExpect P (fun omega => matrixExp (Y omega)))) K)
+    (hH : IsSelfAdjointMatrix H)
+    (hY : RandomSelfAdjointMatrix P Y)
+    (hTraceInt :
+      IntegrableRealRandomVariable P
+        (fun omega => traceMatrixExp (H + Y omega)))
+    (hExpInt : IntegrableRandomMatrix P (fun omega => matrixExp (Y omega)))
+    (hExpMeanSA :
+      IsSelfAdjointMatrix
+        (matrixExpect P (fun omega => matrixExp (Y omega))))
+    (hExpMeanPos :
+      IsStrictlyPositive
+        (matrixExpect P (fun omega => matrixExp (Y omega))))
+    (hKSA : IsSelfAdjointMatrix K)
+    (hMGF :
+      MatrixLE
+        (matrixExpect P (fun omega => matrixExp (Y omega)))
+        (matrixExp K)) :
+    expect P (fun omega => traceMatrixExp (H + Y omega)) <=
+      traceMatrixExp (H + K) :=
+  troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder
+    H K Y hStepChain hJensen hNormalize hLogChain hLog hTrace
+    hH hY hTraceInt hExpInt hExpMeanSA hExpMeanPos hKSA hMGF
+
 example : Prop :=
   troppConditionalStep_of_iIndepFun_statement (P := P) theta X Kfam mHist
 

docs/README.md

@@ -9,6 +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.
 - `TestPlan.md`: checks contributors should run.
 - `Workflow.md`: contribution and cleanup rules.
 - `TODO.md`: short active task list.

docs/RandomMatrixAPI.md

@@ -120,6 +120,7 @@ Tropp/Lieb/Golden-Thompson chain:
 - `matrixExpLogSelfAdjointNormalization_statement`
 - `matrixExpLogSelfAdjointNormalization`
 - `troppMasterTraceMGFStep_of_liebJensen_statement`
+- `troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder`
 
 Conditioning / independence chain:
 
@@ -202,7 +203,7 @@ Hardbone status table:
 | Matrix log/order bridge | `matrixLog_le_of_le_matrixExp_statement` | proven by `matrixLog_le_of_le_matrixExp` | turns explicit log-monotonicity and `matrixExp` log-domain premises into `log M <= K` | `matrixExp` log-domain is supplied by `matrixExpLogDomainForSelfAdjoint`; operator-log monotonicity remains the external input |
 | Real-to-CStar bridge | `realMatrixToCStarMatrix` and transport statement targets | representation map, add/sub, self-adjoint transport, and CStar-side positivity/order/strict-positivity transport from explicit complexified premises proved | exposes the CStar representation route for future operator-log monotonicity proofs | real-to-complex positivity/order premises and unconditional log-back transport remain open |
 | Log/order-to-`K` | `troppLogExpComparisonToK_of_logOrderKChain_statement` | typed-prop | `troppLogExpComparisonToK_of_logMonotone_traceExpMono` | trace-exp monotonicity plus the explicit log/order bridge inputs |
-| 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 |
+| Tropp/Lieb/GT one-step | `troppMasterTraceMGFStep_of_liebJensen_statement` | typed-prop plus progress-first composition consumer | `troppMasterTraceMGFStep_of_liebJensen`; `troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder` composes the one-step primitive with the log/order-to-`K` bridge | Lieb concavity, probability-measure Jensen, log-exp normalization, operator-log/log-domain input, trace-exp monotonicity; 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, 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`, `MatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_two`, exact-row centered-square sample-covariance wrappers and bundles, `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 providers, Tropp/Lieb, trace-MGF integrability, and full Matrix Bernstein remain explicit or open |
@@ -244,7 +245,10 @@ only gives the `(n + 1 : Real)` effective-rank parameter, so zero directions are
 not accidentally treated as free. The thin consumers only apply explicit
 statement-chain assumptions; they do not prove Lieb/Jensen, conditional
 expectation reduction, automatic domination, variance-proxy control,
-finite-family Tropp, or any Matrix Bernstein tail theorem.
+finite-family Tropp, or any Matrix Bernstein tail theorem. The progress-first
+consumer `troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder` directly
+threads explicit Lieb/Jensen and log/order assumptions into a one-step `K` bound;
+its consumed hard assumptions are listed in `docs/STATEMENTS.md`.
 
 ## TraceExp / Tropp Bookkeeping Surface
 

docs/STATEMENTS.md

@@ -0,0 +1,42 @@
+# Statement Assumption Ledger
+
+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.
+
+## RM-LIEB-S8: Tropp one-step `K` bound from explicit Lieb/log-order inputs
+
+Consumer theorem:
+
+- `troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder`
+
+This theorem composes existing thin consumers and requires the following hard
+facts as explicit premises:
+
+- `troppMasterTraceMGFStep_of_liebJensen_statement H Z`, the source-level
+  statement target reducing the Tropp one-step primitive to Lieb/Jensen facts.
+- `liebJensenTraceExp_statement H (fun omega => matrixExp (Z omega))`, the
+  Jensen consequence of Lieb trace-exponential concavity for the exponential
+  random matrix.
+- `forall omega, matrixExpLogSelfAdjointNormalization_statement (Z omega)`, the
+  pointwise `log (exp Z) = Z` normalization target.
+- `troppLogExpComparisonToK_of_logOrderKChain_statement H
+  (matrixExpect P (fun omega => matrixExp (Z omega))) K`, the statement-chain
+  target for replacing the logarithmic one-step RHS by a deterministic `K`.
+- `matrixLog_le_of_le_matrixExp_statement
+  (matrixExpect P (fun omega => matrixExp (Z omega))) K`, the explicit
+  operator-log/log-domain bridge for the matrix MGF mean.
+- `traceMatrixExp_mono_add_selfAdjoint_statement H
+  (CFC.log (matrixExpect P (fun omega => matrixExp (Z omega)))) K`, the
+  trace-exponential monotonicity step after adding the history matrix.
+- The ordinary side conditions consumed by `troppMasterTraceMGFStep_statement`
+  and `troppLogExpComparisonToK_statement`: self-adjointness, random
+  self-adjointness, trace integrability, matrix-exp integrability, strict
+  positivity of the matrix-exp mean, self-adjointness of `K`, and the MGF
+  Loewner comparison against `matrixExp K`.
+
+Non-goals for this consumer:
+
+- It does not prove Lieb concavity, Jensen, operator-log monotonicity,
+  trace-exp monotonicity, Golden-Thompson, conditional expectation,
+  integrability propagation, variance-proxy control, or full Matrix Bernstein.

docs/Status.md

@@ -362,8 +362,10 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact
   `RM-LIEB-S5-real-to-cstar-transport-api-contract`, proving the basic real-to-`CStarMatrix` transport shape in a probe, including entrywise, add/sub, and self-adjoint transport; positivity/order/log transport remains open.
 - Completed hardbone contract leaf:
   `RM-LIEB-S6-real-to-cstar-positivity-order-transport-contract`, proving the CStar-side transport from explicit complexified nonnegativity, Loewner-order, and strict-positivity premises. The real-to-complex positivity/order bridge and unconditional `CFC.log` log-back compatibility remain open.
-- Next safe hardbone task:
-  `RM-LIEB-S7-real-to-complexified-positivity-order-bridge-audit-contract`, focused on whether HighDimProb real PSD/`MatrixLE`/strict-positivity facts can supply the complexified premises without overstating log-back compatibility.
+- Progress-first hardbone contract leaf:
+  `RM-LIEB-S8-tropp-master-trace-mgf-assumption-composition-contract`, adding `troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder` as a high-level consumer from explicit Lieb/Jensen and log/order assumptions to the one-step trace-MGF `K` bound. The hard assumptions consumed by the theorem are recorded in `docs/STATEMENTS.md`; this does not prove those assumptions.
+- Next aggressive hardbone task:
+  `RM-LIEB-S9-conditional-step-assumption-composition-contract`, focused on threading explicit one-step/conditional assumptions into the finite-family trace-MGF route without waiting for the hard assumption providers.
 
 ## Verification
 

docs/TODO.md

@@ -26,12 +26,13 @@ This is the active short list. Old completed task logs were collapsed into
   future provider compression; the compact bounded-row sample-covariance route
   remains the reader-facing surface.
 - Next RandomMatrix hardbone task:
-  `RM-LIEB-S7-real-to-complexified-positivity-order-bridge-audit-contract`.
-- That next task should audit whether HighDimProb real PSD, `MatrixLE`, and real
-  strict-positivity assumptions can provide the complexified premises consumed
-  by the proved real-to-`CStarMatrix` transport lemmas. Do not treat `CFC.log`
-  log-back compatibility as proved unless a separate compatibility theorem is
-  established.
+  `RM-LIEB-S9-conditional-step-assumption-composition-contract`.
+- Current strategy is progress-first: if a hard analytic ingredient is missing,
+  consume it as an explicit assumption, register it in `docs/STATEMENTS.md`, and
+  keep moving the high-level Tropp/Lieb trace-MGF route forward. Do not claim
+  Lieb/Jensen, Golden-Thompson, operator-log monotonicity, trace-exp
+  monotonicity, conditional expectation, or full Matrix Bernstein unless a
+  separate provider theorem proves it.
 
 ## Active Documentation Work
 

docs/TestPlan.md

@@ -39,7 +39,8 @@ git diff --check
   CFC hardbone leaf, the proved matrix-exp/log normalization and log-domain leaves, the proved
   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 are covered in
+  real-to-`CStarMatrix` complexified positivity/order transport leaf, and the
+  progress-first Tropp/Lieb one-step assumption-composition consumer are covered in
   `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`,
   `HighDimProbTest/RandomMatrixCStarBridgeAPI.lean`, and
   `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`.

docs/TheoremAtlas.md

@@ -122,7 +122,11 @@ the sharp-chain premise explicit. The local matrix-exp/log normalization leaf is
 route now includes the proved thin bridge `matrixLog_le_of_le_matrixExp`, which
 composes explicit operator-log monotonicity and `matrixExp` log-domain premises.
 It does not prove those premises or the downstream trace-exponential
-monotonicity step. The finite-family conditioning chain now has the thin witness
+monotonicity step. The progress-first consumer
+`troppMasterTraceMGFStep_trace_bound_of_liebJensen_logOrder` now threads explicit
+Lieb/Jensen, log normalization, log/order, trace-exp monotonicity, and ordinary
+one-step side assumptions into the direct trace-MGF `K` bound; the consumed hard
+assumptions are tracked in `docs/STATEMENTS.md`. The finite-family conditioning chain now has the thin witness
 `troppConditionalStep_of_iIndepFun`; it forwards the explicit per-index
 conditional-expectation provider and does not prove the history, independence,
 or conditional-expectation inputs themselves.