OAI/Computability/UniqueGames/PCP/LoopInitializationLemmas.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

The concrete tapes produced by initialization satisfy the row-zero loop invariant. Execution of initialization is proved separately by Initialization.initializeInTime; this bridge identifies its resulting tapes.

  1. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopInitialization.initialization_ready line 30

    Source documentation

    The actual initial loop tapes contain the complete unread input rows and exactly the two output headers in reverse order on the accumulation tape.

    theorem initialization_ready {q : Nat} (input : GenericGraphTables.Table q) :
    Ready input 0 (Initialization.loopTapes input) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Initialization.loopTapes

  2. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.zeroGuardInTime line 69

    Source documentation

    The zero guard preserves all tapes, resets its temporary register, and enters the actual driver's output-reversal phase in one transition.

    def zeroGuardInTime (input : GenericGraphTables.Table q) (base : Tape → List Bool)
    (ready : LoopState.Ready input input.darts base)
    (relation : GenericGraphTables.RelationTable q) (flag : Bool) :
    StateTransition.EvalsToInTime (TM2.step (Driver.program q))
      ⟨some .guard, normal relation flag, base⟩
      (some ⟨some .reverseOutput, normal relation flag, base⟩) 1 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.LoopState.Ready, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.RelationTable, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.program

  3. structure OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.LoopResult line 84

    Source documentation

    Concrete final configuration and full remaining-loop execution.

    structure LoopResult (input : GenericGraphTables.Table q) (e remaining : Nat)
    (base : Tape → List Bool) (oldRelation : GenericGraphTables.RelationTable q)
    (oldFlag : Bool) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.RelationTable

  4. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.runRemaining line 96
  5. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.prefixTime line 130

    Source documentation

    A quadratic prefix allowance because the number of original rows is at most the length of their fully encoded input table.

    def prefixTime (q N : Nat) : Nat :=
…
  6. structure OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.PrefixResult line 148

    Source documentation

    Actual initialization followed by every row, ending just before reversal.

    structure PrefixResult (input : GenericGraphTables.Table q) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table

  7. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.runPrefix line 160

    Source documentation

    No initialization or row trace is assumed: both are instantiated at this actual finite driver and this input, then composed.

    def runPrefix (input : GenericGraphTables.Table q) : PrefixResult input := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.PrefixResult

  8. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.PrefixResult.reversed line 183
  9. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Loop.PrefixResult.output line 187
  10. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial line 201
  11. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Runtime.prefixPolynomial_eval line 207
  12. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Runtime.time line 214
  13. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Runtime.tableOutputsInTime line 218

    Source documentation

    The concrete driver outputs exactly the checked table encoding.

    noncomputable def tableOutputsInTime {q : Nat} (input : GenericGraphTables.Table q) :
    TM2OutputsInTime (Driver.machine q) (GenericGraphTables.tableBits input)
      (some (GraphTables.tableBits (Table.build input)))
      ((time q).eval (GenericGraphTables.tableBits input).length) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.Table, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.machine, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Table.build, OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Runtime.time

  14. def OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Runtime.tablePolynomialTime line 236

    Source documentation

    Fixed q determines one finite machine and one natural polynomial. The input and output alphabets use the exact shared Bool serialization interfaces.

    noncomputable def tablePolynomialTime (q : Nat) :
    TM2ComputableInPolyTime (GenericGraphTables.tableBits (q := q))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits

  15. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Driver.finiteAlphabet line 271
  16. theorem OAI.UniqueGamesTheorem.Foundations.PCP.AlphabetTable.Runtime.finiteAlphabet line 277
  17. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFinishRuntime.finish line 293
  18. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFinishRuntime.output_eq_finish line 298
  19. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFinishRuntime.finish_degree_positive line 302
  20. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFinishRuntime.computableInPolyTime line 307

    Source documentation

    Both stages supply complete executions, cleanup, and polynomial bounds; the sequential composition includes the physical interstage bit transfer.

    noncomputable def computableInPolyTime (H : PreprocessingTables.BaseTable)
    (d : Nat) (hd : 0 < d) :
    TM2ComputableInPolyTime (PortTables.inputBits (ports := d))
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingTables.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.PortTables.inputBits

  21. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingFinishRuntime.finite_alphabet line 318
  22. def OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRuntime.tablePolynomialTime line 338
  23. theorem OAI.UniqueGamesTheorem.Foundations.PCP.PreprocessingRuntime.finiteAlphabet line 351
  24. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PreprocessingCertificate line 379

    Source documentation

    The exact pending preprocessing interface, including its output encoding.

    abbrev PreprocessingCertificate (H : RoundTables.BaseTable) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.BaseTable

  25. abbrev OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PoweringCertificate line 385

    Source documentation

    The exact powering interface at the fixed parameters of the round.

    abbrev PoweringCertificate :=
…
  26. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.powered_eq_transform line 391
  27. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.poweredPolynomialTimeOfCertificates line 398

    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.UniqueGamesTheorem.Foundations.PCP.RoundTables.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PoweringCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.GenericGraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.alphabet

  28. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.tablePolynomialTimeOfCertificates line 408
  29. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.powered_finiteAlphabet line 420

    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.UniqueGamesTheorem.Foundations.PCP.RoundTables.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PoweringCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.poweredPolynomialTimeOfCertificates

  30. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.finiteAlphabet line 430

    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.UniqueGamesTheorem.Foundations.PCP.RoundTables.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PoweringCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.tablePolynomialTimeOfCertificates

  31. def OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.tablePolynomialTime line 444

    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.UniqueGamesTheorem.Foundations.PCP.RoundTables.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.GraphTables.tableBits, OAI.UniqueGamesTheorem.Foundations.PCP.RoundTables.build

  32. theorem OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.tablePolynomialTime_finite_alphabet line 454

    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.UniqueGamesTheorem.Foundations.PCP.RoundTables.BaseTable, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.PreprocessingCertificate, OAI.UniqueGamesTheorem.Foundations.PCP.RoundComputation.tablePolynomialTime