Expose Tropp conditional-step forwarder

HighDimProb/Examples/RandomMatrix/HardboneStatementAtlasUsage.lean

@@ -38,6 +38,7 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #check bernsteinMatrixExp_le_quadratic
 #check troppLogExpComparisonToK_of_logMonotone_traceExpMono
 #check troppMasterTraceMGFStep_of_liebJensen
+#check troppConditionalStep_of_iIndepFun
 #check troppMasterTraceMGFConditionalStep_of_conditioningBridge
 
 example (theta R : Real) : Prop :=
@@ -64,6 +65,15 @@ example {Omega : Type*} [MeasurableSpace Omega]
     (mHist : Fin m -> MeasurableSpace Omega) : Prop :=
   troppConditionalStep_of_iIndepFun_statement (P := P) theta X K mHist
 
+example {Omega : Type*} [MeasurableSpace Omega]
+    (P : Measure Omega) {m n : Nat}
+    (theta : Real)
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (mHist : Fin m -> MeasurableSpace Omega) :
+    troppConditionalStep_of_iIndepFun_statement (P := P) theta X K mHist :=
+  troppConditionalStep_of_iIndepFun theta X K mHist
+
 example {Omega : Type*} [MeasurableSpace Omega]
     (P : Measure Omega) {m n : Nat}
     (theta R : Real)

HighDimProb/RandomMatrix/HardboneStatements.lean

@@ -850,6 +850,24 @@ theorem troppMasterTraceMGFStep_of_liebJensen {Omega : Type*}
     troppMasterTraceMGFStep_statement (P := P) H Z :=
   hChain hJensen hNormalize
 
+/-- Thin witness for the finite-family conditioning hardbone chain.
+
+This theorem does not prove natural history measurability, history/current-step
+independence, finite-family independence, or the conditional-expectation
+reduction. It only forwards the explicit per-index conditional-expectation
+provider through the statement target. -/
+theorem troppConditionalStep_of_iIndepFun
+    {Omega : Type*} [mOmega : MeasurableSpace Omega]
+    {P : MeasureTheory.Measure Omega} {m n : Nat}
+    (theta : Real)
+    (X : Fin m -> RandomMatrix Omega n n)
+    (K : Fin m -> Matrix (Fin n) (Fin n) Real)
+    (mHist : Fin m -> MeasurableSpace Omega) :
+    @troppConditionalStep_of_iIndepFun_statement Omega mOmega P m n
+      theta X K mHist := by
+  intro _hHist _hHistIndep hCondExp _hIndep i
+  exact hCondExp i
+
 /-- Thin consumer for the Phase 4 conditioning bridge.
 
 The conclusion is one indexed conditional-step target. The proof only applies

HighDimProbJudge/RandomMatrix/TraceExpUse.lean

@@ -104,6 +104,7 @@ open scoped MatrixOrder Matrix.Norms.Operator
 #check HighDimProb.troppHistoryStepIndependent_of_iIndepFun_statement
 #check HighDimProb.condExp_traceExp_history_add_independent_step_statement
 #check HighDimProb.troppConditionalStep_of_iIndepFun_statement
+#check HighDimProb.troppConditionalStep_of_iIndepFun
 #check HighDimProb.matrixExpScaledIntegrable_of_provider_statement
 #check HighDimProb.traceExpIntegrable_troppStateHistory_add_step_statement
 #check HighDimProb.traceExpIntegrable_troppStateHistory_add_K_statement

HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean

@@ -37,6 +37,7 @@ variable (mHist : Fin m -> MeasurableSpace Omega)
 #check troppHistoryStepIndependent_of_iIndepFun_statement
 #check condExp_traceExp_history_add_independent_step_statement
 #check troppConditionalStep_of_iIndepFun_statement
+#check @troppConditionalStep_of_iIndepFun
 #check matrixExpScaledIntegrable_of_provider_statement
 #check traceExpIntegrable_troppStateHistory_add_step_statement
 #check traceExpIntegrable_troppStateHistory_add_K_statement
