Expose sample-covariance wrappers after CFC hardbone#17
Merged
dududuguo merged 1 commit intoJun 19, 2026
Conversation
Add narrow sample-covariance entry points that fill the pointwise Bernstein CFC premise with the proved bernsteinMatrixExp_le_quadratic leaf while keeping Tropp/Lieb, integrability, and variance-proxy assumptions explicit. Migrate example bundles off public cfcPrimitive fields and extend API/judge/docs coverage for the preferred conditional surface. Constraint: RM-HB-sample-covariance-cfc-free-wrapper-contract only removes caller-supplied pointwise CFC obligations; it must not claim Tropp/Lieb, Golden-Thompson, trace-exp providers, full Matrix Bernstein, or unconditional sample-covariance concentration. Rejected: Proving new analytic Tropp/Lieb or integrability leaves | outside this wrapper-contract scope and unsupported by the current theorem surface. Confidence: high Scope-risk: moderate Directive: Preserve explicit-CFC compatibility wrappers and keep future docs honest about remaining analytic assumptions. Tested: lake env lean HighDimProb/RandomMatrix/ConcentrationStatements.lean; lake env lean HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.lean; lake env lean HighDimProb/Examples/RandomMatrix/BoundedRowSampleCovarianceOperatorNormUsage.lean; lake env lean HighDimProbTest/RandomMatrixConcentrationAPI.lean; lake env lean HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean; lake env lean HighDimProbTest/ExamplesAPI.lean; lake build HighDimProbJudge; lake build HighDimProb.Examples; lake test; lake build; python scripts/judge_policy_check.py; python .github/scripts/check_text_quality.py; git diff --check; independent code-reviewer APPROVE; architect CLEAR. Not-tested: GitHub PR checks not run locally.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
bernsteinMatrixExp_le_quadratic.cfcPrimitivefields while keeping Tropp/Lieb and integrability assumptions explicit.Motivation
This completes
RM-HB-sample-covariance-cfc-free-wrapper-contract: after the Bernstein CFC hardbone leaf is proved, callers should not need to supply pointwise Bernstein CFC fields for the sample-covariance wrapper route.Scope
Testing
lake env lean HighDimProb/RandomMatrix/ConcentrationStatements.leanlake env lean HighDimProb/Examples/RandomMatrix/SampleCovarianceTailUsage.leanlake env lean HighDimProb/Examples/RandomMatrix/BoundedRowSampleCovarianceOperatorNormUsage.leanlake env lean HighDimProbTest/RandomMatrixConcentrationAPI.leanlake env lean HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.leanlake env lean HighDimProbTest/ExamplesAPI.leanlake build HighDimProbJudgelake build HighDimProb.Exampleslake testlake buildpython scripts/judge_policy_check.pypython .github/scripts/check_text_quality.pygit diff --check