OAI/Computability/UniqueGames/Machines/MachineProductFieldLemmas.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductField.Layout line 32

   Source documentation

   Gather's table/query/scan/scratch and coordinate tapes; then radix, two Horner accumulators, counter, scratch, isolated field output, global output.

   abbrev Layout (width : Nat) := MachineProductGather.Tape width ⊕ Fin 7

   Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductGather.Tape

2. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.gatherSlots line 34
3. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.hornerRole line 37
4. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.hornerRole_injective line 46
5. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.hornerSlots line 58
6. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.clearTapes line 61
7. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductField.Label line 65
8. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.entry line 69
9. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.instruction line 72
10. structure OAI.UniqueGamesTheorem.Explicit.MachineProductField.Ready line 87

    Source documentation

    Conditions on real input/work stacks; arbitrary output suffixes remain permitted. The two query/scan tapes are empty at a row boundary.

    structure Ready (slots : Layout width ↪ K) (base : K → List Bool) : Prop where
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductField.Layout

11. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.gathered line 98
12. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.evaluated line 103
13. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.emitted line 108
14. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.finalTapes line 114
15. def OAI.UniqueGamesTheorem.Explicit.MachineProductField.steps line 119
16. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.gathered_extra line 128
17. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.fieldTrace line 140

    Source documentation

    Actual execution of the complete gather/Horner/emit/cleanup phase. The field equality connects only mathematical tape contents; all transition work is proved from the concrete instructions.

    theorem fieldTrace (slots : Layout width ↪ K) (values : List Nat) (coefficient : Nat)
        (indices offsets fields : Fin width → Nat)
        (selected : ∀ i, values[coefficient * indices i + offsets i]? = some (fields i))
        (labels : Label slots → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ l, program (labels l) = instruction slots coefficient offsets labels exit l)
        (base : K → List Bool) (suffixes : Fin width → List Bool) (ready : Ready slots base)
        (tableWord : base (slots (.inl (.inl 0))) = encodeWords values)
        (sourceWords : ∀ i, base (slots (.inl (.inr (.inl i)))) =
          encodeWord (indices i) ++ suffixes i)
        (radix : Nat) (digits : Nat → Nat)
        (radixWord : base (slots (.inr 0)) = encodeWord radix)
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductField.Layout, OAI.UniqueGamesTheorem.Explicit.MachineProductField.Label, OAI.UniqueGamesTheorem.Explicit.MachineProductField.instruction, OAI.UniqueGamesTheorem.Explicit.MachineProductField.Ready

18. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.mem_clearTapes line 236
19. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.extra_not_mem_clearTapes line 242
20. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.Ready.empty_clearTapes line 251
21. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.gathered_frame line 258
22. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.finalTapes_eq line 269

    Source documentation

    The complete row-field phase changes just the output accumulator.

    theorem finalTapes_eq (slots : Layout width ↪ K) (values : List Nat) (coefficient : Nat)
        (indices offsets fields : Fin width → Nat) (base : K → List Bool)
        (ready : Ready slots base) (value : Nat) :
        finalTapes slots values coefficient indices offsets fields base value =
          Function.update base (slots (.inr 6))
            ((encodeWord value).reverse ++ base (slots (.inr 6))) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductField.Layout, OAI.UniqueGamesTheorem.Explicit.MachineProductField.Ready, OAI.UniqueGamesTheorem.Explicit.MachineProductField.finalTapes

23. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.Ready.output_update line 296

    Source documentation

    The output update preserves all work-tape entry conditions.

    theorem Ready.output_update (slots : Layout width ↪ K) (base : K → List Bool)
        (ready : Ready slots base) (word : List Bool) :
        Ready slots (Function.update base (slots (.inr 6)) word) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductField.Layout, OAI.UniqueGamesTheorem.Explicit.MachineProductField.Ready

24. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.final_ready line 313
25. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.emitted_clear_length line 321

    Source documentation

    Cleanup only touches gather work; it never scans the global accumulator.

    theorem emitted_clear_length (slots : Layout width ↪ K) (values : List Nat) (coefficient : Nat)
        (indices offsets fields : Fin width → Nat)
        (selected : ∀ i, values[coefficient * indices i + offsets i]? = some (fields i))
        (base : K → List Bool) (ready : Ready slots base) (value : Nat)
        (k : K) (member : k ∈ clearTapes slots) :
        (emitted slots values coefficient indices offsets fields base value k).length ≤
          width * ((encodeWords values).length + 1) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductField.Layout, OAI.UniqueGamesTheorem.Explicit.MachineProductField.Ready, OAI.UniqueGamesTheorem.Explicit.MachineProductField.clearTapes, OAI.UniqueGamesTheorem.Explicit.MachineProductField.emitted

26. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.clearTapes_length line 339
27. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductField.cleanup_steps_le line 342
28. def OAI.UniqueGamesTheorem.Explicit.MachineProductPower.digits line 379
29. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductPower.value_eq line 381
30. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductPower.Label line 388
31. def OAI.UniqueGamesTheorem.Explicit.MachineProductPower.instruction line 390
32. def OAI.UniqueGamesTheorem.Explicit.MachineProductPower.steps line 397
33. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductPower.powerTrace line 402

    Source documentation

    Header powers are computed from a unary input radix, not stored in an unbounded register. Only the output accumulator changes at the boundary.

    theorem powerTrace (slots : MachineHorner.Layout (exponent + 1) ↪ K) (output : K)
        (outside : ∀ i, output ≠ slots i) (labels : Label exponent → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ l, program (labels l) = instruction slots output labels exit l)
        (base : K → List Bool) (radix : Nat)
        (radixWord : base (slots (.inl 0)) = encodeWord radix)
        (digitWords : ∀ i : Fin (exponent + 1), base (slots (.inr i)) = encodeWord (digits i.val))
        (clean : MachineHorner.Clean slots base) (fieldEmpty : base (slots (.inl 3)) = [])
        (ambient : σ) (register : Option Bool) :
        (advance (TM2.step program))^[steps radix exponent]
          (some ⟨some (labels (.inl .start)), ((ambient, ()), register), base⟩) =
          some ⟨exit, ((ambient, ()), none),
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductPower.Label, OAI.UniqueGamesTheorem.Explicit.MachineProductPower.instruction, OAI.UniqueGamesTheorem.Explicit.MachineProductPower.digits, OAI.UniqueGamesTheorem.Explicit.MachineProductPower.steps

34. def OAI.UniqueGamesTheorem.Explicit.MachineProductPower.timePolynomial line 444
35. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductPower.steps_le line 448
36. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Layout line 475
37. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Command line 476
38. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.fieldRole line 479

    Source documentation

    Only the radix tape is switched between endpoint and alphabet fields.

    def fieldRole (useAlphabet : Bool) : MachineProductField.Layout width → Layout width
      | .inr 0 => if useAlphabet then .inr () else .inl (.inr 0)
      | tape => .inl tape

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductField.Layout, OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Layout

39. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductRow.fieldRole_injective line 483
40. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.fieldSlots line 496
41. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductRow.LocalLabel line 500
42. abbrev OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Label line 503
43. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.localMain line 506
44. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.localInstruction line 509
45. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.entry line 514
46. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.instruction line 518
47. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.outputTape line 524
48. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.appendField line 526
49. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.rowBits line 530

    Source documentation

    Exact literal output of the command list in field order.

    def rowBits (values : Command width → Nat) (commands : List (Command width)) : List Bool :=
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Command

50. def OAI.UniqueGamesTheorem.Explicit.MachineProductRow.result line 533
51. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductRow.resultOf_eq line 537
52. structure OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Ready line 550

    Source documentation

    The input-dependent data needed for one whole row, held invariant by all physical field executions.

    structure Ready (slots : Layout width ↪ K) (table : List Nat) (indices : Fin width → Nat)
        (radices : Bool → Nat) (base : K → List Bool) : Prop where
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Layout

53. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Ready.appendField line 557
54. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductRow.rowTrace line 580

    Source documentation

    Complete row trace from the concrete field implementation. The only premises concerning values are literal indexed-table identities and the Horner interpretation of those values.

    theorem rowTrace (slots : Layout width ↪ K) (table : List Nat) (coefficient : Nat)
        (indices : Fin width → Nat) (radices : Bool → Nat) (commands : List (Command width))
        (fields : Command width → Fin width → Nat) (digits : Command width → Nat → Nat)
        (selected : ∀ command ∈ commands, ∀ i,
          table[coefficient * indices i + command.2 i]? = some (fields command i))
        (reversed : ∀ command ∈ commands, ∀ i : Fin width,
          digits command i.val = fields command i.rev)
        (labels : Label slots commands → Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (MachineHorner.State σ))
        (atLabels : ∀ l, program (labels l) = instruction slots coefficient commands labels exit l)
        (base : K → List Bool) (ready : Ready slots table indices radices base) (ambient : σ) :
        let values := fun c : Command width => MachineHorner.value (radices c.1) (digits c) width
    …

    Mentions: OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Layout, OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Command, OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Label, OAI.UniqueGamesTheorem.Explicit.MachineProductRow.instruction, OAI.UniqueGamesTheorem.Explicit.MachineProductRow.Ready

55. def OAI.UniqueGamesTheorem.Explicit.MachineProductBounds.fieldPolynomial line 633
56. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductBounds.fieldPolynomial_eval line 638
57. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductBounds.field_steps_le line 644
58. def OAI.UniqueGamesTheorem.Explicit.MachineProductBounds.rowCost line 667
59. theorem OAI.UniqueGamesTheorem.Explicit.MachineProductBounds.row_steps_le line 675
60. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial line 712
61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval line 716
62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial_eval_reverse line 722
63. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.coefficients line 729

    Source documentation

    An actual finite coefficient list for every fixed natural polynomial. No evaluation of an input is included in this static representation choice.

    noncomputable def coefficients (p : Polynomial Nat) :
        {cs : List Nat // coefficientPolynomial cs = p} := by
    …

    Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.coefficientPolynomial

64. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients line 749
65. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.width line 752
66. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.digit line 754
67. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.digitBound line 757
68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.le_sum_of_mem line 759
69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.digit_le_bound line 769
70. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.highCoefficients_foldl line 775
71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.range_map_digit line 782
72. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.prependFields line 796
73. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes line 802
74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_prependFields line 808
75. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.prependFieldsTapes_apply line 818
76. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.popN line 832
77. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_popN line 837
78. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields line 848
79. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes line 853
80. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.stepAux_clearFields line 858
81. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.clearFieldsTapes_apply line 868
82. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.Layout line 886
83. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.Label line 887
84. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.State line 888
85. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.fieldWord line 890
86. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices line 894
87. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.fieldIndices_nodup line 897
88. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.inl_not_mem_fields line 900
89. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.inr_mem_fields line 903
90. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.initialTapes line 906
91. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes line 909
92. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inl line 912
93. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_inr line 917
94. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.slots line 922
95. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.preparedTapes_clean line 924
96. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.innerLabels line 928
97. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.program line 931
98. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.machine line 941
99. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.afterHornerTapes line 952
100. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.afterInputTapes line 955
101. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.finalTapes line 958
102. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.clearFields_final line 961
103. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.initList_eq line 972
104. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.haltList_eq line 978
105. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.initializationTrace line 984
106. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.cleanupTrace line 994
107. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial line 1011
108. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial line 1015
109. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.prefixValuePolynomial_eval line 1021
110. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.prefixCostPolynomial_eval line 1027
111. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial line 1037
112. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial_eval line 1041
113. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.hornerValue_eq_eval line 1048
114. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.hornerStageTrace line 1054
115. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.outputsInTime line 1070

     Source documentation

     Exact execution includes literal initialization, the physical Horner subroutine, input consumption, and cleanup of every coefficient tape.

     def outputsInTime (p : Polynomial Nat) (n : Nat) :
         Turing.TM2OutputsInTime (machine p) (encodeWord n) (some (encodeWord (p.eval n)))
           ((timePolynomial p).eval n) where
     …

     Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.machine, OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord, OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.timePolynomial

116. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.PolynomialMachine.computableInPolyTime line 1091

     Source documentation

     A genuine finite Boolean-stack machine for evaluating any fixed natural polynomial on zero-delimited unary input, with a polynomial transition bound.

     def computableInPolyTime (p : Polynomial Nat) :
         Turing.TM2ComputableInPolyTime encodeWord encodeWord p.eval where
     …

     Mentions: OAI.UniqueGamesTheorem.Foundations.Complexity.encodeWord