OAI/Computability/UniqueGames/Reduction/MachineAddressEdgeLemmas.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Actual edge emission from two fixed address templates. Capacity is copied before unary addition, so the original capacity tape is preserved. All local labels and literal instructions depend only on fixed templates and layout.

  1. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Tape line 20
  2. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.State line 21
  3. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Alphabet line 22
  4. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.addressSlots line 26
  5. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.capacityTape line 30
  6. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.outputTape line 31
  7. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.workTape line 32
  8. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.tempTape line 33
  9. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.scratchTape line 34
  10. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.address_ne_output line 37
  11. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.capacity_ne_output line 41
  12. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.work_ne_output line 45
  13. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.temp_ne_work line 49
  14. abbrev OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Label line 52
  15. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.leftLabel line 55
  16. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.rightLabel line 57
  17. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.plumbing line 59
  18. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.instruction line 62
  19. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.program line 88
  20. structure OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Clean line 93
  21. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.appended line 97
  22. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.appended_address line 100
  23. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.appended_capacity line 106
  24. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.appended_output line 110
  25. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.appended_other line 115
  26. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.appended_append line 120
  27. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Clean.appended line 125
  28. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.edgeBits line 139
  29. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.phaseSteps line 144
  30. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.addressResult_eq line 152
  31. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.transfer_result line 156
  32. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.literalStep line 187
  33. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.phaseTrace line 198

    Source documentation

    Both actual address computations, a preserved-capacity copy, unary addition, cleanup, two reverse transfers, and the fixed permutation instruction.

    theorem phaseTrace (base : K → List Bool) (B C : Nat)
    (leftValues rightValues : List Nat)
    (leftLength : leftValues.length = width) (rightLength : rightValues.length = width)
    (clean : Clean slots base)
    (baseField : base (addressSlots slots .radix) = encodeWord B)
    (capacityField : base (capacityTape slots) = encodeWord C)
    (leftCorrect : MachineFieldTemplate.templateOutput left
      (fun j => base (addressSlots slots (.field j))) = encodeWords leftValues)
    (rightCorrect : MachineFieldTemplate.templateOutput right
      (fun j => base (addressSlots slots (.field j))) = encodeWords rightValues)
    (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step P))^[phaseSteps left right slots base B C leftValues rightValues]
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Clean, OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.addressSlots, OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.capacityTape, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateOutput, OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.phaseSteps

  34. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.programTrace line 331
  35. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.phaseInTime line 354
  36. def OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.timePolynomial line 385

    Source documentation

    A fixed polynomial in a common magnitude bound for the input fields, serialized words, radix, capacity, and digits.

    noncomputable def timePolynomial (leftCount rightCount width : Nat) : Polynomial Nat :=
…
  37. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.timePolynomial_eval line 391
  38. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.radix_le_magnitude line 399
  39. theorem OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.phaseSteps_le_timePolynomial line 408
  40. structure OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Spec line 447
  41. structure OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Values line 453

    Source documentation

    Numeric interpretations are proof-side data, separate from the program.

    structure Values (width : Nat) where
…
  42. abbrev OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Rhs line 459
  43. abbrev OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Row line 460
  44. abbrev OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.State line 461
  45. abbrev OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Alphabet line 462
  46. abbrev OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.LocalLabel line 466
  47. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.localMain line 470
  48. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.localInstruction line 475
  49. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.payload line 480
  50. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.rowResult line 484
  51. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.rowCost line 489
  52. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.rowCosts line 496

    Source documentation

    Exact per-row costs at their actual accumulated output frames.

    def rowCosts (slots : MachineAddressEdge.Tape q width ↪ K)
    (B C : Nat) (values : Spec q width → Values width) :
    List (Spec q width) → (K → List Bool) → List Nat
  | [], _ => []
  | row :: rows, base => rowCost slots B C values row base ::
      rowCosts slots B C values rows (rowResult slots B C values row base)

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Tape, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Spec, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Values, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.rowCost, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.rowResult

  53. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.rowCosts_length line 503
  54. structure OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Invariant line 511
  55. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Invariant.appended line 525
  56. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.appended_nil line 536
  57. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.sequence_result line 540
  58. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.sequence_steps line 552
  59. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.sequenceInstruction line 561
  60. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.sequenceTrace line 569

    Source documentation

    The generic finite-sequence local obligation is discharged by the concrete edge program, including its address arithmetic and capacity restoration.

    theorem sequenceTrace (slots : MachineAddressEdge.Tape q width ↪ K)
    (rows : List (Spec q width))
    (place : MachineFiniteSequence.Label (LocalLabel slots) rows → Λ) (exit : Option Λ)
    (P : Λ → TM2.Stmt (Alphabet (K := K)) Λ (MachineAddressEdge.State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Tape, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Spec, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.LocalLabel, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Alphabet, OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.State

  61. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.selected line 596
  62. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.selected_length line 599
  63. abbrev OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Label line 602
  64. instance OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.localLabelFintype line 605
  65. instance OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.localLabelDecidableEq line 608
  66. instance OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.labelFintype line 619
  67. instance OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.labelDecidableEq line 622
  68. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.sequenceEntry line 625
  69. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.dispatcher line 633

    Source documentation

    Reuse the RHS vector already loaded by MachineRhsLoad; dispatch takes one real transition, and resets only the optional temporary bit.

    def dispatcher (slots : MachineAddressEdge.Tape q width ↪ K) :
    (rows : List (Row k q width)) → (Label slots rows → Λ) → Option Λ →
      TM2.Stmt (Alphabet (K := K)) Λ (State k σ)
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Tape, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Row, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Label, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Alphabet, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.State

  70. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.instruction line 641
  71. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.program line 648
  72. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.dispatcherStep line 652
  73. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.phaseTrace line 665
  74. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.phaseInTime line 687
  75. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.emitted_output line 704
  76. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.exact_row_count line 713
  77. def OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.timePolynomial line 721

    Source documentation

    Sum of fixed row polynomials; the additional constant is the dispatcher. This proof-side polynomial contains no runtime input field values.

    noncomputable def timePolynomial (rows : List (Spec q width)) : Polynomial Nat :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Spec

  78. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.rowCosts_sum_le line 725
  79. theorem OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.phaseCost_le_timePolynomial line 756

    Source documentation

    The actual dispatcher-and-rows count is bounded by a fixed polynomial in explicit tape and digit magnitudes, using the checked edge arithmetic bound.

    theorem phaseCost_le_timePolynomial (slots : MachineAddressEdge.Tape q width ↪ K)
    (rows : List (Spec q width)) (base : K → List Bool)
    (B C : Nat) (values : Spec q width → Values width) (M : Nat)
    (clean : MachineAddressEdge.Clean slots base)
    (fieldsBound : ∀ j, (base (MachineAddressEdge.addressSlots slots (.field j))).length ≤ M)
    (radixBound : B ≤ M) (capacityBound : C ≤ M)
    (valuesBound : ∀ row ∈ rows,
      (encodeWords (values row).left).length ≤ M ∧
      (encodeWords (values row).right).length ≤ M ∧
      (∀ i, i < width → MachineTemplateAddress.digits (values row).left i ≤ M) ∧
      (∀ i, i < width → MachineTemplateAddress.digits (values row).right i ≤ M)) :
    (rowCosts slots B C values rows base).sum + 1 ≤ (timePolynomial rows).eval M := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Tape, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Spec, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.Values, OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.Clean, OAI.UniqueGamesTheorem.Reduction.MachineAddressEdge.addressSlots, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.digits, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.rowCosts, OAI.UniqueGamesTheorem.Reduction.MachineOutcomeRows.timePolynomial