Prove honest real-to-CStar positivity transport leaf

HighDimProb/RandomMatrix/CStarBridge.lean

@@ -77,6 +77,43 @@ theorem isSelfAdjoint_realMatrixToCStarMatrix {n : Nat}
     simpa using h.symm
   simp [realMatrixToCStarMatrix, hsym]
 
+/-! ## Proved transport from explicit complexified premises -/
+
+/-- Nonnegativity of the complexified matrix survives the `CStarMatrix` representation.
+
+This is deliberately stated with the complexified matrix premise.  The separate
+real-to-complex positivity bridge is not claimed here. -/
+theorem realMatrixToCStarMatrix_nonneg_of_complexified_nonneg {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Real)
+    (hA : 0 <= A.map (algebraMap Real Complex)) :
+    0 <= realMatrixToCStarMatrix A := by
+  exact map_rel (CStarMatrix.ofMatrixStarAlgEquiv :
+    Matrix (Fin n) (Fin n) Complex ≃⋆ₐ[Complex]
+      CStarMatrix (Fin n) (Fin n) Complex) hA
+
+/-- Loewner order of complexified matrices survives the `CStarMatrix` representation.
+
+This is the proved CStar-side order transport contract.  It does not by itself
+prove that a HighDimProb `MatrixLE A B` supplies the complexified order premise. -/
+theorem realMatrixToCStarMatrixLE_of_complexified_le {n : Nat}
+    (A B : Matrix (Fin n) (Fin n) Real)
+    (hAB : A.map (algebraMap Real Complex) <= B.map (algebraMap Real Complex)) :
+    realMatrixToCStarMatrix A <= realMatrixToCStarMatrix B := by
+  exact map_rel (CStarMatrix.ofMatrixStarAlgEquiv :
+    Matrix (Fin n) (Fin n) Complex ≃⋆ₐ[Complex]
+      CStarMatrix (Fin n) (Fin n) Complex) hAB
+
+/-- Strict positivity of the complexified matrix survives the `CStarMatrix` representation. -/
+theorem realMatrixToCStarStrictlyPositive_of_complexified {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Real)
+    (hA : IsStrictlyPositive (A.map (algebraMap Real Complex))) :
+    IsStrictlyPositive (realMatrixToCStarMatrix A) := by
+  refine ⟨?_, ?_⟩
+  · exact realMatrixToCStarMatrix_nonneg_of_complexified_nonneg A hA.nonneg
+  · exact IsUnit.map (CStarMatrix.ofMatrixStarAlgEquiv :
+      Matrix (Fin n) (Fin n) Complex ≃⋆ₐ[Complex]
+        CStarMatrix (Fin n) (Fin n) Complex) hA.isUnit
+
 /-! ## Statement targets for the remaining transport layer -/
 
 /-- Target: strict positivity survives the real-to-CStar representation. -/
@@ -95,6 +132,17 @@ abbrev realMatrixToCStarLogBack_statement {n : Nat}
   CFC.log (realMatrixToCStarMatrix A) =
     realMatrixToCStarMatrix (CFC.log A)
 
+/-- Close the log-back statement when the log transport equality is supplied explicitly.
+
+This wrapper is intentionally an assumption consumer, not a proof of CFC-log
+compatibility for real-to-CStar transport. -/
+theorem realMatrixToCStarLogBack_of_transport {n : Nat}
+    (A : Matrix (Fin n) (Fin n) Real)
+    (hlog : CFC.log (realMatrixToCStarMatrix A) =
+      realMatrixToCStarMatrix (CFC.log A)) :
+    realMatrixToCStarLogBack_statement A :=
+  hlog
+
 end
 
 end HighDimProb

HighDimProbJudge/RandomMatrix/TraceExpUse.lean

@@ -2,7 +2,7 @@ import HighDimProb.RandomMatrix
 
 noncomputable section
 
-open scoped MatrixOrder Matrix.Norms.Operator
+open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator
 
 #check HighDimProb.matrixExp
 #check HighDimProb.matrixTrace
