Skip to content

Add rank-one operator norm boundedness bridge#8

Merged
dududuguo merged 1 commit into
mainfrom
rm-rank-one-operator-norm-bound
Jun 13, 2026
Merged

Add rank-one operator norm boundedness bridge#8
dududuguo merged 1 commit into
mainfrom
rm-rank-one-operator-norm-bound

Conversation

@freezed-corpse-143

Copy link
Copy Markdown
Collaborator

Summary

  • add rankOneOperatorNorm_le_vectorSqNorm for ||v vᵀ||op <= ||v||₂²
  • add pointwise rank-one wrappers for BoundedOperatorNorm and PointwiseOperatorNormBound
  • add API/judge coverage and sync RandomMatrix planning docs to RM-centered-operator-norm-bound

Scope

  • proves only the rank-one operator-norm boundedness bridge
  • does not prove centered summand bounds, vector-to-matrix measurability/integrability, PSD nullspace converse, lambda-max/operator-norm Matrix Bernstein tails, Tropp/Lieb, Bernstein CFC, Golden-Thompson, or full Matrix Bernstein

Testing

  • lake build
  • lake test
  • lake build HighDimProbJudge
  • python scripts/judge_policy_check.py
  • git diff --check
  • forbidden-token scan over HighDimProb, HighDimProbTest, HighDimProbJudge

Constraint: local workflow required theory extraction, Plan-Execute, review gates, and docs sync before closeout

Rejected: bundle centered bounds, measurability, integrability, or PSD nullspace converse | kept this PR to one concept cluster

Confidence: high

Scope-risk: narrow

Directive: next safe task is RM-centered-operator-norm-bound

Tested: lake build; lake test; lake build HighDimProbJudge; python scripts/judge_policy_check.py; git diff --check

Not-tested: upstream CI
@dududuguo dududuguo merged commit 37c3e56 into main Jun 13, 2026
4 checks passed
@dududuguo dududuguo deleted the rm-rank-one-operator-norm-bound branch June 13, 2026 13:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants