Discharge matrix exp-log normalization hardbone leaf

HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean

@@ -23,6 +23,7 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #check operatorLogMonotoneOnPositiveMatrices_statement
 #check troppLogExpComparisonToK_of_logOrderKChain_statement
 #check liebTraceExpConcavity_statement
+#check matrixExpLogSelfAdjointNormalization_statement
 #check troppMasterTraceMGFStep_of_liebJensen_statement
 #check troppConditionalStep_of_iIndepFun_statement
 #check matrixExpScaledIntegrable_of_provider_statement
@@ -37,6 +38,7 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #check bernsteinMatrixExp_le_quadratic_of_cfcLeaves
 #check bernsteinMatrixExp_le_quadratic
 #check troppLogExpComparisonToK_of_logMonotone_traceExpMono
+#check matrixExpLogSelfAdjointNormalization
 #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} (A : Matrix (Fin n) (Fin n) Real) :
+    matrixExpLogSelfAdjointNormalization_statement A :=
+  matrixExpLogSelfAdjointNormalization A
+
 example {Omega : Type*} [MeasurableSpace Omega]
     (P : Measure Omega) [IsProbabilityMeasure P] {n : Nat}
     (H : Matrix (Fin n) (Fin n) Real)

HighDimProb/RandomMatrix/HardboneStatements.lean

@@ -832,6 +832,17 @@ theorem troppLogExpComparisonToK_of_logMonotone_traceExpMono {n : Nat}
     troppLogExpComparisonToK_statement H M K :=
   hChain hLog hTrace
 
+/-- Matrix-log normalization for self-adjoint exponentials.
+
+This is a local CFC normalization leaf.  It does not prove Lieb concavity,
+Jensen, Golden-Thompson, conditioning, integrability propagation, variance
+proxy control, or full Matrix Bernstein. -/
+theorem matrixExpLogSelfAdjointNormalization {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Real) :
+    matrixExpLogSelfAdjointNormalization_statement A := by
+  intro hA
+  simpa [matrixExp] using (CFC.log_exp (a := A) hA.isSelfAdjoint)
+
 /-- Thin consumer for the Tropp/Lieb/Jensen one-step hardbone chain.
 
 This theorem does not prove Lieb concavity, Jensen, or log-exp normalization;

HighDimProbJudge/RandomMatrix/TraceExpUse.lean

@@ -99,6 +99,7 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #check HighDimProb.liebJensenTraceExp_statement
 #check HighDimProb.goldenThompsonTraceExp_statement
 #check HighDimProb.matrixExpLogSelfAdjointNormalization_statement
+#check HighDimProb.matrixExpLogSelfAdjointNormalization
 #check HighDimProb.troppMasterTraceMGFStep_of_liebJensen_statement
 #check HighDimProb.troppNaturalHistoryMeasurable_statement
 #check HighDimProb.troppHistoryStepIndependent_of_iIndepFun_statement

HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean

@@ -57,6 +57,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #check bernsteinMatrixExp_le_quadratic_of_spectrum_cfcOrder
 #check bernsteinMatrixExp_le_quadratic_of_cfcChain_spectrum
 #check troppLogExpComparisonToK_of_logMonotone_traceExpMono
+#check matrixExpLogSelfAdjointNormalization
 #check troppMasterTraceMGFStep_of_liebJensen
 #check troppMasterTraceMGFConditionalStep_of_conditioningBridge
 
@@ -114,3 +115,7 @@ example :
 example :
     bernsteinMatrixExp_le_quadratic_statement A theta R :=
   bernsteinMatrixExp_le_quadratic A theta R
+
+example :
+    matrixExpLogSelfAdjointNormalization_statement A :=
+  matrixExpLogSelfAdjointNormalization A

docs/JudgeSystem.md

@@ -64,7 +64,8 @@ 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 hardbone matrix-exp/log normalization theorem, 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

@@ -82,6 +82,7 @@ Tropp/Lieb/Golden-Thompson chain:
 - `liebJensenTraceExp_statement`
 - `goldenThompsonTraceExp_statement`
 - `matrixExpLogSelfAdjointNormalization_statement`
+- `matrixExpLogSelfAdjointNormalization`
 - `troppMasterTraceMGFStep_of_liebJensen_statement`
 
 Conditioning / independence chain:

docs/Status.md

@@ -86,6 +86,10 @@ Hardbone Bernstein CFC leaf:
 - `bernsteinMatrixExp_le_quadratic_of_cfcLeaves`
 - `bernsteinMatrixExp_le_quadratic`
 
+Hardbone matrix-exp/log normalization leaf:
+
+- `matrixExpLogSelfAdjointNormalization`
+
 Example-layer wrappers:
 
 - `sampleCovariance_quadraticForm_tail_usage`
@@ -114,7 +118,10 @@ 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
+  normalization. The local matrix-exp/log normalization leaf is now proved by
+  `matrixExpLogSelfAdjointNormalization`; it is only the pointwise CFC
+  normalization consumed by the Tropp/Lieb one-step chain. 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
@@ -134,7 +141,11 @@ 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`.
-- Next safe hardbone task: `RM-HB12-select-next-hardbone-proof-leaf`.
+- Completed hardbone proof leaf:
+  `RM-HB12-matrix-exp-log-selfadjoint-normalization-leaf`.
+- Next safe hardbone task: select another smallest theorem-backed proof leaf
+  among the remaining log/order, Tropp/Lieb, integrability, variance-proxy, or
+  dimension/rank blockers.
 
 ## Verification
 

docs/TODO.md

@@ -6,14 +6,17 @@ This is the active short list. Old completed task logs were collapsed into
 ## Active RandomMatrix Work
 
 - Select the next smallest theorem-backed hardbone proof leaf with a read-only
-  Mathlib/API audit before editing Lean.
+  Mathlib/API audit before editing Lean; the local
+  `matrixExpLogSelfAdjointNormalization` leaf is now done.
 - Keep the Matrix Bernstein under-primitives API honest: wrappers may use Tropp/provider assumptions explicitly, but should not claim missing Tropp/Lieb, Golden-Thompson, trace-MGF, or full Matrix Bernstein proofs.
 - Continue reducing repeated optimized-RHS formulas through shared helpers in `ConcentrationStatements.lean`.
 - 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`.
-- Next RandomMatrix hardbone task:
-  `RM-HB12-select-next-hardbone-proof-leaf`.
+- Completed RandomMatrix hardbone proof leaf:
+  `RM-HB12-matrix-exp-log-selfadjoint-normalization-leaf`.
+- Next RandomMatrix hardbone task: choose the next smallest remaining proof
+  leaf after a fresh read-only Mathlib/API audit.
 
 ## Active Documentation Work
 

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-exp/log normalization leaf, are covered in
   `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`,
   `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`, and the
   `HardboneStatementAtlasUsage` example.

docs/TheoremAtlas.md

@@ -49,7 +49,9 @@ The preferred optimized Matrix Bernstein wrappers use
 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.
+assumptions explicit. The local matrix-exp/log normalization leaf is proved as
+`matrixExpLogSelfAdjointNormalization`; it supplies only the pointwise CFC
+normalization needed by the Tropp/Lieb one-step chain.
 
 ## Not Yet Proved
 
@@ -59,8 +61,8 @@ assumptions explicit.
 - 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,
-  Tropp/Lieb, conditioning, integrability, variance-proxy sharpening, and
-  dimension/rank refinements.
+  Tropp/Lieb concavity/Jensen, conditioning, integrability, variance-proxy
+  sharpening, and dimension/rank refinements.
 - A public-friendly Matrix Bernstein wrapper directly over the natural-state
   route.