feat(PH): the polynomial hierarchy and the Sipser-Lautemann theorem - #28
Closed
BoltonBailey wants to merge 21 commits into
Closed
feat(PH): the polynomial hierarchy and the Sipser-Lautemann theorem#28BoltonBailey wants to merge 21 commits into
BoltonBailey wants to merge 21 commits into
Conversation
Define certificate quantifiers over the pair codec (polyExistsLang / polyForallLang and their class operators), the levels SigmaP / PiP by the standard recursion through complement classes, and PH as their union. Prove quantifier and class-level complement duality, monotonicity, the recursion laws, and level inclusions, the latter conditional on the single machine-engineering seam `pairFst ∈ FP` (first-component pair decoding), isolated as a hypothesis following the WitnessNTMConstruction pattern. Ported from leanprover/cslib#192, re-proved against this library's machine model and Set-based languages. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
# Conflicts: # Complexitylib/Classes.lean
State `BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ` against the library's concrete `BPP` and the certificate-quantifier levels `SigmaP`/`PiP`, packaged as the `Prop`-valued `SipserLautemann` so downstream results can be proved against it before the probabilistic argument lands. Adds the unconditional consequences: the split into halves, the reduction of the statement to its `Σ₂` half given closure of `BPP` under complement, and `BPP ⊆ PH`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Reduce `BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ` to a single machine-engineering interface, `MatrixInP`, and prove every other step unconditionally: - `SipserLautemann.Covering`: Lautemann's covering lemma in both directions — a union bound over shifted translates of an event in the seed space gives covering shifts when the event is large, and a cardinality bound rules them out when it is small. - `SipserLautemann.TimeBound`: the acceptance probability is frozen past the halting time, so a machine's arbitrary time bound may be replaced by a dominating polynomial. This is what makes the matrix predicate computable. - `SipserLautemann.Amplified`: majority amplification plus the covering lemma give `x ∈ L ↔ ∃ shifts, ∀ seeds, some shift accepts`, and the complementary form for `x ∉ L`, which yields the `Π₂` half without needing closure of `BPP` under complement. - `SipserLautemann.Encode`: bitstring codecs for seeds and shift tuples. - `SipserLautemann.Matrix`: the quantifier-free matrix as a language of encoded triples, and the identity exhibiting `L` and `Lᶜ` as polynomially bounded `∃∀` forms over it. `MatrixInP` — the matrix language is decidable in deterministic polynomial time — is the same NTM-path-simulation construction already deferred by `NP.WitnessNTMConstruction`, and is isolated rather than assumed silently. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`NTM.choiceTM` appends a choice tape to an NTM and reads one bit per step from it, writing it back unchanged and advancing that head, which turns the nondeterministic machine into a deterministic one whose run is the chosen path. `NTM.choiceTM_simulates` proves the exact correspondence: a `T`-step run is `tm.trace T` along the bits found on the tape, stopping early exactly when the path halts. This is the primitive a deterministic decider needs in order to evaluate "does `tm` accept `x` along choice sequence `c`" — the missing ingredient behind both `NP.WitnessNTMConstruction` and the `MatrixInP` interface of the Sipser-Lautemann development. Also adds `TM.stepCfg` and `TM.step_of_not_halted`, the non-halted step unfolding used throughout the correspondence proof. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`mem_P_of_decisionFn` and `mem_P_of_decisionFn_bool` put a language in `P` given a verdict function in `FP`, by reading the verdict through `Language.containsOne` and closing under polynomial-time preimages. Adds the `mem_containsZero`/`mem_containsOne` membership lemmas this needs. This lets a development establish membership in `P` by exhibiting a function — in particular by building one in Cobham's algebra via `CobhamFP_eq_FP` — instead of constructing a decider machine by hand. Uses it to sharpen the Sipser-Lautemann interface: `MatrixVerdictInFP` states the remaining obligation as a function in `FP`, `matrixInP_of_verdictInFP` converts it to `MatrixInP`, and `sipserLautemann_of_verdictInFP` gives the theorem from it. `Lautemann.matrixVerdict` is the verdict function, with `mem_matrixLang_iff_verdict` tying it to the matrix language. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The remaining obligation is now `MatrixVerdictInFP`, a function-level statement dischargeable inside Cobham's algebra, and the path semantics it needs are available from `NTM.choiceTM_simulates`. Records the concrete remaining piece: an initial-configuration encoder that places the choice string on the choice tape. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Simulating one path of an NTM inside Cobham's algebra needs a starting configuration with the choice string already on the choice tape. This adds that encoder and the correspondence lemmas: - `Cobham.choiceCfg` / `Cobham.choiceTape` — the starting configuration of `NTM.choiceTM tm`, with the choice head parked on the first bit; - `Cobham.initChoiceFn` with `initChoiceFn_mem` and `initChoiceFn_eq` — the encoder is in the algebra and computes `cfgCode` of that configuration; - `Cobham.iterate_stepFn_choice` — iterating the algebra's step function tracks the deterministic run, with the start-marker and head-position invariants proved for choice runs; - `Cobham.dropChoice_runCfg_choiceCfg` — that run is exactly `tm.trace` along the bits of the choice string, via `NTM.choiceTM_simulates`. Next: iterate under a clock inside the algebra and read the verdict off the final configuration, giving the path verdict in `FP`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Completes the in-algebra simulation of one nondeterministic path: - `Cobham.runChoiceFn` iterates the encoded step function once per bit of the choice string, with `runChoiceFn_mem` placing it in the algebra via the bounded-iteration combinator; - `Cobham.outPairChoiceFn` rewinds the output tape and `Cobham.acceptChoiceFn` reads the verdict off the final configuration — the state block against the halt state's code, and the first output cell against the code for `1`; - `Cobham.acceptChoiceFn_eq_true_iff` proves that verdict is exactly `Cobham.PathAccepts`: after `|c|` steps along the choice bits of `c`, the machine has halted with `1` on the first output cell. With `acceptChoiceFn_mem` this gives the path verdict as a member of Cobham's algebra, hence in `FP` by `CobhamFP_eq_FP`, with no machine construction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…tional `Cobham.fstBlock` is the payload scanner of Cobham's algebra and `Cobham.fstBlock_mem_FP` already proves it polynomial-time. Defining `pairFst` as that scanner discharges the `pairFst ∈ FP` hypothesis the polynomial hierarchy's inclusions were stated against, so `P_subset_polyExistsClass_P`, `P_subset_polyForallClass_P`, `SigmaP_subset_SigmaP_succ` and `PiP_subset_PiP_succ` are now unconditional. Only `pairFst`'s behaviour on canonical pairs is used, and `pairFst_pair` is unchanged; the scanner differs from the old definition only on malformed input, where it returns the bits decoded so far rather than the empty string. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…he algebra Three utilities the matrix computation needs, all machine-free: - `Cobham.polyLen` — for any `Polynomial ℕ`, a member of the algebra whose output has exactly the polynomial's value as its length, by Horner's scheme through `smash` (which multiplies lengths) and concatenation (which adds them); - `Cobham.lenLeFlag` / `Cobham.lenEqFlag` — length comparison flags, a drop followed by an emptiness test; - `Cobham.xorSuffix` — bitwise exclusive-or of a string with the matching suffix of a second string, as one limited recursion whose step reads the paired bit of the second argument through a ruler cut to the right width; `xorSuffix_eq_zipWith_of_length` identifies it with the pointwise operation on equal-length strings. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both loops of the amplified acceptance test, as limited recursions over a ruler whose length is the iteration count — the block index at each step is the length of the remaining tail, so no state is threaded through: - `Cobham.acceptCountAux` counts, in unary, the blocks of a seed on which the path accepts, with `acceptCountAux_length` identifying the count and `acceptCountAux_mem` placing it in the algebra; - `Cobham.majorityFlag` and `Cobham.verdictFlag` turn that count into the amplified majority verdict (or its negation), with `majorityFlag_eq_true_iff`; - `Cobham.anyShiftAux` takes the disjunction of the verdict over the shift blocks of the witness, with `anyShiftAux_eq_true_iff` identifying it with an existential over shift indices. Also adds `orBit_flag` and `orBit_length` to the flag API. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
`BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ` is now unconditional: `Complexity.sipserLautemann`, with `BPP_subset_SigmaP_two`, `BPP_subset_PiP_two` and `BPP_subset_PH`. The last interface, `MatrixVerdictInFP`, is discharged by computing the matrix verdict inside Cobham's algebra — no machine construction: - `SipserLautemann.Verdict` builds the rulers (per-trial step count, trial count, seed length and shift count as `smash` lengths from the polynomial time bound), decodes the triple with the payload scanners, and takes the disjunction over shift blocks of the majority vote over trial blocks; - `matrixFn_eq` proves that computation equals `matrixVerdict`, bridging the string view and the `Finset` counting view: `blockEventCount_seedOfList` matches the counts, `seedOfList_xorSuffix` and `seedOfList_padTo_block` match the exclusive-or with the shift action, and `pathAccepts_iff` matches a block's acceptance with membership in the single-trial event; - `matrixVerdict_mem_FP` concludes via `CobhamFP_subset_FP`. `Matrix` now decodes with `Cobham.fstBlock`/`sndBlock` rather than `unpair?`, so the matrix language and its verdict agree on every input, including malformed ones. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Collaborator
Author
|
Superseded: splitting the Sipser–Lautemann work onto its own branch; |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Proves the Sipser–Lautemann theorem,
BPP ⊆ Σ₂ᵖ ∩ Π₂ᵖ, unconditionally:with
BPP_subset_SigmaP_two,BPP_subset_PiP_two, andBPP_subset_PH.This branch also carries the polynomial-hierarchy definitions (
Complexitylib.Classes.PH:SigmaP,PiP,PH, quantifier duality, level inclusions) and the bitstring-encodingwork they depend on, which were previously on separate branches.
The development
SipserLautemann.CoveringSipserLautemann.TimeBoundSipserLautemann.Amplified∃∀characterization ofL, and its complementary form forLᶜSipserLautemann.Encode,.MatrixLandLᶜas polynomially bounded∃∀forms over the matrix languageSipserLautemann.VerdictFPThe polynomial-time obligation on the matrix is discharged with no machine construction:
CobhamFP_eq_FPturns it into a programming task in Cobham's algebra. Two supporting piecesmake that possible:
Models.TuringMachine.ChoiceTape—NTM.choiceTMfeeds an NTM's choice bit from a work tape,one per step, so running one nondeterministic path is a definition, not a simulation loop;
choiceTM_simulatesproves aT-step run istm.trace Talong the bits on the tape. This isalso the primitive
NP.WitnessNTMConstructionhas been waiting for.Classes.P.Cobham.Internal.ChoiceSim/.BlockLoop— that run, and the amplified verdict,inside the algebra; plus
.PolyLen/.StringOpsfor polynomial lengths, length tests, andexclusive-or.
Classes.P.DecisionFn—mem_P_of_decisionFn_boolturns a verdict function inFPintomembership in
P.Side effect: PH's own
pairFst ∈ FPseam is closed —Cobham.fstBlock_mem_FPwas alreadyproved — so
P_subset_polyExistsClass_P,P_subset_polyForallClass_P,SigmaP_subset_SigmaP_succandPiP_subset_PiP_succare now unconditional.Test plan
All CI gates pass locally:
lake build --wfail(3933 jobs) and all five validation targetspython3 scripts/lint_style.pylake exe runLinteron the public root and all five validation import graphslake env lean scripts/AxiomGuard.lean— 43463 declarations, 0 axioms;sipserLautemanndepends only on
propext,Classical.choice,Quot.sound🤖 Generated with Claude Code