Bridge exact-row variance proxies to centered-square wrappers#22
Merged
Conversation
added 2 commits
June 20, 2026 05:30
Add a narrow hardbone bridge that lets exact-row sample-covariance variance-proxy consumers depend on the generic centered-square chain while preserving explicit Tropp/Lieb and Matrix Bernstein boundaries. Constraint: Keep theorem boundaries honest; generic centered-square chain and Tropp/Lieb primitives remain explicit. Rejected: Proving a full hardbone sharp-chain or Matrix Bernstein theorem | would broaden the verified contract beyond available leaves. Confidence: high Scope-risk: moderate Directive: Do not treat these wrappers as unconditional concentration theorems; downstream wrappers must keep missing analytic primitives explicit. Tested: lake env lean HighDimProb/RandomMatrix/HardboneStatements.lean; lake build HighDimProb.RandomMatrix.HardboneStatements; API/judge focused checks; python .github/scripts/check_text_quality.py; python scripts/judge_policy_check.py; git diff --check; lake build HighDimProbJudge; lake test; lake build Not-tested: GitHub Actions after PR creation
Route sample-covariance tail wrappers through the generic centered-square variance-proxy chain while preserving explicit Tropp and analytic premises.\n\nConstraint: Keep generic centered-square chain, Tropp/Lieb, trace-MGF, and Matrix Bernstein boundaries explicit.\nRejected: Proving or hiding the centered-square chain inside tail wrappers | That would overstate the current hardbone boundary.\nConfidence: high\nScope-risk: narrow\nDirective: Future wrappers should derive sample-specific sharp-chain premises before reusing exact-row routes, not duplicate variance-proxy proofs.\nTested: RED unknown identifiers in concentration API and MatrixBernstein judge; lake build HighDimProb.RandomMatrix.ConcentrationStatements; lake env lean HighDimProbTest/RandomMatrixConcentrationAPI.lean; lake env lean HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.lean; python .github/scripts/check_text_quality.py; python scripts/judge_policy_check.py; git diff --check; lake build HighDimProbJudge; lake test; lake build\nNot-tested: GitHub PR checks were not refreshed after this local commit.
freezed-corpse-143
changed the title
9 tasks
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
varianceProxyNormBound_of_centeredSquareChain_statementdirectly for:Motivation
This narrows the remaining exact-row variance-proxy premise surface for sample-covariance routes while keeping theorem boundaries honest. The new wrappers let callers provide the generic centered-square variance-proxy chain over
rankOneRandomMatrixFamily (rowVector A)instead of the sample-specific sharp-chain premise.Scope
sampleCovarianceVarianceProxy_sharp_statement_of_centeredSquareChain_exactRowSqNorm_bound_memLp_twosampleCovarianceVarianceProxy_sharp_of_exactRowSqNorm_bound_memLp_two_of_centeredSquareChainMatrixVarianceProxyNormBound_centeredSampleCovarianceRowRankOneFamilyNeg_of_exactRowSqNorm_bound_memLp_twosampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_troppPrimitivesampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_troppPrimitivessampleCovariance_quadraticForm_tail_optimized_under_exactRowSqNorm_bound_of_centeredSquareChain_of_troppPrimitivesampleCovariance_selfAdjointOperatorNorm_tail_optimized_arbitrary_of_pos_under_exactRowSqNorm_bound_with_neg_square_adapters_of_centeredSquareChain_of_troppPrimitivesBoundary
This PR does not prove Tropp/Lieb, Golden-Thompson, trace-MGF iteration, full Matrix Bernstein, the generic centered-square chain itself, or unconditional sample-covariance concentration. Those hypotheses remain explicit.
Testing
python .github/scripts/check_text_quality.pypython scripts/judge_policy_check.pygit diff --checklake build HighDimProb.RandomMatrix.HardboneStatementslake build HighDimProb.RandomMatrix.ConcentrationStatementslake env lean HighDimProbTest/RandomMatrixHardboneStatementsAPI.leanlake env lean HighDimProbTest/RandomMatrixConcentrationAPI.leanlake env lean HighDimProbJudge/RandomMatrix/TraceExpUse.leanlake env lean HighDimProbJudge/RandomMatrix/VarianceProxyUse.leanlake env lean HighDimProbJudge/RandomMatrix/MatrixBernsteinUse.leanlake build HighDimProbJudgelake testlake buildNotes
Local
.codebase-memory/*generated-file changes were intentionally left uncommitted.