OAI/Computability/UniqueGames/PCP/SourceLoopInitLemmas.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.HeaderTape line 12
2. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList line 16
3. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList_getElem?_ctorIdx_eq line 18
4. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.HeaderTape.enumList_nodup line 22
5. instance OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.(instance at line 24) line 24
6. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.Tape line 28
7. inductive OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.Label line 30
8. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.variableHeader line 38
9. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.clauseHeader line 39
10. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.headerDestination line 40
11. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.readStart line 41
12. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.readLoop line 42
13. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.labelAt line 43
14. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.program line 45
15. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.atReadStart line 64
16. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.atReadLoop line 69
17. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.atReadDone line 74
18. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.copiedInput line 80
19. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.readOutput line 83
20. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.headerOutput line 87
21. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.clear_readOutput line 92
22. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.readOutput_work line 102
23. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.headerOutput_frame line 107
24. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.headerInTime line 111
25. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.digitOutput line 147
26. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.digitOutput_frame line 150
27. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.digitInTime line 154
28. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.stageTapes line 197
29. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.stageTapes_frame line 202
30. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.stageTapes_current line 213
31. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.stageTapes_remaining line 233
32. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.prefixInTime line 254
33. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.digitsInTime line 282
34. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.outputTapes line 301
35. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.initializeInTime line 304
36. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.output_current line 336
37. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.output_remaining line 340
38. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.output_frame line 344
39. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.output_work line 350
40. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.output_variableHeader line 355
41. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.output_clauseHeader line 360
42. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.output_headers line 365
43. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.output_formula line 371
44. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.timePolynomial line 376
45. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.timePolynomial_eval line 379
46. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceLoopInit.machine line 383
47. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.Label line 402
48. abbrev OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.Tapes line 403
49. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.entry line 405
50. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.statement line 410

    Source documentation

    All instructions act on physical stacks. The final load only resets the finite internal register; no input-dependent integer is stored in it.

    def statement (clearKeys : List K) (accumulator output : K) (canonical : σ)
        (labels : Label clearKeys → Λ) (exit : Option Λ) :
        Label clearKeys → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool)
      | .inl label => MachineDrainMany.instruction clearKeys (fun l => labels (.inl l))
          (some (labels (.inr false))) label
      | .inr false => Reduction.MachineTransfer.loopAt accumulator output id false
          (labels (.inr false)) (some (labels (.inr true)))
      | .inr true => .load (fun _ => (canonical, none)) (Reduction.MachineTransfer.exitAt output exit)

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.Label, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.loopAt, OAI.UniqueGamesTheorem.Reduction.MachineTransfer.exitAt

51. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.canonicalTapes line 419
52. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.finishCost line 422
53. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.cleared_frame line 425
54. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.reversed_tapes line 429
55. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.finishInTime line 448

    Source documentation

    Exact execution, including the real drain loops, reversal, and reset. The only program hypotheses identify the caller's actual placed statements.

    def finishInTime (clearKeys : List K) (accumulator output : K)
        (distinct : accumulator ≠ output)
        (keepAccumulator : accumulator ∉ clearKeys) (keepOutput : output ∉ clearKeys)
        (covers : ∀ k, k ≠ accumulator → k ≠ output → k ∈ clearKeys)
        (canonical : σ) (labels : Label clearKeys → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (σ × Option Bool))
        (atLabels : ∀ label,
          program (labels label) = statement clearKeys accumulator output canonical labels exit label)
        (base : Tapes K) (outputEmpty : base output = []) (ambient : σ) (register : Option Bool) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨entry clearKeys labels, (ambient, register), base⟩
          (some ⟨exit, (canonical, none), canonicalTapes output (base accumulator).reverse⟩)
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.Label, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.statement, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.Tapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.entry, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.canonicalTapes

56. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.finishCost_le_list line 508
57. def OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.totalLength line 518
58. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.totalLength_erase line 520
59. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.drain_conservation line 536

    Source documentation

    Each physical pop removes one stored symbol; repeated clear keys add only the extra empty-tape loop test after their first occurrence.

    theorem drain_conservation (clearKeys : List K) (base : Tapes K) :
        MachineDrainMany.steps clearKeys base +
          totalLength (MachineDrainMany.finalTapes clearKeys base) =
            totalLength base + clearKeys.length := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.Tapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.totalLength

60. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.cleared_totalLength line 548
61. theorem OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.finishCost_eq_totalLength line 567

    Source documentation

    Exact finalization cost from the complete initial stack contents.

    theorem finishCost_eq_totalLength (clearKeys : List K) (accumulator output : K)
        (keepAccumulator : accumulator ∉ clearKeys) (keepOutput : output ∉ clearKeys)
        (covers : ∀ k, k ≠ accumulator → k ≠ output → k ∈ clearKeys)
        (base : Tapes K) (outputEmpty : base output = []) :
        finishCost clearKeys accumulator base = totalLength base + clearKeys.length + 2 := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.Tapes, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.finishCost, OAI.UniqueGamesTheorem.Foundations.Hastad.SourceRuntimeFinish.totalLength