OAI/Computability/UniqueGames/Reduction/MachineTemplateAddress.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

A fixed canonical-word template followed by actual radix-address execution. The program is determined by the fixed tokens and tape layout. Numeric field values enter only the tape invariants and execution theorem, never the labels.

  1. inductive OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Tape line 21
  2. abbrev OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.State line 28
  3. abbrev OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Alphabet line 29
  4. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.hornerLayout line 33
  5. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.hornerSlots line 49
  6. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.chosen line 52
  7. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.mem_chosen line 55
  8. abbrev OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Label line 59
  9. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.emitLabel line 63
  10. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.reverseLabel line 65
  11. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parseLabel line 66
  12. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.hornerLabel line 68
  13. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.cleanupLabel line 70
  14. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parseDestination line 73
  15. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parseDestination_below line 77
  16. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.instruction line 81

    Source documentation

    Fixed finite instruction assembly, with arbitrary placement and continuation.

    def instruction (tokens : List (MachineFieldTemplate.Token q)) (slots : Tape q width ↪ K)
    (place : Label tokens.length width (chosen slots) → Λ) (exit : Option Λ) :
    Label tokens.length width (chosen slots) → TM2.Stmt (Alphabet (K := K)) Λ (State σ)
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Token, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Tape, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Label, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.chosen, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Alphabet, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.State

  17. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.program line 104
  18. structure OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Clean line 110
  19. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.digits line 120
  20. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.forwardTapes line 122
  21. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parsedTapes line 125
  22. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.resultTapes line 130
  23. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.afterHorner line 133
  24. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.phaseSteps line 138
  25. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.resultTapes_output line 145
  26. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.resultTapes_other line 149
  27. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.hornerValue_eq_radix line 155

    Source documentation

    The numeric recurrence used by the checked Horner machine is the direct canonical-address radix, in the original template-word order.

    theorem hornerValue_eq_radix (B : Nat) (values : List Nat) :
    MachineHorner.value B (digits values) values.length = CanonicalAddress.radix B values := by
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.digits, OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix

  28. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parsedTapes_other line 165
  29. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parsedTapes_source line 176
  30. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parsedTapes_digit line 185
  31. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parsedTapes_clean line 204
  32. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.cleanup_result line 225
  33. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parse_atStart line 265
  34. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parse_atLoop line 274
  35. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.parse_atDone line 284
  36. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.phaseTrace line 290
  37. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.programTrace line 384

    Source documentation

    The emitted finite program discharges every instruction-placement premise.

    theorem programTrace (tokens : List (MachineFieldTemplate.Token q)) (slots : Tape q width ↪ K)
    (exit : Option (Label tokens.length width (chosen slots)))
    (base : K → List Bool) (B : Nat) (values : List Nat) (hlen : values.length = width)
    (clean : Clean slots base) (baseField : base (slots .radix) = encodeWord B)
    (wordCorrect : MachineFieldTemplate.templateOutput tokens (fun j => base (slots (.field j))) =
      encodeWords values) (ambient : σ) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program tokens slots exit)))^[phaseSteps tokens slots base B values]
      (some ⟨some (emitLabel (MachineFieldTemplate.startAt tokens.length 0)),
        ((ambient, ()), register), base⟩) =
      some ⟨exit, ((ambient, ()), none), resultTapes slots base (CanonicalAddress.radix B values)⟩ :=
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Token, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Tape, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Label, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.chosen, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Clean, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.templateOutput, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.program, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.phaseSteps, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.emitLabel, OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.startAt, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.resultTapes, OAI.UniqueGamesTheorem.Reduction.CanonicalAddress.radix

  38. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.phaseInTime line 398

    Source documentation

    Timed witness with the exact sum of the five concrete phase counts.

    def phaseInTime (tokens : List (MachineFieldTemplate.Token q)) (slots : Tape q width ↪ K)
    (place : Label tokens.length width (chosen slots) → Λ) (exit : Option Λ)
    (P : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State σ))
…

    Mentions: OAI.UniqueGamesTheorem.Reduction.MachineFieldTemplate.Token, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Tape, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Label, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.chosen, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.Alphabet, OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.State

  39. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.copiedLength_le line 417
  40. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.lengthSum_le line 435
  41. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.timePolynomial line 449

    Source documentation

    A fixed polynomial in a magnitude bounding input fields, the serialized word list, the radix, and the digits. Width and token count are static.

    noncomputable def timePolynomial (tokenCount width : Nat) : Polynomial Nat :=
…
  42. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.timePolynomial_eval line 455
  43. theorem OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.phaseSteps_le_timePolynomial line 461
  44. def OAI.UniqueGamesTheorem.Reduction.MachineTemplateAddress.phaseInPolynomialTime line 494