From 49a8a180d392c1906dc01b54e3b1bd28535d0125 Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Sun, 21 Jun 2026 08:43:52 +0000 Subject: [PATCH] Thread explicit Tropp assumptions forward Constraint: Hard Lieb/Jensen, log-order, and trace-exp monotonicity providers are being filled separately, so this leaf must consume them explicitly rather than prove them. Rejected: Waiting for all hard assumptions before composing the one-step route | the current strategy is progress-first with assumptions recorded in docs/STATEMENTS.md Confidence: high Scope-risk: narrow Directive: Keep future high-level Tropp progress assumption-consuming unless a separate provider theorem actually discharges the analytic input. Tested: lake build HighDimProb.RandomMatrix.HardboneStatements; lake env lean HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean; lake env lean HighDimProbJudge/RandomMatrix/TraceExpUse.lean; python .github/scripts/check_text_quality.py; python scripts/judge_policy_check.py; git diff --check; lake build HighDimProbJudge; lake test; lake build Not-tested: Provider proofs for Lieb concavity, Jensen, operator-log monotonicity, trace-exp monotonicity, conditional expectation, integrability propagation, and full Matrix Bernstein remain open. --- .../RandomMatrix/HardboneStatements.lean | 52 +++++++++++++++++++ .../RandomMatrix/TraceExpUse.lean | 1 + .../RandomMatrixHardboneStatementsAPI.lean | 38 ++++++++++++++ docs/README.md | 1 + docs/RandomMatrixAPI.md | 8 ++- docs/STATEMENTS.md | 42 +++++++++++++++ docs/Status.md | 6 ++- docs/TODO.md | 13 ++--- docs/TestPlan.md | 3 +- docs/TheoremAtlas.md | 6 ++- 10 files changed, 158 insertions(+), 12 deletions(-) create mode 100644 docs/STATEMENTS.md diff --git a/HighDimProb/RandomMatrix/HardboneStatements.lean b/HighDimProb/RandomMatrix/HardboneStatements.lean index 88659ef..0bfd59e 100644 --- a/HighDimProb/RandomMatrix/HardboneStatements.lean +++ b/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 diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index ceb2d42..02cdd15 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/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 diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index 707974c..0b1f88e 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/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 diff --git a/docs/README.md b/docs/README.md index 87142f3..a00666f 100644 --- a/docs/README.md +++ b/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. diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index 6b263a1..5a6007a 100644 --- a/docs/RandomMatrixAPI.md +++ b/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 diff --git a/docs/STATEMENTS.md b/docs/STATEMENTS.md new file mode 100644 index 0000000..723904f --- /dev/null +++ b/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. diff --git a/docs/Status.md b/docs/Status.md index 43d2f00..f3d9eae 100644 --- a/docs/Status.md +++ b/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 diff --git a/docs/TODO.md b/docs/TODO.md index 901d8aa..90f8a86 100644 --- a/docs/TODO.md +++ b/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 diff --git a/docs/TestPlan.md b/docs/TestPlan.md index 2a1914c..2b23055 100644 --- a/docs/TestPlan.md +++ b/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`. diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 5728dad..51c5c62 100644 --- a/docs/TheoremAtlas.md +++ b/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.