OAI/Computability/MaxCut/PCP/DescriptorEmission.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

An actual fixed finite traversal of all query/noise tapes. The finite control contains one branch for each prescribed tape. The input-dependent signature and the three address bases remain in registers throughout.

  1. def OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.codedEquation line 14
  2. def OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorWords line 18
  3. def OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorBits line 21
  4. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorWords_length line 24
  5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorBits_length_le line 28
  6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.decode_descriptorBits line 32
  7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.parse_descriptorWords line 36
  8. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.decode_codedEquation line 44

    Source documentation

    Decoding the finite address suffixes recovers the exact local equation, including all repeated occurrences and the Boolean correction.

    theorem decode_codedEquation (u D : ℕ) (state : LocalInput u D) :
    mapEquation (localKeyEncoding u).code.symm (codedEquation u D state) =
      SourceLocalEquation.emit u D state := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.mapEquation, OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.codedEquation, OAI.MaxCutGames.Foundations.Hastad.SourceLocalEquation.emit

  9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.codedEquation_global line 55
  10. def OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorPushBound line 64
  11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorPushBound_le line 67
  12. instance OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.localInputDecidableEq line 84

    Source documentation

    Executable state equality is obtained from the explicit radix code.

    instance localInputDecidableEq (u D : ℕ) : DecidableEq (LocalInput u D) :=
…
  13. def OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor line 92

    Source documentation

    Concrete finite-table statement. Its state is the finite signature/tape pair; every branch leaf contains a fixed finite push chain.

    def emitDescriptor (u D : ℕ) (dst : K)
    (next : TM2.Stmt (fun _ : K => Bool) Λ (LocalInput u D)) :
    TM2.Stmt (fun _ : K => Bool) Λ (LocalInput u D) :=
