NP.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Verifier-defined NP over finite bitstring machines. This definition does not mention SAT. Inputs and witnesses use a fixed explicit framing, verifiers return one Boolean symbol, and all stacks have finite alphabets. The Cook–Levin target separately requires an actual polynomial-time machine producing the established formulaBits serialization, in addition to satisfiability equivalence.

def OAI.MaxCutGames.Foundations.Complexity.CookLevin.pairBits line 17
Source documentation
A unary length frame followed by input bits and witness bits.
```
def pairBits (input : List Bool × List Bool) : List Bool :=
…
```
def OAI.MaxCutGames.Foundations.Complexity.CookLevin.decodePairAux line 20
def OAI.MaxCutGames.Foundations.Complexity.CookLevin.decodePair line 26
theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.decodePairAux_frame line 29
theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.decodePair_pairBits line 39
theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.pairBits_injective line 45
theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.pairBits_length line 50
def OAI.MaxCutGames.Foundations.Complexity.CookLevin.pairEncoding line 55
structure OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier line 64
Source documentation
A standard polynomial-time Boolean verifier. FinTM2 already requires finitely many stacks, control labels, and internal states; this field also requires every stack alphabet to be finite. The actual machine runs on the explicit paired input and halts with exactly one Boolean output symbol.
```
structure NPVerifier where
…
```
def OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier.Accepts line 70
def OAI.MaxCutGames.Foundations.Complexity.CookLevin.InNP line 77
Source documentation
NP is specified by polynomial witnesses and genuine finite-machine verification, independently of any reduction or satisfiability problem.
```
def InNP (language : List Bool → Prop) : Prop :=
…
```
theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier.acceptedLanguage_inNP line 80
structure OAI.MaxCutGames.Foundations.Complexity.CookLevin.PolynomialThreeSATReduction line 86
Source documentation
The demanded Cook–Levin endpoint: both the SAT equivalence and an actual machine producing the fixed existing unary-token 3CNF encoding. This structure contains obligations; its inhabitance is not assumed or asserted here.
```
structure PolynomialThreeSATReduction (language : List Bool → Prop) where
…
```
def OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier.horizon line 92
Source documentation
A common clock for all witnesses of permitted length for one input.
```
noncomputable def NPVerifier.horizon (verifier : NPVerifier) (inputLength : Nat) : Nat :=
…
```
Mentions: OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier
theorem OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier.input_time_le_horizon line 96

def OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier.runWithinHorizon line 107

Source documentation

A real verifier execution, enlarged to the single input-dependent clock. The machine and its output are the ones supplied in the verifier definition.

def NPVerifier.runWithinHorizon (verifier : NPVerifier)
    (input witness : List Bool)
    (bounded : witness.length ≤ verifier.witnessBound.eval input.length) :
    Turing.TM2OutputsInTime verifier.computation.tm
      ((pairBits (input, witness)).map verifier.computation.inputAlphabet.invFun)
      (some ([verifier.verify (input, witness)].map verifier.computation.outputAlphabet.invFun))
      (verifier.horizon input.length) where
…

Mentions: OAI.MaxCutGames.Foundations.Complexity.CookLevin.NPVerifier, OAI.MaxCutGames.Foundations.Complexity.CookLevin.pairBits