Repository navigation

feat(Probability): pair and tail estimates for frame-conditioned retention channels - #1710

Merged

SamuelSchlesinger merged 40 commits into

cslib-community:mainfrom

chris-ai1:feat/frame-retention-1444

Oct 31, 2026

Merged

feat(Probability): pair and tail estimates for frame-conditioned retention channels#1710
SamuelSchlesinger merged 40 commits into
cslib-community:mainfrom
chris-ai1:feat/frame-retention-1444

Commits on Oct 29, 2026
- chore(deps): track CSLib main and Lean rc2
  SamuelSchlesinger
  committed
  888918d
- refactor(probability): use generic infinite-sum lemmas
  SamuelSchlesinger
  committed
  9a1b754
- fix(build): adapt proofs to the rc2 Mathlib API
  SamuelSchlesinger
  committed
  d7dcd79
- Merge remote-tracking branch 'origin/main' into work/cslib-rc2-sync-1648-codex
  SamuelSchlesinger
  committed
  7925011
- test(quantum): qualify the protected matrix lemma
  SamuelSchlesinger
  committed
  f5a70cb
- fix(build): normalize goals before proof automation
  SamuelSchlesinger
  committed
  bb3e910
- Merge commit '96fd02a85579bbbce97c02110ed80da02684cb2e' into work/cslib-rc2-sync-1648-codex
  SamuelSchlesinger
  committed
  0d38523
- feat(Foundations): correction factorization and reward transport for transition matrices
  
  chris-ai1
  and
  claude
  committed
  7085d68
- fix(Foundations): expose IsStrictUpperTriangular so importers can apply it
  
  chris-ai1
  and
  claude
  committed
  832f939
- fix(Foundations): separate row-sum control from nonnegativity; add reward lower bound
  
  chris-ai1
  and
  claude
  committed
  1fbc267
- feat(Foundations): factorial truncation of cutoff corrections
  
  chris-ai1
  and
  claude
  committed
  b5cc059
- refactor(Foundations): use Nat.sum_Icc_choose for the hockey-stick step
  
  chris-ai1
  and
  claude
  committed
  6e0388d
- doc(Foundations): count chains with the integer support size
  
  chris-ai1
  and
  claude
  committed
  8b3f572
- feat(Probability): retention by pairwise independent hashing (#1444)
  
  chris-ai1
  and
  claude
  committed
  14714b9
- feat(Foundations): one stage of the correction-and-copy hierarchy
  
  chris-ai1
  and
  claude
  committed
  7fd99bc
- feat(Probability): affine retention channels over a prime field (#1682)
  
  chris-ai1
  and
  claude
  committed
  4943d9b
Commits on Oct 30, 2026
- Merge #1676 (1fbc2671) into the #1653 rc2 pin (0d38523e)
  
  chris-ai1
  and
  claude
  committed
  7050537
- fix(Foundations): qualify Matrix apply lemmas for the rc2 Mathlib API
  
  chris-ai1
  and
  claude
  committed
  ea663ce
- Merge #1677 (8b3f5725) into rc2-refresh/1676
  
  chris-ai1
  and
  claude
  committed
  2283aa2
- feat(Foundations): copy stages preserve strict upper triangularity
  
  chris-ai1
  and
  claude
  committed
  ed3268e
- fix(Foundations): qualify Matrix apply lemmas in FactorialTruncation for rc2
  
  chris-ai1
  and
  claude
  committed
  19cf8a8
- refactor(Foundations): general copySplit_isStrictUpperTriangular beside copySplit
  
  chris-ai1
  and
  claude
  committed
  35dd78f
- feat(Probability): frame-conditioned channels, validated variants and conditional averaging (#1682)
  
  chris-ai1
  and
  claude
  committed
  53de6a3
- feat(Foundations): pilot with step-dependent multipliers and probabilistic column detectors
  
  chris-ai1
  and
  claude
  committed
  f1303d9
- refactor(Foundations): derive fixed-multiplier iterate bounds from IsCorrectionSeq
  
  chris-ai1
  and
  claude
  committed
  80b604b
- Merge #1688 (feat/retention-channel-1444) into feat/detectors-affine-1444
  
  chris-ai1
  and
  claude
  committed
  a7541c6
- feat(Probability): affine retention channels satisfy the detector interface
  
  chris-ai1
  and
  claude
  committed
  0fd3e72
- Merge remote-tracking branch 'fork/feat/conditional-averaging-1444' into feat/frame-retention-1444
  chris-ai1
  committed
  42665b4
- Merge remote-tracking branch 'origin/main' into feat/frame-retention-1444
  chris-ai1
  committed
  24f9218
- Merge remote-tracking branch 'fork/rc2-refresh/1677' into feat/frame-retention-1444
  chris-ai1
  committed
  4389a4d
- fix(Foundations): qualify Matrix apply lemmas in CopyStage and PilotCorrection for rc2
  
  chris-ai1
  and
  claude
  committed
  34406a0
- feat(Probability): pair and tail estimates for frame-conditioned retention channels
  
  chris-ai1
  and
  claude
  committed
  e6b8537
- Merge supported main into the reviewed detector stage
  SamuelSchlesinger
  committed
  e101d8e
- fix(Foundations): qualify Matrix apply lemmas in CopyStage and PilotCorrection for rc2
  
  authored and
  SamuelSchlesinger
  committed
  9151713
- Merge refreshed #1696 (main 311e9841 + rc2 repair) into feat/detectors-affine-1444
  
  chris-ai1
  and
  claude
  committed
  5a64396
- Merge origin/main into feat/conditional-averaging-1444
  
  chris-ai1
  and
  claude
  committed
  ae99b48
- Merge refreshed #1698 (5a6439697) into feat/frame-retention-1444
  
  chris-ai1
  and
  claude
  committed
  3586bea
- Merge refreshed #1691 (ae99b483b) into feat/frame-retention-1444
  
  chris-ai1
  and
  claude
  committed
  eb8ee8e
Commits on Oct 31, 2026
- Merge origin/main into feat/frame-retention-1444
  
  SamuelSchlesinger
  and
  claude
  committed
  5d6d647
- Merge origin/main into feat/frame-retention-1444
  
  SamuelSchlesinger
  and
  claude
  committed
  6891006

Commits

Commits on Oct 29, 2026

Commits on Oct 30, 2026

Commits on Oct 31, 2026