feat: PCP theorem, interactive proof classes, and complexity class containments - #31
Merged
SamuelSchlesinger merged 34 commits intoAug 30, 2026
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>
A verifier is a language in `P` — a polynomial-time predicate — applied to the encoded tuple it sees, with private coins measured by `eventProb`, so the definitions stay machine-free and auditable. - `MA` — Merlin's proof cannot depend on the coins, so the existential sits outside the probability; - `AM` — Arthur's public coins come first, so the existential over Merlin's reply sits inside it; - `IP` — `Protocol` bundles a round count, a private-coin count, a message-length bound, the verifier's next message as a function in `FP`, and its verdict as a language in `P`; `Protocol.transcript` runs the interaction against a `ProverStrategy`, which sees the transcript but never the coins. Completeness asks for one length-respecting strategy; soundness quantifies over all of them. `P_subset_MA` and `P_subset_AM` pin the definitions down: the verifier ignores the proof and the coins and decodes the input with `Cobham.fstBlock`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
BoltonBailey
marked this pull request as draft
August 30, 2026 14:51
SamuelSchlesinger
pushed a commit
that referenced
this pull request
Aug 30, 2026
Adds `PCP_theorem`: `NP` equals the union of `PCP r q` over constructible `r =O log` and constant `q`, proved via Dinur's gap amplification (the `NP ⊆ PCP` direction) and a guess-and-verify simulation (`PCP ⊆ NP`). This is the transitive import closure of the theorem's proof, extracted from the larger #31 branch: the `Classes/PCP` tree (Defs, surface, and 115 internal modules), plus the `FP` toolkit lemmas under `Classes/Containments/Internal` and `Classes/P` that the PCP algorithms reuse (pair-decoder bridge, binary arithmetic, bounded search, witness enumeration), and the `Interactive`/`PH` class definitions those depend on. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
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
2 participants
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.
This is a really big PR that comes from several overnight runs, lots of it is currently unreviewed, but I'll put it up in case its useful.
🤖 Generated with Claude Code