Show centered-square bundle usage in examples

HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean

@@ -104,6 +104,31 @@ theorem sampleCovariance_quadraticForm_tail_usage
       h.traceExpIntegrable h.radiusPositive h.deviationPositive
       h.troppPrimitive
 
+
+/-- Example-level exact-row centered-square-chain quadratic-form tail usage.
+
+This demonstrates the core assumption bundle
+`SampleCovarianceExactRowCenteredSquareTroppAssumptions` directly, rather than
+copying its long field list into an example-local structure. The generic
+centered-square chain, Tropp primitive, and analytic assumptions remain fields
+of that core bundle. -/
+theorem sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage
+    {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega}
+    [IsProbabilityMeasure P] {m n : Nat}
+    (A : RandomMatrix Omega m (n + 1))
+    (R t : Real)
+    (Rvar : Fin m -> Real)
+    (h : SampleCovarianceExactRowCenteredSquareTroppAssumptions
+      (P := P) A R t Rvar) :
+    P (quadraticFormUpperTailEvent
+        (centeredRandomMatrix P (sampleCovariance A)) t) <=
+      sampleCovarianceQuadraticFormTailRHS
+        (m := m) (n := n + 1) R t
+        (rowSqNormVarianceProxyNormRHS Rvar) := by
+  exact
+    sampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppAssumptions
+      (P := P) A R t Rvar h
+
 /-- Assumptions needed by the public conditional sample-covariance
 operator-norm tail wrapper.
 
@@ -195,6 +220,32 @@ theorem sampleCovariance_operatorNorm_tail_usage
       h.negativeRadiusPositive
       h.troppPrimitiveNeg
 
+
+/-- Example-level exact-row centered-square-chain operator-norm tail usage.
+
+This demonstrates the two-sided core bundle
+`SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions`. It adds no
+new mathematics; it only routes the bundled assumptions to the public core
+wrapper. -/
+theorem sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage
+    {Omega : Type*} [MeasurableSpace Omega] {P : Measure Omega}
+    [IsProbabilityMeasure P] {m n : Nat}
+    (A : RandomMatrix Omega m (n + 1))
+    (R Rneg t : Real)
+    (Rvar RvarNeg : Fin m -> Real)
+    (h : SampleCovarianceExactRowCenteredSquareTwoSidedTroppAssumptions
+      (P := P) A R Rneg t Rvar RvarNeg) :
+    P (SelfAdjointOperatorNormTailEvent
+        (centeredRandomMatrix P (sampleCovariance A)) t) <=
+      sampleCovarianceQuadraticFormTailRHS
+          (m := m) (n := n + 1) R t (rowSqNormVarianceProxyNormRHS Rvar) +
+        sampleCovarianceQuadraticFormTailRHS
+          (m := m) (n := n + 1) Rneg t
+          (rowSqNormVarianceProxyNormRHS RvarNeg) := by
+  exact
+    sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppAssumptions
+      (P := P) A R Rneg t Rvar RvarNeg h
+
 end
 
 end HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage

HighDimProb/Examples/RandomMatrix/StatementRoutes.lean

@@ -39,6 +39,8 @@ obligations without creating another core sample-covariance API.
 -/
 
 #check sampleCovariance_operatorNorm_tail_usage
+#check sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage
+#check sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage
 
 /-!
 ## Rank-one covariance and Gram routes

HighDimProbTest/ExamplesAPI.lean

@@ -10,6 +10,8 @@ through `HighDimProb.Examples`.
 #check HighDimProb.Examples.RandomMatrix.SampleCovarianceUsage.sampleCovariance_psd_usage
 #check HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage.sampleCovariance_quadraticForm_tail_usage
 #check HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage.sampleCovariance_operatorNorm_tail_usage
+#check HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage
+#check HighDimProb.Examples.RandomMatrix.SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage
 #check HighDimProb.Examples.RandomMatrix.RankOneMatrixBernsteinPipelineUsage.rankOnePipeline_quadraticForm_tail_optimized_under_primitives
 #check HighDimProb.Examples.RandomMatrix.RandomFeatureKernelUsage.randomFeatureKernel_quadraticForm_tail_optimized_under_primitives
 #check HighDimProb.Examples.RandomMatrix.NTKGramUsage.ntkGram_quadraticForm_tail_optimized_under_primitives

docs/JudgeSystem.md

@@ -337,7 +337,8 @@ python scripts/judge_policy_check.py
   adapters, the explicit-CFC sample-covariance wrappers, the CFC-free
   `_of_troppPrimitive` / `_of_troppPrimitives` sample-covariance wrappers, and
   the opposite-parameter sample-covariance exp/trace/CFC provider-transfer
-  adapters.
+  adapters. Example API checks cover the exact-row centered-square bundle usage
+  wrappers through `StatementRoutes`.
 - The checks are import-boundary/API checks only; they do not prove
   exponential/trace integrability, Tropp/Lieb, Golden-Thompson, full Matrix
   Bernstein, or unconditional sample-covariance concentration. The CFC-free

docs/RandomMatrixAPI.md

@@ -289,6 +289,11 @@ The two-sided/operator-norm exact-row integration is exposed as
 `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`,
 with centered-square-chain variant
 `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitives`.
