RoundComputation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual sequential finite-machine composition for the concrete numbered round. The initial composition lemma isolates the preprocessing and powering execution certificates with their shared bit codecs. The final endpoint supplies the checked powering and alphabet machines, leaving only preprocessing explicit.

abbrev OAI.MaxCutGames.Foundations.PCP.RoundComputation.PreprocessingCertificate line 20
Source documentation
The exact pending preprocessing interface, including its output encoding.
```
abbrev PreprocessingCertificate (H : RoundTables.BaseTable) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.RoundTables.BaseTable
abbrev OAI.MaxCutGames.Foundations.PCP.RoundComputation.PoweringCertificate line 26
Source documentation
The exact powering interface at the fixed parameters of the round.
```
abbrev PoweringCertificate :=
…
```
theorem OAI.MaxCutGames.Foundations.PCP.RoundComputation.powered_eq_transform line 32
def OAI.MaxCutGames.Foundations.PCP.RoundComputation.poweredPolynomialTimeOfCertificates line 39
Source documentation
Both actual transfer loops between the machines are included by MachineSequential.composeBits; their work contributes to its polynomial.
```
noncomputable def poweredPolynomialTimeOfCertificates (H : RoundTables.BaseTable)
    (preprocessing : PreprocessingCertificate H) (powering : PoweringCertificate) :
    TM2ComputableInPolyTime GraphTables.tableBits
      (GenericGraphTables.tableBits (q := RoundTables.alphabet))
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.RoundTables.BaseTable, OAI.MaxCutGames.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.MaxCutGames.Foundations.PCP.RoundComputation.PoweringCertificate, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.GenericGraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.RoundTables.alphabet
def OAI.MaxCutGames.Foundations.PCP.RoundComputation.tablePolynomialTimeOfCertificates line 49
theorem OAI.MaxCutGames.Foundations.PCP.RoundComputation.powered_finiteAlphabet line 61
Source documentation
All intermediate work alphabets stay finite under the actual sequential composition, provided that they are finite in the two supplied machines.
```
theorem powered_finiteAlphabet (H : RoundTables.BaseTable)
    (preprocessing : PreprocessingCertificate H) (powering : PoweringCertificate)
    (hpreprocessing : MachineFiniteAlphabet.FiniteAlphabet preprocessing.tm)
    (hpowering : MachineFiniteAlphabet.FiniteAlphabet powering.tm) :
    MachineFiniteAlphabet.FiniteAlphabet
      (poweredPolynomialTimeOfCertificates H preprocessing powering).tm :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.RoundTables.BaseTable, OAI.MaxCutGames.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.MaxCutGames.Foundations.PCP.RoundComputation.PoweringCertificate, OAI.MaxCutGames.Foundations.PCP.RoundComputation.poweredPolynomialTimeOfCertificates
theorem OAI.MaxCutGames.Foundations.PCP.RoundComputation.finiteAlphabet line 71
Source documentation
This is a separate work-alphabet fact about the same runtime certificate; the final alphabet stage has homogeneous Bool tapes.
```
theorem finiteAlphabet (H : RoundTables.BaseTable)
    (preprocessing : PreprocessingCertificate H) (powering : PoweringCertificate)
    (hpreprocessing : MachineFiniteAlphabet.FiniteAlphabet preprocessing.tm)
    (hpowering : MachineFiniteAlphabet.FiniteAlphabet powering.tm) :
    MachineFiniteAlphabet.FiniteAlphabet
      (tablePolynomialTimeOfCertificates H preprocessing powering).tm :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.RoundTables.BaseTable, OAI.MaxCutGames.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.MaxCutGames.Foundations.PCP.RoundComputation.PoweringCertificate, OAI.MaxCutGames.Foundations.PCP.RoundComputation.tablePolynomialTimeOfCertificates
def OAI.MaxCutGames.Foundations.PCP.RoundComputation.tablePolynomialTime line 85
Source documentation
Powering and alphabet reduction now use their constructed finite machines. The only remaining input is an execution certificate for preprocessing.
```
noncomputable def tablePolynomialTime (H : RoundTables.BaseTable)
    (preprocessing : PreprocessingCertificate H) :
    TM2ComputableInPolyTime GraphTables.tableBits GraphTables.tableBits
      (RoundTables.build H) :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.RoundTables.BaseTable, OAI.MaxCutGames.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.MaxCutGames.Foundations.PCP.GraphTables.tableBits, OAI.MaxCutGames.Foundations.PCP.RoundTables.build
theorem OAI.MaxCutGames.Foundations.PCP.RoundComputation.tablePolynomialTime_finite_alphabet line 95
Source documentation
The same certificate has finite work-tape alphabets whenever the supplied preprocessing machine does; both later stages supply their own proof.
```
theorem tablePolynomialTime_finite_alphabet (H : RoundTables.BaseTable)
    (preprocessing : PreprocessingCertificate H)
    (hpreprocessing : MachineFiniteAlphabet.FiniteAlphabet preprocessing.tm) :
    MachineFiniteAlphabet.FiniteAlphabet
      (tablePolynomialTime H preprocessing).tm :=
…
```
Mentions: OAI.MaxCutGames.Foundations.PCP.RoundTables.BaseTable, OAI.MaxCutGames.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.MaxCutGames.Foundations.PCP.RoundComputation.tablePolynomialTime