MachineFiniteAlphabet.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finiteness of every alphabet of the actual machines used by the reduction. FinTM2 already bundles finitely many tapes, control labels and register states, but its alphabet field only requires the input tape alphabet to be finite. This additional property is preserved by the actual sequential and repetition constructors; it does not replace or alter their execution certificates.

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.input_finite line 26
Source documentation
This one alphabet is already finite in the underlying machine record.
```
theorem input_finite (M : FinTM2) : Finite (M.Γ M.k₀) := by
…
```
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.of_homogeneous line 30
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.of_bool line 37
Source documentation
All concrete Boolean-stack machines satisfy the stronger alphabet condition.
```
theorem of_bool (M : FinTM2) (alphabet : ∀ k, M.Γ k = Bool) : FiniteAlphabet M :=
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.of_equiv line 40
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.symbols_finite line 45
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.sequential_machine line 53
Source documentation
The first two tape groups retain their original alphabets. The sole new bridge tape uses the second machine's already finite input alphabet.
```
theorem sequential_machine (first second : FinTM2)
    (relabel : first.Γ first.k₁ → second.Γ second.k₀)
    (fallback : second.Γ second.k₀)
    (hfirst : FiniteAlphabet first) (hsecond : FiniteAlphabet second) :
    FiniteAlphabet (MachineSequential.machine first second relabel fallback) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.machine

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.compose line 66

Source documentation

Preservation for the machine actually stored in the polynomial-time composition certificate, with its actual relabeling bridge.

theorem compose {α β γ αΓ βΓ γΓ : Type}
    {ea : α → List αΓ} {eb : β → List βΓ} {ec : γ → List γΓ}
    {f : α → β} {g : β → γ}
    (first : TM2ComputableInPolyTime ea eb f)
    (second : TM2ComputableInPolyTime eb ec g) (fallback : βΓ)
    (hfirst : FiniteAlphabet first.tm) (hsecond : FiniteAlphabet second.tm) :
    FiniteAlphabet (MachineSequential.compose first second fallback).tm := by
…

Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineSequential.compose

theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.composeBits line 77
theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.repeat_machine line 88
Source documentation
Counter, temporary, and output tapes of the actual repeat machine all use the body's finite input alphabet; body tapes retain their original alphabets.
```
theorem repeat_machine (body : FinTM2)
    (input : body.Γ body.k₀ ≃ Bool) (output : body.Γ body.k₁ ≃ Bool)
    (hbody : FiniteAlphabet body) :
    FiniteAlphabet (MachineRepeat.machine body input output) := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet, OAI.UniqueGamesTheorem.Foundations.Complexity.MachineRepeat.machine