@@ -103,6 +103,32 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #check HighDimProb.realMatrixToCStarStrictlyPositive_statement
 #check HighDimProb.realMatrixToCStarMatrixLE_statement
 #check HighDimProb.realMatrixToCStarLogBack_statement
+#check HighDimProb.realMatrixToCStarMatrix_nonneg_of_complexified_nonneg
+#check HighDimProb.realMatrixToCStarMatrixLE_of_complexified_le
+#check HighDimProb.realMatrixToCStarStrictlyPositive_of_complexified
+#check HighDimProb.realMatrixToCStarLogBack_of_transport
+
+example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
+    (hA : 0 <= A.map (algebraMap Real Complex)) :
+    0 <= HighDimProb.realMatrixToCStarMatrix A :=
+  HighDimProb.realMatrixToCStarMatrix_nonneg_of_complexified_nonneg A hA
+
+example {n : Nat} (A B : Matrix (Fin n) (Fin n) Real)
+    (hAB : A.map (algebraMap Real Complex) <= B.map (algebraMap Real Complex)) :
+    HighDimProb.realMatrixToCStarMatrix A <= HighDimProb.realMatrixToCStarMatrix B :=
+  HighDimProb.realMatrixToCStarMatrixLE_of_complexified_le A B hAB
+
+example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
+    (hA : IsStrictlyPositive (A.map (algebraMap Real Complex))) :
+    IsStrictlyPositive (HighDimProb.realMatrixToCStarMatrix A) :=
+  HighDimProb.realMatrixToCStarStrictlyPositive_of_complexified A hA
+
+example {n : Nat} (A : Matrix (Fin n) (Fin n) Real)
+    (hlog : CFC.log (HighDimProb.realMatrixToCStarMatrix A) =
+      HighDimProb.realMatrixToCStarMatrix (CFC.log A)) :
+    HighDimProb.realMatrixToCStarLogBack_statement A :=
+  HighDimProb.realMatrixToCStarLogBack_of_transport A hlog
+
 #check HighDimProb.matrixExpLogDomainForSelfAdjoint_statement
 #check HighDimProb.matrixLog_le_of_le_matrixExp_statement
 #check HighDimProb.matrixLog_le_of_le_matrixExp

HighDimProbTest/RandomMatrixCStarBridgeAPI.lean

@@ -0,0 +1,41 @@
+import HighDimProb.RandomMatrix.CStarBridge
+
+open HighDimProb
+open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator
+
+variable {n : Nat}
+variable (A B : Matrix (Fin n) (Fin n) Real)
+
+#check realMatrixToCStarMatrix
+#check realMatrixToCStarMatrix_apply
+#check realMatrixToCStarMatrix_add
+#check realMatrixToCStarMatrix_sub
+#check isSelfAdjoint_realMatrixToCStarMatrix
+#check realMatrixToCStarMatrix_nonneg_of_complexified_nonneg
+#check realMatrixToCStarMatrixLE_of_complexified_le
+#check realMatrixToCStarStrictlyPositive_of_complexified
+#check realMatrixToCStarStrictlyPositive_statement
+#check realMatrixToCStarMatrixLE_statement
+#check realMatrixToCStarLogBack_statement
+#check realMatrixToCStarLogBack_of_transport
+
+example
+    (hA : 0 <= A.map (algebraMap Real Complex)) :
+    0 <= realMatrixToCStarMatrix A :=
+  realMatrixToCStarMatrix_nonneg_of_complexified_nonneg A hA
+
+example
+    (hAB : A.map (algebraMap Real Complex) <= B.map (algebraMap Real Complex)) :
+    realMatrixToCStarMatrix A <= realMatrixToCStarMatrix B :=
+  realMatrixToCStarMatrixLE_of_complexified_le A B hAB
+
+example
+    (hA : IsStrictlyPositive (A.map (algebraMap Real Complex))) :
+    IsStrictlyPositive (realMatrixToCStarMatrix A) :=
+  realMatrixToCStarStrictlyPositive_of_complexified A hA
+
+example
+    (hlog : CFC.log (realMatrixToCStarMatrix A) =
+      realMatrixToCStarMatrix (CFC.log A)) :
+    realMatrixToCStarLogBack_statement A :=
+  realMatrixToCStarLogBack_of_transport A hlog

HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean

@@ -3,7 +3,7 @@ import HighDimProb.RandomMatrix.HardboneStatements
 
 open MeasureTheory
 open HighDimProb
-open scoped MatrixOrder Matrix.Norms.Operator
+open scoped ComplexOrder MatrixOrder Matrix.Norms.Operator
 
 variable {Omega : Type*} [MeasurableSpace Omega]
 variable {P : Measure Omega}
@@ -36,6 +36,10 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #check realMatrixToCStarStrictlyPositive_statement
 #check realMatrixToCStarMatrixLE_statement
 #check realMatrixToCStarLogBack_statement
+#check realMatrixToCStarMatrix_nonneg_of_complexified_nonneg
+#check realMatrixToCStarMatrixLE_of_complexified_le
+#check realMatrixToCStarStrictlyPositive_of_complexified
+#check realMatrixToCStarLogBack_of_transport
 #check traceMatrixExp_mono_add_selfAdjoint_statement
 #check troppLogExpComparisonToK_of_logOrderKChain_statement
 #check liebTraceExpConcavity_statement
@@ -120,6 +124,27 @@ example : Prop :=
 example : Prop :=
   realMatrixToCStarLogBack_statement A
 
+example
+    (hA : 0 <= A.map (algebraMap Real Complex)) :
+    0 <= realMatrixToCStarMatrix A :=
+  realMatrixToCStarMatrix_nonneg_of_complexified_nonneg A hA
+
+example
+    (hAB : M.map (algebraMap Real Complex) <= K.map (algebraMap Real Complex)) :
+    realMatrixToCStarMatrix M <= realMatrixToCStarMatrix K :=
+  realMatrixToCStarMatrixLE_of_complexified_le M K hAB
+
+example
+    (hA : IsStrictlyPositive (A.map (algebraMap Real Complex))) :
+    IsStrictlyPositive (realMatrixToCStarMatrix A) :=
+  realMatrixToCStarStrictlyPositive_of_complexified A hA
+
+example
+    (hlog : CFC.log (realMatrixToCStarMatrix A) =
+      realMatrixToCStarMatrix (CFC.log A)) :
+    realMatrixToCStarLogBack_statement A :=
+  realMatrixToCStarLogBack_of_transport A hlog
+
 example : Prop :=
   troppMasterTraceMGFStep_of_liebJensen_statement (P := P) H Y
 

docs/RandomMatrixAPI.md

@@ -46,14 +46,20 @@ CStar representation bridge:
 - `realMatrixToCStarMatrix_add`
 - `realMatrixToCStarMatrix_sub`
 - `isSelfAdjoint_realMatrixToCStarMatrix`
+- `realMatrixToCStarMatrix_nonneg_of_complexified_nonneg`
+- `realMatrixToCStarMatrixLE_of_complexified_le`
+- `realMatrixToCStarStrictlyPositive_of_complexified`
 - `realMatrixToCStarStrictlyPositive_statement`
 - `realMatrixToCStarMatrixLE_statement`
 - `realMatrixToCStarLogBack_statement`
+- `realMatrixToCStarLogBack_of_transport`
 
 These expose the real-matrix to `CStarMatrix` representation layer needed to
-reuse Mathlib CStar functional-calculus order results. Strict positivity,
-Loewner-order, and `CFC.log` transport are still statement targets, not proved
-facts.
+reuse Mathlib CStar functional-calculus order results. The CStar-side transport
+from explicit complexified nonnegativity, Loewner order, and strict positivity
+premises is proved. The real-matrix-to-complexified positivity/order bridge and
+unconditional `CFC.log` transport remain open; `realMatrixToCStarLogBack_of_transport`
+only consumes an explicitly supplied log-back equality.
 
 ## Matrix Bernstein Surface
 
@@ -194,7 +200,7 @@ 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 |
 | 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 | basic representation map, add/sub, and self-adjoint transport proved | exposes the CStar representation route for future operator-log monotonicity proofs | strict positivity/order/log-back transport from real matrices to `CStarMatrix` remains open |
+| 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 |
 | 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 |

