Expose natural-state provider tail route#33
Closed
freezed-corpse-143 wants to merge 1 commit into
Closed
Conversation
Package the S16 tail wrapper as a public route over the existing provider-assumption record while keeping the S15 conditioning contract explicit. Constraint: S15 audit leaves history/current conditioning as explicit assumptions until a sigma-algebra independence bridge is proved. Rejected: compress ordinary iIndepFun into the conditional step contract | it would overstate the available conditioning theorem. Confidence: high Scope-risk: moderate Directive: Do not market this wrapper as full Matrix Bernstein or as closing Epstein/Lieb/Tropp one-step. Tested: lake build HighDimProb.RandomMatrix.ConcentrationStatements; lake env lean HighDimProbTest/RandomMatrixLiebProviderAPI.lean; lake env lean HighDimProbJudge/RandomMatrix/LiebProviderUse.lean; python scripts/judge_policy_check.py; python .github/scripts/check_text_quality.py; git diff --check; lake test; lake build; lake build HighDimProbJudge. Not-tested: Provider S14 derivative primitives live in the separate HighDimProbLiebProvider repository.
Owner
|
Thanks for the careful provider-route work here. The useful S16 natural-state tail wrapper surface has now been manually integrated and refactored into main in 7413583 (Integrate Lieb provider bridge layer), along with the corresponding tests, judge check, and docs. I'm closing this stacked PR rather than merging the old branch because the final main version keeps the provider/core API split and avoids reintroducing older abstraction/doc structure. |
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
matrixBernsteinQuadraticFormUpperTail_of_naturalStateProviderAssumptionsas a public-friendly S16 wrapper over the existing conditioning-trace-MGF provider assumptions.#checksurfaces.docs/STATEMENTS.md,docs/RandomMatrixAPI.md,docs/Status.md, anddocs/TestPlan.md.Scope
This is an API/assumption-compression route only. It keeps the hard conditioning assumptions explicit and does not claim full Matrix Bernstein, Epstein affine-line concavity, Lieb, or Tropp one-step closure.
Stacking
Stacked on
rm-lieb-provider-theorem-push/ PR #32.Testing
lake build HighDimProb.RandomMatrix.ConcentrationStatementslake env lean HighDimProbTest/RandomMatrixLiebProviderAPI.leanlake env lean HighDimProbJudge/RandomMatrix/LiebProviderUse.leanpython scripts/judge_policy_check.pypython .github/scripts/check_text_quality.pygit diff --checklake testlake buildlake build HighDimProbJudge