@@ -75,6 +76,10 @@ example : Prop :=
 example : Prop :=
   troppConditionalStep_of_iIndepFun_statement (P := P) theta X Kfam mHist
 
+example :
+    troppConditionalStep_of_iIndepFun_statement (P := P) theta X Kfam mHist :=
+  troppConditionalStep_of_iIndepFun theta X Kfam mHist
+
 example : Prop :=
   traceExpIntegrable_randomMatrixSum_of_traceExpDominatingProvider_statement
     (P := P) theta X D

docs/RandomMatrixAPI.md

@@ -90,6 +90,7 @@ Conditioning / independence chain:
 - `troppHistoryStepIndependent_of_iIndepFun_statement`
 - `condExp_traceExp_history_add_independent_step_statement`
 - `troppConditionalStep_of_iIndepFun_statement`
+- `troppConditionalStep_of_iIndepFun`
 
 Integrability provider chain:
 
@@ -118,6 +119,7 @@ Thin hardbone consumers:
 - `bernsteinMatrixExp_le_quadratic`
 - `troppLogExpComparisonToK_of_logMonotone_traceExpMono`
 - `troppMasterTraceMGFStep_of_liebJensen`
+- `troppConditionalStep_of_iIndepFun`
 - `troppMasterTraceMGFConditionalStep_of_conditioningBridge`
 
 Hardbone status table:
@@ -128,7 +130,7 @@ Hardbone status table:
 | 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 |
 | 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 |
+| 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 | none yet | absolute domination, Golden-Thompson/product, or boundedness provider |
 | Variance proxy / centered square | `varianceProxyNormBound_of_centeredSquareChain_statement` | typed-prop | none yet | centered-square expansion, rank-one comparison, order/norm bookkeeping |
 | Dimension / support / effective rank | `traceMatrixExp_effectiveRank_bound_statement` | typed-prop | none yet | rank/support/effective-rank core theory |
@@ -137,13 +139,16 @@ 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 finite-family conditioning chain is
+proved by `troppConditionalStep_of_iIndepFun`, but it only forwards the explicit
+per-index conditional-expectation provider and does not discharge the history or
+independence hypotheses. The remaining log/order, Tropp/Lieb, 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,
-finite-family Tropp, or any Matrix Bernstein tail theorem.
+statement-chain assumptions; they do not prove Lieb/Jensen, conditional
+expectation reduction, finite-family Tropp, or any Matrix Bernstein tail theorem.
 
 ## TraceExp / Tropp Bookkeeping Surface
 

docs/Status.md

@@ -86,6 +86,10 @@ Hardbone Bernstein CFC leaf:
 - `bernsteinMatrixExp_le_quadratic_of_cfcLeaves`
 - `bernsteinMatrixExp_le_quadratic`
 
+Hardbone conditioning bridge leaf:
+
+- `troppConditionalStep_of_iIndepFun`
+
 Example-layer wrappers:
 
 - `sampleCovariance_quadraticForm_tail_usage`
@@ -114,7 +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
+  normalization. The conditioning chain now has the thin theorem witness
+  `troppConditionalStep_of_iIndepFun`, which only forwards the explicit
+  per-index conditional-expectation provider and does not prove history
+  measurability or independence. 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,6 +142,8 @@ 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-tropp-conditional-step-of-iindepfun-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-tropp-conditional-step-of-iindepfun-bridge-leaf`.
 - Next RandomMatrix hardbone task:
   `RM-HB12-select-next-hardbone-proof-leaf`.
 

docs/TheoremAtlas.md

@@ -50,16 +50,21 @@ 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 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.
 
 ## Not Yet Proved
 
 - Full Tropp/Lieb machinery.
 - Golden-Thompson route.
 - Full unconditional Matrix Bernstein theorem.
-- Natural history measurability, independence conditioning, and trace-exp
-  integrability propagation for the conditional-step Tropp route.
+- Natural history measurability, independence conditioning,
+  conditional-expectation reduction, 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
+  Tropp/Lieb, integrability, variance-proxy sharpening, and
   dimension/rank refinements.
 - A public-friendly Matrix Bernstein wrapper directly over the natural-state
   route.