feat(PH): the Sipser-Lautemann theorem - #29

Merged

SamuelSchlesinger merged 23 commits into

SamuelSchlesinger:devfrom

BoltonBailey:feat/sipser-lautemann

Aug 30, 2026

Commits on Jul 24, 2026

feat(Classes): define the polynomial hierarchy

BoltonBailey
and
claude
committed
0cd989d

Commits on Jul 25, 2026

Commits on Aug 1, 2026

Merge branch 'feat/bitstring-encoding' into feat/polynomial-hierarchy
BoltonBailey
committed
8d5fb7e

Commits on Aug 14, 2026

Commits on Aug 16, 2026

Commits on Aug 19, 2026

feat(PH): state the Sipser-Lautemann theorem

BoltonBailey
and
claude
committed
0b2b8e2
feat(PH): prove Sipser-Lautemann from one simulation interface

BoltonBailey
and
claude
committed
064579a
feat(models): run one nondeterministic path from a choice tape

BoltonBailey
and
claude
committed
1c3f232
feat(P): decide a language by a polynomial-time verdict function

BoltonBailey
and
claude
committed
1a677f7
docs(roadmap): record the sharpened Sipser-Lautemann obligation

BoltonBailey
and
claude
committed
dd01f04
feat(cobham): encode and iterate a nondeterministic path in the algebra

BoltonBailey
and
claude
committed
1af04f8
feat(cobham): compute a nondeterministic path's verdict in the algebra

BoltonBailey
and
claude
committed
0733312
feat(PH): close the pairFst seam, making the level inclusions unconditional

BoltonBailey
and
claude
committed
8a53f56
feat(cobham): polynomial lengths, length tests, and exclusive-or in the algebra

BoltonBailey
and
claude
committed
de8993f
feat(cobham): block loops for the amplified verdict

BoltonBailey
and
claude
committed
0f1f3be
feat(PH): prove the Sipser-Lautemann theorem

BoltonBailey
and
claude
committed
dd35c35
docs(PH): flag the Sipser-Lautemann development as unreviewed

BoltonBailey
and
claude
committed
af6a8d9
Merge remote-tracking branch 'origin/dev' into boltonbailey-dev
BoltonBailey
committed
e511e68

Commits on Aug 30, 2026

Merge remote-tracking branch 'origin/dev' into feat/sipser-lautemann
BoltonBailey
committed
bde2acd