Repository navigation

feat(Foundations): constants and the iterated correction-and-copy hierarchy with its stage bound - #1702

Merged

SamuelSchlesinger merged 22 commits into

cslib-community:mainfrom

chris-ai1:feat/hierarchy-constants-1444

Oct 30, 2026

Merged

feat(Foundations): constants and the iterated correction-and-copy hierarchy with its stage bound#1702
SamuelSchlesinger merged 22 commits into
cslib-community:mainfrom
chris-ai1:feat/hierarchy-constants-1444

Commits on Oct 29, 2026
- 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(Foundations): one stage of the correction-and-copy hierarchy
  
  chris-ai1
  and
  claude
  committed
  7fd99bc
Commits on Oct 30, 2026
- feat(Foundations): copy stages preserve strict upper triangularity
  
  chris-ai1
  and
  claude
  committed
  ed3268e
- refactor(Foundations): general copySplit_isStrictUpperTriangular beside copySplit
  
  chris-ai1
  and
  claude
  committed
  35dd78f
- 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
- feat(Foundations): constants of the correction-and-copy hierarchy
  
  chris-ai1
  and
  claude
  committed
  5d3394d
- feat(Foundations): the iterated correction-and-copy hierarchy and its stage bound
  
  chris-ai1
  and
  claude
  committed
  892f45c
- doc(Foundations): document every HierarchyParams field
  
  chris-ai1
  and
  claude
  committed
  4a207ab
- doc(Foundations): clarify reduced hierarchy parameter scope
  SamuelSchlesinger
  committed
  e136883
- Merge supported main into correction hierarchy
  SamuelSchlesinger
  committed
  6392301
- fix(Foundations): qualify Matrix apply lemmas for the rc2 Mathlib API
  
  authored and
  SamuelSchlesinger
  committed
  4014d0c
- Merge supported correction parent into factorial truncation
  SamuelSchlesinger
  committed
  a6e69b7
- fix(Foundations): qualify Matrix apply lemmas in FactorialTruncation for rc2
  
  authored and
  SamuelSchlesinger
  committed
  b0b0005
- Merge commit 'b0b00058c5845fb44ba7f50f5ec33bf3764cacd9' into work/hierarchy-fixes-1702-codex-20261030
  SamuelSchlesinger
  committed
  cbc2615
- fix(Foundations): qualify Matrix apply lemmas in CopyStage and PilotCorrection for rc2
  
  authored and
  SamuelSchlesinger
  committed
  f7f51f7
- chore(probability): merge current main into the hierarchy constants
  SamuelSchlesinger
  committed
  f6ad6fb

Commits

Commits on Oct 29, 2026

Commits on Oct 30, 2026