docs/Status.md

@@ -360,8 +360,10 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact
   `RM-LIEB-S4-real-matrix-to-cstar-log-monotonicity-contract`, proving that Mathlib `CFC.log_le_log` is available on `CStarMatrix (Fin n) (Fin n) ℂ` while leaving real-matrix transport open.
 - Completed hardbone contract leaf:
   `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-S6-real-to-cstar-positivity-order-transport-contract`, focused on positivity/order/log transport for the real-to-CStar route.
+  `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.
 
 ## Verification
 

docs/TODO.md

@@ -26,8 +26,12 @@ 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-S6-real-to-cstar-positivity-order-transport-contract`.
-- That next task should audit positivity/order/log transport for the real-to-CStar route; the basic transport map, entrywise behavior, add/sub, and self-adjoint transport are probe-ready.
+  `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.
 
 ## Active Documentation Work
 

docs/TestPlan.md

@@ -38,8 +38,10 @@ git diff --check
 - RandomMatrix hardbone statement-target checks, including the proved Bernstein
   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,
-  and the proved centered-square expectation bridge leaf are covered in
+  the proved centered-square expectation bridge leaf, and the proved
+  real-to-`CStarMatrix` complexified positivity/order transport leaf are covered in
   `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`,
+  `HighDimProbTest/RandomMatrixCStarBridgeAPI.lean`, and
   `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`.
 - RandomMatrix sample-covariance negative-side provider-transfer adapters, the
   compact `SampleCovarianceTailTarget` /

docs/TheoremAtlas.md

@@ -78,7 +78,7 @@ supplies it from coordinate `MemLp 4` assumptions via Mathlib Holder product
 APIs. The bounded-row provider
 `integrableRandomMatrix_randomMatrixSquare_rankOneRandomMatrix_of_sqNorm_bound_memLp_two`
 supplies it from coordinate `MemLp 2` plus pointwise `vectorSqNorm <= R`.
-Centered rank-one square-integrability providers are proved for coordinate `MemLp 4` and bounded-row `MemLp 2` routes. The row-specific exact-row consumer `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two` now supplies a `rowSqNormVarianceProxyNormRHS R` variance-proxy bound from coordinate `MemLp 2`, pointwise `vectorSqNorm <= R_i`, nonnegative radii, and the explicit hardbone sharp-chain premise. The bridge layer connects generic centered-square chains to exact-row sample-covariance variance-proxy consumers, transfers exact-row control to the negative family, and exposes positive/two-sided exact-row centered-square wrappers and bundles. The deterministic PSD Loewner-to-operator-norm bridge is proved as `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`. These are infrastructure routes; full generic centered-square providers, Tropp/Lieb, trace-MGF integrability, and full Matrix Bernstein remain explicit or open.
+Centered rank-one square-integrability providers are proved for coordinate `MemLp 4` and bounded-row `MemLp 2` routes. The row-specific exact-row consumer `sampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two` now supplies a `rowSqNormVarianceProxyNormRHS R` variance-proxy bound from coordinate `MemLp 2`, pointwise `vectorSqNorm <= R_i`, nonnegative radii, and the explicit hardbone sharp-chain premise. The bridge layer connects generic centered-square chains to exact-row sample-covariance variance-proxy consumers, transfers exact-row control to the negative family, and exposes positive/two-sided exact-row centered-square wrappers and bundles. The deterministic PSD Loewner-to-operator-norm bridge is proved as `deterministicMatrixVarianceProxyNorm_mono_of_matrixLE`. The real-to-`CStarMatrix` route now transports explicit complexified nonnegativity, Loewner order, and strict positivity premises to CStar order/strict positivity; real-to-complex positivity/order and unconditional `CFC.log` log-back compatibility remain separate blockers. These are infrastructure routes; full generic centered-square providers, Tropp/Lieb, trace-MGF integrability, and full Matrix Bernstein remain explicit or open.
 The rank/support trace-bound bridge is proved by
 `traceMatrixExp_le_trace_support_exp_lambdaMax_of_supportDomination`,
 with rank/support consumers for the hardbone targets. Deterministic trace/rank