…
  14. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.stepAux_emitDescriptor line 98
  15. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor_push_bound line 109
  16. def OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptorInTime line 118

    Source documentation

    One actual TM2 transition emits the descriptor and enters the chosen continuation label. Only a program-definition equation is required.

    def emitDescriptorInTime (u D : ℕ) (dst : K)
    (program : Λ → TM2.Stmt (fun _ : K => Bool) Λ (LocalInput u D))
    (label exitLabel : Λ)
    (atLabel : program label = emitDescriptor u D dst (.goto (fun _ => exitLabel)))
    (state : LocalInput u D) (tapes : K → List Bool) :
    StateTransition.EvalsToInTime (TM2.step program)
      ⟨some label, state, tapes⟩
      (some ⟨some exitLabel, state,
        Function.update tapes dst (descriptorBits u D state ++ tapes dst)⟩) 1 :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.emitDescriptor, OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.descriptorBits

  17. theorem OAI.MaxCutGames.Foundations.Hastad.SourceDescriptorEmission.descriptor_output_frame line 131
  18. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.Label line 147
  19. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.State line 148
  20. def OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.localEquation line 150
  21. def OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.bodyLabel line 153
  22. def OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.program line 158
  23. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.testTrace line 168

    Source documentation

    The table selector is one real transition; every subsequent copy/push transition belongs to the same fixed program.

    theorem testTrace (u D : ℕ) (sources : Fin 3 → K) (destination scratch : K)
    (sourceDestination : ∀ side, sources side ≠ destination)
    (sourceScratch : ∀ side, sources side ≠ scratch)
    (destinationScratch : destination ≠ scratch) (exit : Option (Label u D))
    (state : LocalInput u D) (base : K → List Bool) (values : Fin 3 → ℕ)
    (sourceWords : ∀ side, base (sources side) = encodeWord (values side))
    (scratchEmpty : base scratch = []) (register : Option Bool) :
    (MachineComposition.advance (TM2.step (program u D sources destination scratch exit)))^[
      SourceEquationEmit.steps values (localEquation u D state) + 1]
        (some ⟨some (.inl ()), (state, register), base⟩) =
      some ⟨exit, (state, none),
        prefixTapes destination base (words values (localEquation u D state))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.program, OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.steps, OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.localEquation

  24. def OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.testInTime line 189
  25. def OAI.MaxCutGames.Foundations.Hastad.SourceTestEmit.sourceTestInTime line 206
  26. inductive OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Label line 244
  27. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.State line 249
  28. structure OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Layout line 251
  29. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.equationBits line 263
  30. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.steps line 266
  31. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.bodyLabel line 272
  32. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.statement line 276
  33. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.program line 285
  34. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes line 289
  35. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes_other line 292
  36. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes_source line 296
  37. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes_temporary line 300
  38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes_scratch line 304
  39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.emitTrace line 309

    Source documentation

    Placement-aware finite selection plus actual equation emission.

    theorem emitTrace (u D : Nat) (layout : Layout K) (labels : Label u D → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State u D))
    (atLabels : ∀ label, p (labels label) = statement u D layout labels exit label)
    (state : LocalInput u D) (base : K → List Bool) (values : Fin 3 → Nat)
    (sourceWords : ∀ side, base (layout.sources side) = encodeWord (values side))
    (scratchEmpty : base layout.scratch = []) (register : Option Bool) :
    (MachineComposition.advance (TM2.step p))^[
      SourceEquationEmit.steps values (localEquation u D state) + 1]
      (some ⟨some (labels (.test (.inl ()))), (state, register), base⟩) =
      some ⟨some (labels .append), (state, none),
        prefixTapes layout.temporary base (words values (localEquation u D state))⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.State, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.statement, OAI.MaxCutGames.Foundations.Hastad.SourceEquationEmit.steps

  40. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.appendTrace line 338

    Source documentation

    Exact one-record append trace in an arbitrary caller program.

    theorem appendTrace (u D : Nat) (layout : Layout K) (labels : Label u D → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State u D))
    (atLabels : ∀ label, p (labels label) = statement u D layout labels exit label)
    (state : LocalInput u D) (base : K → List Bool) (values : Fin 3 → Nat)
    (sourceWords : ∀ side, base (layout.sources side) = encodeWord (values side))
    (scratchEmpty : base layout.scratch = []) (temporaryEmpty : base layout.temporary = [])
    (register : Option Bool) :
    (MachineComposition.advance (TM2.step p))^[steps u D values state]
      (some ⟨some (labels (.test (.inl ()))), (state, register), base⟩) =
      some ⟨exit, (state, none), resultTapes layout base (equationBits u D values state)⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.State, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.statement, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.steps, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.equationBits

  41. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.appendInTime line 381
  42. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.programInTime line 397
  43. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.sourceAppendInTime line 409
  44. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Tape line 445
  45. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.standardLayout line 447
  46. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.machine line 459
  47. def OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.machineInTime line 470
  48. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.Query line 492
  49. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.State line 493
  50. inductive OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.Label line 495
  51. def OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.finish line 502
  52. def OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.statement line 508
  53. def OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.prefixBits line 520
  54. def OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.prefixSteps line 526
  55. theorem OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.resultTapes_append line 532
  56. theorem OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.prefixTrace line 543
  57. theorem OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.prefixSteps_le line 595
  58. theorem OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.loopInTime line 608

    Source documentation

    The complete finite traversal, including its final exit transition.

    theorem loopInTime (u D n B : Nat) (queries : Nat → Query u D)
    (layout : SourceTestAppend.Layout K) (labels : Label u D n → Λ) (exit : Option Λ)
    (p : Λ → TM2.Stmt (fun _ : K => Bool) Λ (State u D))
    (atLabels : ∀ l, p (labels l) = statement u D n queries layout labels exit l)
    (signature : Signature u) (initialQuery : Query u D)
    (base : K → List Bool) (values : Fin 3 → Nat)
    (sourceWords : ∀ side, base (layout.sources side) = encodeWord (values side))
    (scratchEmpty : base layout.scratch = []) (temporaryEmpty : base layout.temporary = [])
    (hbound : ∀ i, i < n → SourceTestAppend.steps u D values (signature, queries i) ≤ B) :
    ∃ lastQuery : Query u D,
      Nonempty (StateTransition.EvalsToInTime (TM2.step p)
        ⟨some (labels (.load ⟨0, by omega⟩)), ((signature, initialQuery), none), base⟩
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.Layout, OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.Label, OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.State, OAI.MaxCutGames.Foundations.Hastad.SourceQueryLoop.statement, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.steps