Skip to content

feat(lean): port native gates and nonlinear phase-fold proof - #19

Merged
barghouthi merged 1 commit into
mainfrom
codex/native-controlled-gates
Sep 23, 2026
Merged

barghouthi merged 1 commit into
mainfrom
codex/native-controlled-gates

Conversation

@barghouthi

Copy link
Copy Markdown
Collaborator

Summary

  • Port native CCX, CCZ, and CZ optimization and exact decomposition to Lean, with gate-aware MURM synthesis bases.
  • Connect randomized nonlinear phase folding to packed GF(2^128) arithmetic and prove the executable transfer, refinement, and failure bound.
  • Port gate, pipeline, QASM, and PhaseFold tests, including opt-in slow parity cases.

Verification

  • lake build
  • lake build TzapLean.PhaseFoldSlowTests

This PR contains only the Lean commit; new planning and test-report Markdown files remain untracked.

@barghouthi
barghouthi merged commit 74b4998 into main Sep 23, 2026
20 of 21 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