Skip to content

feat(FineGrained): instantiate Lemma 4.8 schedule for CNF sparse parity-design counter (#1226) #1307

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

Merged
SamuelSchlesinger merged 33 commits into from
Oct 27, 2026
Merged

feat(FineGrained): instantiate Lemma 4.8 schedule for CNF sparse parity-design counter (#1226) #1307

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
33 commits
Select commit Hold shift + click to select a range
3ebccd4
feat(Foundations/Data/Polynomial): integer parity amplifier and share…
SamuelSchlesinger Oct 26, 2026
c22f67d
doc(references): pin the subexponential SAT manuscript
SamuelSchlesinger Oct 26, 2026
9384790
refactor(Polynomial): reuse Mathlib helpers and cite OpenAI2026ETH in…
SamuelSchlesinger Oct 27, 2026
f4ccf6c
feat(BooleanAnalysis): sparse F2 equation zero counting, cleared deno…
SamuelSchlesinger Oct 27, 2026
14ea8f8
feat(BooleanAnalysis): univariate parity-product specialization and h…
SamuelSchlesinger Oct 27, 2026
e23f8bf
Merge remote-tracking branch 'origin/main' into feat/parity-amplifier…
SamuelSchlesinger Oct 27, 2026
f731bcd
feat(BooleanAnalysis): add §5.6 shared-precision branch recovery and …
SamuelSchlesinger Oct 27, 2026
4ac3e50
Merge branch 'feat/parity-amplifier-1226-jetski' into feat/sparse-zer…
SamuelSchlesinger Oct 27, 2026
01ba227
refactor(Polynomial,BooleanAnalysis): extract shared CoeffNorm1 and a…
SamuelSchlesinger Oct 27, 2026
a3f6c45
Merge branch 'feat/sparse-zero-count-1226-jetski' into feat/sparse-br…
SamuelSchlesinger Oct 27, 2026
56ff42b
refactor(Polynomial,BooleanAnalysis): extract ParityAmplifierDegree a…
SamuelSchlesinger Oct 27, 2026
bcf6ea4
feat(Foundations/BooleanAnalysis): add cleared-denominator specializa…
SamuelSchlesinger Oct 27, 2026
8728e1f
docs,test(BooleanAnalysis,Polynomial): qualify clearing premises and …
SamuelSchlesinger Oct 27, 2026
514f88e
Merge origin/main into feat/sparse-cleared-specialization-1226-jetski…
SamuelSchlesinger Oct 27, 2026
5be06c8
feat(Foundations/BooleanAnalysis): instantiate cleared parity special…
SamuelSchlesinger Oct 27, 2026
1d6220a
test(BooleanAnalysis): add concrete expected-value and checked branch…
SamuelSchlesinger Oct 27, 2026
06df186
Merge branch 'main' into feat/sparse-replacement-design-1226-jetski
SamuelSchlesinger Oct 27, 2026
f0bdbb0
fix(BooleanAnalysis/SparseReplacementDesign): address #1294 review items
SamuelSchlesinger Oct 27, 2026
fe083e6
Merge remote-tracking branch 'origin/main' into feat/cnf-sparse-desig…
SamuelSchlesinger Oct 27, 2026
3dc9025
doc(BooleanAnalysis): correct replacement degree provenance
SamuelSchlesinger Oct 27, 2026
6fc8e4e
Merge remote-tracking branch 'origin/feat/sparse-replacement-design-1…
SamuelSchlesinger Oct 27, 2026
ffb5db9
feat(Logics/Propositional/CNF): bridge sparse replacement design with…
SamuelSchlesinger Oct 27, 2026
a5f2b8e
Merge remote-tracking branch 'origin/main' into feat/sparse-cnf-desig…
SamuelSchlesinger Oct 27, 2026
e96809c
feat(FineGrained): add Section 6.3 compiled parity-row schedule feasi…
SamuelSchlesinger Oct 27, 2026
dcdef39
feat(FineGrained): instantiate Lemma 4.8 schedule for CNF sparse pari…
SamuelSchlesinger Oct 27, 2026
0d8c600
doc(FineGrained): distinguish equation ratio from source sparsity par…
SamuelSchlesinger Oct 27, 2026
1ed5501
Merge remote-tracking branch 'origin/main' into feat/cnf-sparse-desig…
SamuelSchlesinger Oct 27, 2026
5a8047b
Merge branch 'feat/cnf-sparse-design-counter-1226-jetski' into feat/s…
SamuelSchlesinger Oct 27, 2026
12238fb
Merge remote-tracking branch 'origin/feat/sparse-parity-schedule-1226…
SamuelSchlesinger Oct 27, 2026
b0323d2
refactor(FineGrained): consume SparseParitySchedule in SparseCNFDesig…
SamuelSchlesinger Oct 27, 2026
82300cf
Merge remote-tracking branch 'origin/main' into feat/sparse-cnf-desig…
SamuelSchlesinger Oct 27, 2026
bf7c87a
test(FineGrained): exercise recovery conclusions on nonzero parity ro…
SamuelSchlesinger Oct 27, 2026
fff00ef
Merge remote-tracking branch 'origin/main' into feat/sparse-cnf-desig…
SamuelSchlesinger Oct 27, 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 Complexity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -777,6 +777,7 @@ public import Complexity.Computability.Complexity.FineGrained.ReplacementSchedul
public import Complexity.Computability.Complexity.FineGrained.Schoening
public import Complexity.Computability.Complexity.FineGrained.SparseBranchAsymptotics
public import Complexity.Computability.Complexity.FineGrained.SparseBranchSchedule
public import Complexity.Computability.Complexity.FineGrained.SparseCNFDesignSchedule
public import Complexity.Computability.Complexity.FineGrained.SparseCountingScale
public import Complexity.Computability.Complexity.FineGrained.SparseParitySchedule
public import Complexity.Computability.Complexity.FineGrained.Sparsification
Expand Down
Loading
Loading