Machine2.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.Foundations.Complexity.naturalWordsEncoding line 8
def OAI.MaxCutGames.Foundations.Complexity.formulaEncoding line 13
def OAI.MaxCutGames.Foundations.Complexity.gameEncoding line 19
Source documentation
Concrete forward-table output syntax with a checked parser.
```
def gameEncoding (alphabet : Nat) : Computability.Encoding (Target.Instance alphabet) Bool where
…
```
Mentions: OAI.MaxCutGames.Foundations.Target.Instance
def OAI.MaxCutGames.Foundations.Complexity.prefixBitMachine line 26
Source documentation
A fixed-bit prefixer uses one finite stack, one label, and one internal state. The bit is fixed in the program; it is not a second, freely accessible input.
```
def prefixBitMachine (bit : Bool) : Turing.FinTM2 where
…
```
def OAI.MaxCutGames.Foundations.Complexity.prefixBitPolyTime line 40
Source documentation
A real machine certificate: one transition performs the push and halts. TM2 counts execution of one finite statement as one transition. Here that statement contains exactly one stack push.
```
noncomputable def prefixBitPolyTime (bit : Bool) :
    Turing.TM2ComputableInPolyTime (id : List Bool → List Bool) id (bit :: ·) where
…
```

def OAI.MaxCutGames.Foundations.Complexity.enlargePolynomialBound line 60

Source documentation

Increasing a polynomial bound preserves the actual execution witness.

def enlargePolynomialBound {α β αΓ βΓ : Type}
    {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
    (certificate : Turing.TM2ComputableInPolyTime ea eb f)
    (bound : Polynomial Nat)
    (larger : ∀ n, certificate.time.eval n ≤ bound.eval n) :
    Turing.TM2ComputableInPolyTime ea eb f where
…

def OAI.MaxCutGames.Foundations.Complexity.composeMachinePhases line 76

Source documentation

Two verified phases of one transition system compose with added polynomial budgets, both measured in the original input length. This theorem preserves the actual sequence of transition steps, not merely the sizes of configurations.

def composeMachinePhases {σ : Type} (step : σ → Option σ)
    (start intermediate : σ) (finish : Option σ)
    (p q : Polynomial Nat) (inputLength : Nat)
    (first : StateTransition.EvalsToInTime step start (some intermediate) (p.eval inputLength))
    (second : StateTransition.EvalsToInTime step intermediate finish (q.eval inputLength)) :
    StateTransition.EvalsToInTime step start finish ((p + q).eval inputLength) := by
…

structure OAI.MaxCutGames.Foundations.Complexity.PolynomialGapReduction line 88