Skip to content

feat(univariate): Cantor-Zassenhaus linear-factor splitter and root finder #252

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
DimitriosMitsios wants to merge 21 commits into
base: master
Choose a base branch
from
Open

feat(univariate): Cantor-Zassenhaus linear-factor splitter and root finder #252

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
d2bf4bb
feat(univariate): Cantor–Zassenhaus linear-factor splitter (algorithm…
DimitriosMitsios Jun 9, 2026
7ecc4a9
feat(univariate): CZ shifted modexp evaluation (eval_shiftedPowModWith)
DimitriosMitsios Jun 9, 2026
da2a055
feat(univariate): CZ quadratic-residue routing lemma
DimitriosMitsios Jun 9, 2026
30a889a
feat(univariate): CZ root-isolation lemma (gcd with linear factor)
DimitriosMitsios Jun 9, 2026
d6286ca
feat(univariate): CZ monicNormalize_linearFactor
DimitriosMitsios Jun 9, 2026
ebd6b29
feat(univariate): CZ base emit lemma + represented-factor helpers
DimitriosMitsios Jun 9, 2026
9b53c29
feat(univariate): CZ completeness over prime fields (czComplete)
DimitriosMitsios Jun 9, 2026
0b02ae8
feat(univariate): package CZ splitter (czLinearFactorProductSplitter)
DimitriosMitsios Jun 9, 2026
8d0fc9d
feat(univariate): CZ completeness over ZMod prime fields (czComplete_…
DimitriosMitsios Jun 9, 2026
f5a0fc7
test(univariate): Cantor-Zassenhaus splitter regression tests over ZM…
DimitriosMitsios Jun 9, 2026
fcb16ce
docs(univariate): refine CZ docstrings (concise, completeness proved)
DimitriosMitsios Jun 9, 2026
25be967
refactor(univariate): flatten CZ completeness statements via HasRootF…
DimitriosMitsios Jun 10, 2026
6768320
chore(univariate): author name Dimitris in CZ files
DimitriosMitsios Jun 10, 2026
2f1f85e
feat(univariate): end-to-end CZ root finder czRoots over ZMod q
DimitriosMitsios Jun 10, 2026
48d466b
docs(univariate): tighten CZ docstrings to state-what-not-how
DimitriosMitsios Jun 11, 2026
f766784
docs(test): tighten CZ test section comments
DimitriosMitsios Jun 11, 2026
6571491
docs(univariate): clarify short-schedule completeness is future work
DimitriosMitsios Jun 11, 2026
667dc37
style(univariate): use maps-to arrow (fun x ↦) in CZ lambdas
DimitriosMitsios Jun 12, 2026
9141508
Merge branch 'master' into cz-root-finding
DimitriosMitsios Jun 12, 2026
b467d9e
Merge branch 'master' into cz-root-finding
DimitriosMitsios Jun 27, 2026
7165a41
Merge branch 'master' into cz-root-finding
alexanderlhicks Jul 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CompPoly.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -219,6 +219,7 @@ import CompPoly.Univariate.ReedSolomon.GaoCorrectness
import CompPoly.Univariate.ReedSolomon.GaoDecoder
import CompPoly.Univariate.Roots
import CompPoly.Univariate.Roots.Backend
import CompPoly.Univariate.Roots.CantorZassenhaus
import CompPoly.Univariate.Roots.Context
import CompPoly.Univariate.Roots.Correctness
import CompPoly.Univariate.Roots.Enumeration
Expand Down
Loading
Loading