Skip to content

feat(lean): randomize phase folding - #17

Merged
barghouthi merged 1 commit into
mainfrom
codex/randomized-phase-fold
Sep 8, 2026
Merged

barghouthi merged 1 commit into
mainfrom
codex/randomized-phase-fold

Conversation

@barghouthi

Copy link
Copy Markdown
Collaborator

Summary

  • model phase folding as a RandPass over uniform finite samples
  • prove the failure event is bounded by the affine-tag collision probability
  • draw fresh 128-bit tags from the OS in the executable pipeline
  • compose randomized passes and fixpoint rounds with conditional fresh seeds
  • remove the exact phase-fold fallback so PhaseFoldRand is the default implementation

Verification

  • lake build (5269 jobs)
  • PhaseFoldRand CLI smoke test
  • git diff --check

Model phase folding as a randomized pass with a machine-checked collision bound. Use fresh OS randomness in the executable pipeline and remove the exact phase-fold fallback.
@barghouthi
barghouthi merged commit 2c29be4 into main Sep 8, 2026
20 checks passed
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.

1 participant