Discharge matrix log-to-exp hardbone bridge

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)

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

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

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
 

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,

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,

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

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`.
 

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.

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