From 1120f423f3762bd55494c94c30e48d0fea3dfe6e Mon Sep 17 00:00:00 2001 From: HighDimProb Dev Date: Fri, 19 Jun 2026 11:39:06 +0000 Subject: [PATCH] Discharge the conditional matrix log-to-exp bridge leaf Constraint: RM-HB12-matrix-log-le-of-le-matrix-exp-bridge-leaf is a thin hardbone leaf over existing explicit log-monotonicity and matrix-exp log-domain premises. Rejected: Proving operator-log monotonicity or matrixExp strict positivity in this leaf | those remain separate analytic hardbone targets. Confidence: high Scope-risk: narrow Directive: Do not cite this bridge as discharging log-monotonicity, trace-exp monotonicity, Tropp/Lieb, Golden-Thompson, integrability, variance-proxy, or full Matrix Bernstein. Tested: RED lake env lean HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean failed on missing matrixLog_le_of_le_matrixExp; lake build HighDimProb.RandomMatrix.HardboneStatements; lake env lean HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean; lake env lean HighDimProbJudge/RandomMatrix/TraceExpUse.lean; lake env lean HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean; python scripts/judge_policy_check.py; python .github/scripts/check_text_quality.py; git diff --check; lake build HighDimProbJudge; lake build HighDimProb.Examples; lake test; lake build. Not-tested: GitHub CI and PR checks not run because no PR was requested. --- .../HardboneStatementAtlasUsage.lean | 6 ++++++ .../RandomMatrix/HardboneStatements.lean | 18 ++++++++++++++++++ HighDimProbJudge/RandomMatrix/TraceExpUse.lean | 1 + .../RandomMatrixHardboneStatementsAPI.lean | 5 +++++ docs/JudgeSystem.md | 2 +- docs/RandomMatrixAPI.md | 14 ++++++++++---- docs/Status.md | 12 ++++++++++-- docs/TODO.md | 2 ++ docs/TestPlan.md | 2 +- docs/TheoremAtlas.md | 7 ++++++- 10 files changed, 60 insertions(+), 9 deletions(-) diff --git a/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean b/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean index 1e037cc..a559abc 100644 --- a/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean +++ b/HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean @@ -21,6 +21,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check cfcScalarInequalityToMatrixLE_statement #check bernsteinMatrixExp_le_quadratic_of_cfcChain_statement #check operatorLogMonotoneOnPositiveMatrices_statement +#check matrixLog_le_of_le_matrixExp_statement #check troppLogExpComparisonToK_of_logOrderKChain_statement #check liebTraceExpConcavity_statement #check troppMasterTraceMGFStep_of_liebJensen_statement @@ -36,6 +37,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check cfcScalarInequalityToMatrixLE_bernsteinExpQuadratic #check bernsteinMatrixExp_le_quadratic_of_cfcLeaves #check bernsteinMatrixExp_le_quadratic +#check matrixLog_le_of_le_matrixExp #check troppLogExpComparisonToK_of_logMonotone_traceExpMono #check troppMasterTraceMGFStep_of_liebJensen #check troppMasterTraceMGFConditionalStep_of_conditioningBridge @@ -50,6 +52,10 @@ example {n : Nat} (A : Matrix (Fin n) (Fin n) Real) (theta R : Real) : example {n : Nat} (H M K : Matrix (Fin n) (Fin n) Real) : Prop := troppLogExpComparisonToK_of_logOrderKChain_statement H M K +example {n : Nat} (M K : Matrix (Fin n) (Fin n) Real) : + matrixLog_le_of_le_matrixExp_statement M K := + matrixLog_le_of_le_matrixExp M K + example {Omega : Type*} [MeasurableSpace Omega] (P : Measure Omega) [IsProbabilityMeasure P] {n : Nat} (H : Matrix (Fin n) (Fin n) Real) diff --git a/HighDimProb/RandomMatrix/HardboneStatements.lean b/HighDimProb/RandomMatrix/HardboneStatements.lean index ab29cf2..d071de3 100644 --- a/HighDimProb/RandomMatrix/HardboneStatements.lean +++ b/HighDimProb/RandomMatrix/HardboneStatements.lean @@ -820,6 +820,24 @@ theorem bernsteinMatrixExp_le_quadratic_of_cfcChain_spectrum {n : Nat} (cfcScalarInequalityToMatrixLE_bernsteinExpQuadratic A theta R) (bernsteinCFCExpressionNormalization A theta R) +/-- Thin bridge from a log-monotonicity premise and the matrix-exp log-domain +premise to the direct `log M <= K` comparison. + +This theorem only composes explicit assumptions from the log/order-to-`K` +chain. It does not prove operator-log monotonicity, strict positivity of +`matrixExp K`, trace-exp monotonicity, Tropp/Lieb, Golden-Thompson, +integrability propagation, variance-proxy control, or full Matrix +Bernstein. -/ +theorem matrixLog_le_of_le_matrixExp {n : Nat} + (M K : Matrix (Fin n) (Fin n) Real) : + matrixLog_le_of_le_matrixExp_statement M K := by + intro hLog hDomain hM hMpos hK hMK + rcases hDomain hK with ⟨hExpSA, hExpPos, hLogExp⟩ + have hLE : MatrixLE (CFC.log M) (CFC.log (matrixExp K)) := + hLog hM hMpos hExpSA hExpPos hMK + rw [hLogExp] at hLE + exact hLE + /-- Thin consumer for the log/order-to-`K` hardbone chain. This theorem only composes the Phase 2 log-order and trace-exp monotonicity diff --git a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean index dd0bb70..fa56e56 100644 --- a/HighDimProbJudge/RandomMatrix/TraceExpUse.lean +++ b/HighDimProbJudge/RandomMatrix/TraceExpUse.lean @@ -93,6 +93,7 @@ open scoped MatrixOrder Matrix.Norms.Operator #check HighDimProb.operatorLogMonotoneOnPositiveMatrices_statement #check HighDimProb.matrixExpLogDomainForSelfAdjoint_statement #check HighDimProb.matrixLog_le_of_le_matrixExp_statement +#check HighDimProb.matrixLog_le_of_le_matrixExp #check HighDimProb.traceMatrixExp_mono_add_selfAdjoint_statement #check HighDimProb.troppLogExpComparisonToK_of_logOrderKChain_statement #check HighDimProb.liebTraceExpConcavity_statement diff --git a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean index 95686d5..2caf289 100644 --- a/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean +++ b/HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean @@ -26,6 +26,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega) #check operatorLogMonotoneOnPositiveMatrices_statement #check matrixExpLogDomainForSelfAdjoint_statement #check matrixLog_le_of_le_matrixExp_statement +#check matrixLog_le_of_le_matrixExp #check traceMatrixExp_mono_add_selfAdjoint_statement #check troppLogExpComparisonToK_of_logOrderKChain_statement #check liebTraceExpConcavity_statement @@ -69,6 +70,10 @@ example : Prop := example : Prop := troppLogExpComparisonToK_of_logOrderKChain_statement H M K +example : + matrixLog_le_of_le_matrixExp_statement M K := + matrixLog_le_of_le_matrixExp M K + example : Prop := troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Y diff --git a/docs/JudgeSystem.md b/docs/JudgeSystem.md index 2851c9b..437d8df 100644 --- a/docs/JudgeSystem.md +++ b/docs/JudgeSystem.md @@ -64,7 +64,7 @@ theorems or typed statements without relying on local test internals. explicit hypotheses, self-adjoint matrix-exponential PSD and trace nonnegativity bridges, random self-adjoint trace-exp moment nonnegativity, real/lintegral bridge theorem, natural-state Tropp/trace-MGF route checks, - and remaining typed statement APIs. + the proved matrix log/order bridge, and remaining typed statement APIs. - `HighDimProbJudge/RandomMatrix/LaplaceUse.lean`: matrix Laplace RHS and lintegral RHS vocabulary, trace-exp threshold events, MB-S5 conditional Markov/Laplace bridge APIs, MB-S6 explicit-dominance conditional wrappers, diff --git a/docs/RandomMatrixAPI.md b/docs/RandomMatrixAPI.md index f0bcfd9..daa9e53 100644 --- a/docs/RandomMatrixAPI.md +++ b/docs/RandomMatrixAPI.md @@ -73,6 +73,7 @@ Log/order-to-`K` chain: - `operatorLogMonotoneOnPositiveMatrices_statement` - `matrixExpLogDomainForSelfAdjoint_statement` - `matrixLog_le_of_le_matrixExp_statement` +- `matrixLog_le_of_le_matrixExp` - `traceMatrixExp_mono_add_selfAdjoint_statement` - `troppLogExpComparisonToK_of_logOrderKChain_statement` @@ -116,6 +117,7 @@ Thin hardbone consumers: - `bernsteinMatrixExp_le_quadratic_of_cfcChain` - `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` - `bernsteinMatrixExp_le_quadratic` +- `matrixLog_le_of_le_matrixExp` - `troppLogExpComparisonToK_of_logMonotone_traceExpMono` - `troppMasterTraceMGFStep_of_liebJensen` - `troppMasterTraceMGFConditionalStep_of_conditioningBridge` @@ -126,7 +128,8 @@ Hardbone status table: |---|---|---|---|---| | Scalar Bernstein hardbone leaf | `scalarBernsteinExpQuadraticInequality_statement` | proven by `scalarBernsteinExpQuadraticInequality` | CFC-chain assumptions can reuse the proved scalar theorem | none for this scalar leaf | | Bernstein CFC | `bernsteinMatrixExp_le_quadratic_statement` | proven by `bernsteinMatrixExp_le_quadratic` | `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` documents the reusable composition | preferred `*_of_troppAssumptions` wrappers bypass pointwise CFC fields; explicit-CFC wrappers remain for compatibility | -| Log/order-to-`K` | `troppLogExpComparisonToK_of_logOrderKChain_statement` | typed-prop | `troppLogExpComparisonToK_of_logMonotone_traceExpMono` | operator-log monotonicity, log domain for `matrixExp`, trace-exp monotonicity | +| 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` | operator-log monotonicity and the `matrixExp` log-domain premise remain external inputs | +| 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 | | 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 | @@ -137,9 +140,12 @@ Hardbone status table: 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 direct matrix log/order bridge is +proved by `matrixLog_le_of_le_matrixExp`, but it only composes explicit +operator-log monotonicity and `matrixExp` log-domain premises. The remaining +log-domain, trace-exp monotonicity, Tropp/Lieb, conditioning, integrability, +variance-proxy, and dimension/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, diff --git a/docs/Status.md b/docs/Status.md index ab5c807..6237486 100644 --- a/docs/Status.md +++ b/docs/Status.md @@ -86,6 +86,10 @@ Hardbone Bernstein CFC leaf: - `bernsteinMatrixExp_le_quadratic_of_cfcLeaves` - `bernsteinMatrixExp_le_quadratic` +Hardbone log/order bridge leaf: + +- `matrixLog_le_of_le_matrixExp` + Example-layer wrappers: - `sampleCovariance_quadraticForm_tail_usage` @@ -114,8 +118,11 @@ Example modules: 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 - are now `MatrixBernsteinPositiveSideTroppAssumptions` and + normalization. The matrix log/order bridge is now proved through + `matrixLog_le_of_le_matrixExp`, but it only composes explicit + log-monotonicity and `matrixExp` log-domain premises. 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 `_under_primitives` wrappers remain compatibility surfaces. @@ -134,6 +141,7 @@ Example modules: assumptions onto the named negative sample-covariance family; they do not prove exponential integrability, trace-exponential integrability, or CFC. - Completed hardbone wrapper task: `RM-HB-sample-covariance-cfc-free-wrapper-contract`. +- Completed hardbone proof leaf: `RM-HB12-matrix-log-le-of-le-matrix-exp-bridge-leaf`. - Next safe hardbone task: `RM-HB12-select-next-hardbone-proof-leaf`. ## Verification diff --git a/docs/TODO.md b/docs/TODO.md index 7f04f70..f76e4c8 100644 --- a/docs/TODO.md +++ b/docs/TODO.md @@ -12,6 +12,8 @@ This is the active short list. Old completed task logs were collapsed into - Keep public examples readable: name families and adapters first, then call the shared RandomMatrix API. - Completed RandomMatrix hardbone wrapper task: `RM-HB-sample-covariance-cfc-free-wrapper-contract`. +- Completed RandomMatrix hardbone proof leaf: + `RM-HB12-matrix-log-le-of-le-matrix-exp-bridge-leaf`. - Next RandomMatrix hardbone task: `RM-HB12-select-next-hardbone-proof-leaf`. diff --git a/docs/TestPlan.md b/docs/TestPlan.md index 9d51701..759421c 100644 --- a/docs/TestPlan.md +++ b/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 proved matrix log/order bridge leaf, are covered in `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`, `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`, and the `HardboneStatementAtlasUsage` example. diff --git a/docs/TheoremAtlas.md b/docs/TheoremAtlas.md index 5f1dc87..db6f8b2 100644 --- a/docs/TheoremAtlas.md +++ b/docs/TheoremAtlas.md @@ -50,6 +50,10 @@ fields in generic call sites. The sample-covariance route now also has CFC-free `_of_troppPrimitive` / `_of_troppPrimitives` wrappers that reuse `bernsteinMatrixExp_le_quadratic` while keeping Tropp/Lieb and integrability assumptions explicit. +The log/order-to-`K` 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. ## Not Yet Proved @@ -58,7 +62,8 @@ assumptions explicit. - Full unconditional Matrix Bernstein theorem. - 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, +- Proofs of the remaining hardbone statement targets for operator-log + monotonicity, `matrixExp` log-domain support, trace-exp monotonicity, Tropp/Lieb, conditioning, integrability, variance-proxy sharpening, and dimension/rank refinements. - A public-friendly Matrix Bernstein wrapper directly over the natural-state