+The reader-facing example route also exposes
+`SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage`
+and
+`SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage`
+as thin demonstrations of the corresponding core assumption bundles.
 These wrappers do not prove Tropp/Lieb, Golden-Thompson, trace-exp
 integrability, variance-proxy control beyond existing named adapters, or
 unconditional sample-covariance concentration.
@@ -340,6 +345,9 @@ and they are not tail wrappers by themselves.
 - Prefer named adapters over anonymous lambdas.
 - Prefer the sample-covariance `_of_troppPrimitive` / `_of_troppPrimitives`
   wrappers when pointwise Bernstein CFC is the only remaining explicit field.
+- For exact-row centered-square routes, prefer the core `SampleCovarianceExactRowCenteredSquare*TroppAssumptions`
+  bundles and the corresponding `SampleCovarianceTailUsage` examples instead of
+  copying the full hypothesis list.
 - Keep positive-side and negative-side assumptions visibly distinct when the
   theorem still needs both sides.
 - Put domain vocabulary in examples as thin wrappers over the core RandomMatrix

docs/Status.md

@@ -93,6 +93,8 @@ Sample covariance wrappers:
 - `sampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_rowSqNorm_bound_with_neg_square_adapters_of_troppPrimitives`
 - `SampleCovarianceTailUsage.SampleCovarianceTailAssumptions`
 - `SampleCovarianceTailUsage.SampleCovarianceOperatorNormTailAssumptions`
+- `SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_quadraticForm_tail_usage`
+- `SampleCovarianceTailUsage.sampleCovariance_exactRow_centeredSquare_operatorNorm_tail_usage`
 
 Sample covariance negative-side provider-transfer adapters:
 
@@ -264,7 +266,7 @@ Low-level prefix/state, reindex, negative-family, nullspace/decomposition, exact
   hypotheses.
 - `StatementRoutes` is an examples-only route index; it groups representative example-level statement families without adding core API. Lower-level bridge and frontier checks belong in source, tests, and judge files rather than separate reader-facing examples.
 - Positive-threshold operator-norm routes use `0 < t`; the zero-dimensional `t = 0` endpoint is not part of that route.
-- Sample covariance wrappers remain conditional APIs, not unconditional concentration theorems. The positive-side quadratic-form route and the two-sided/operator-norm route now have exact-row variance-proxy wrappers, plus centered-square-chain variants that replace sample-specific sharp-chain premises by generic centered-square-chain premises. The named negative sample-covariance family has an exact-row variance-proxy provider. The preferred sample-covariance example route now uses Tropp-only wrappers that fill pointwise Bernstein CFC fields with `bernsteinMatrixExp_le_quadratic`; explicit-CFC wrappers remain compatibility surfaces.
+- Sample covariance wrappers remain conditional APIs, not unconditional concentration theorems. The positive-side quadratic-form route and the two-sided/operator-norm route now have exact-row variance-proxy wrappers, plus centered-square-chain variants that replace sample-specific sharp-chain premises by generic centered-square-chain premises. The named negative sample-covariance family has an exact-row variance-proxy provider. The preferred sample-covariance example route now uses Tropp-only wrappers that fill pointwise Bernstein CFC fields with `bernsteinMatrixExp_le_quadratic`; it also includes exact-row centered-square bundle usage examples. Explicit-CFC wrappers remain compatibility surfaces.
 - Negative-side provider-transfer adapters only move explicit opposite-parameter
   assumptions onto the named negative sample-covariance family; they do not
   prove exponential integrability, trace-exponential integrability, or CFC. The

docs/TODO.md

@@ -17,8 +17,8 @@ This is the active short list. Old completed task logs were collapsed into
   Matrix Bernstein proofs.
 - Prefer shared RandomMatrix APIs over unfolded formulas in examples, tests,
   judge files, and docs.
-- Current RandomMatrix hardbone branch: assumption-bundle follow-up for
-  `RM-natural-state-centered-square-wrapper-assumption-bundling-contract`.
+- Current RandomMatrix hardbone branch: example-usage follow-up for
+  `RM-SC-centered-square-bundle-example-usage-contract`.
 - The centered-square-chain wrapper variants are available for both the
   positive-side quadratic-form route and the two-sided/operator-norm route;
   natural assumption bundles now package those exact-row routes without

docs/TestPlan.md

@@ -42,7 +42,7 @@ git diff --check
   `HighDimProbTest/RandomMatrixHardboneStatementsAPI.lean`,
   `HighDimProbJudge/RandomMatrix/TraceExpUse.lean`.
 - RandomMatrix sample-covariance negative-side provider-transfer adapters and
-  CFC-free sample-covariance wrappers, including the positive-side exact-row variance-proxy quadratic-form wrapper, its centered-square-chain variant and assumption bundle, the two-sided/operator-norm exact-row wrappers, their centered-square assumption bundle, and the negative exact-row variance-proxy provider, are covered in
+  CFC-free sample-covariance wrappers, including the positive-side exact-row variance-proxy quadratic-form wrapper, its centered-square-chain variant and assumption bundle, the example usage route for that bundle, the two-sided/operator-norm exact-row wrappers, their centered-square assumption bundle and example usage route, and the negative exact-row variance-proxy provider, are covered in
   `HighDimProbTest/RandomMatrixConcentrationAPI.lean`,
   `HighDimProbTest/ExamplesAPI.lean`, and
   `HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean`.