OAI/Computability/MaxCut/PCP/TupleBody.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

One actual clause-tuple body. Its fixed finite control loads the context, computes the shared right address base, traverses every selected-slot tuple and query tape in their declared encoding order, and physically clears its work.

  1. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.SlotCount line 17
  2. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.QueryCount line 18
  3. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query line 19
  4. inductive OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label line 21
  5. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.selected line 40
  6. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.main line 43
  7. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.framed line 45
  8. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.framedConfiguration line 50
  9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.framed_stepAux line 59
  10. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.framed_step line 66
  11. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.framedExecution line 81
  12. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.finish line 96
  13. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.drainProgram line 102
  14. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.drainStatement line 106
  15. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.selectState line 113

    Source documentation

    Only the chosen-slot/query registers change; the computed context profile and original signature remain available across all local traversals.

    def selectState (initialQuery : Query u D) (index : Fin (SlotCount u))
    (state : State u D) : State u D :=
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.SlotCount

  16. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program line 118
  17. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.reset_step line 156

    Source documentation

    All finite internal state is reset before the caller continuation.

    theorem reset_step (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (state : State u D) (tapes : Arena u Extra → List Bool) :
    TM2.step (program initialQuery exit) ⟨some .reset, state, tapes⟩ =
      some ⟨exit, canonicalState initialQuery, tapes⟩ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program

  18. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.resetInTime line 162
  19. structure OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Ready line 172

    Source documentation

    The complete representation needed at one odometer leaf. Remaining-digit stacks, output history, and retained unused headers are arbitrary.

    structure Ready (F : Target.Formula) (c : ClauseContext F u)
    (base : Arena u Extra → List Bool) : Prop where
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula

  20. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.contextSignature line 198
  21. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.workingState line 201
  22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.workingState_loader line 206
  23. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.arithmeticMetadata line 210
  24. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.queryMetadata line 216
  25. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.arithmeticState_working line 221
  26. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.queryState_working line 226
  27. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.select_workingState line 231
  28. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.rightValue line 236
  29. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.variableRank line 239
  30. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.leftValue line 242
  31. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.slotBudget line 245
  32. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.preparePhase line 254

    Source documentation

    Concrete context-loader/signature phase in the tuple-body program.

    noncomputable def preparePhase (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (base : Arena u Extra → List Bool)
    (hformula : base .formula = formulaBits F)
    (hcurrent : ∀ j, base (.current j) = encodeWord (c j).val)
    (hindex : base .index = []) (hwork : base .work = [])
    (hscratch : base .scratch = []) (hcopy : base .copyScratch = [])
    (hfields : ∀ p : Position u, base (SourceSignaturePrepare.variableField p) = []) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some main, canonicalState initialQuery, base⟩
      (some ⟨some .seedZero,
        SourceContextPrepare.finalState F c (fun _ => .first)
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.variableField, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.main, OAI.MaxCutGames.Foundations.Hastad.SourceContextPrepare.finalState

  33. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.seedZeroPhase line 277
  34. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.drainPhase line 292

    Source documentation

    The caller only supplies a local code equality; the physical drain and its entire runtime are obtained from the checked drain machine.

    def drainPhase (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (source : Arena u Extra) (entry : Label u D Extra) (next : Option (Label u D Extra))
    (atEntry : program initialQuery exit entry = drainStatement source entry next)
    (base : Arena u Extra → List Bool)
    (metadata : SourceSignaturePrepare.State u (QueryState u D × ArithmeticState))
    (register : Option Bool) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some entry, (((), register), metadata), base⟩
      (some ⟨next, (((), none), metadata), Function.update base source []⟩)
      ((base source).length + 1) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.drainStatement, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.State

  35. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.clauseRankPhase line 306
  36. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.variableRankPhase line 323
  37. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.rightBasePhase line 344
  38. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.leftBasePhase line 366
  39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.queryPhase line 391
  40. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.selectPhase line 417

    Source documentation

    The fixed selected-slot tuple is loaded in one actual transition.

    def selectPhase (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (index : Fin (SlotCount u)) (state : State u D) (base : Arena u Extra → List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some (.select index.castSucc), state, base⟩
      (some ⟨some (.variableRank index .start), selectState initialQuery index state, base⟩) 1 where
…

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.SlotCount, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.variableRank, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.selectState

  41. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.loaded_extra line 429
  42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Ready.loadedClean line 435
  43. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.loopSnapshot line 443
  44. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.rankSnapshot line 446
  45. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.baseSnapshot line 450
  46. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.slotInTime line 456

    Source documentation

    One selected-slot tuple: actual rank, base construction, complete query stream, and physical cleanup, in the one fixed caller program.

    theorem slotInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery beforeQuery : Query u D) (beforeSignature : Signature u)
    (exit : Option (Label u D Extra)) (base : Arena u Extra → List Bool) (h : Ready F c base)
    (index : Fin (SlotCount u)) (bits : List Bool) :
    ∃ afterQuery : Query u D,
      Nonempty (StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
        ⟨some (.select index.castSucc), workingState F c beforeSignature beforeQuery,
          tapes (SourceContextLoad.stageTapes F c base u) (loopSnapshot F c bits)⟩
        (some ⟨some (.select ⟨index.val + 1, by omega⟩),
          workingState F c (ofContext F c (selected index)) afterQuery,
          tapes (SourceContextLoad.stageTapes F c base u)
            (loopSnapshot F c (bits ++ SourceQueryOrder.slotBits F u D c (selected index)))⟩)
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Ready, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.SlotCount, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.workingState, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.loopSnapshot, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.selected, OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.slotBits

  47. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.slotAt line 553
  48. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.prefixBits line 556
  49. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.prefixBudget line 560
  50. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.prefixInTime line 565

    Source documentation

    The explicit finite loop runs in ascending slot-encoding order.

    theorem prefixInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery beforeQuery : Query u D) (beforeSignature : Signature u)
    (exit : Option (Label u D Extra)) (base : Arena u Extra → List Bool) (h : Ready F c base)
    (r : Nat) (hr : r ≤ SlotCount u) :
    ∃ afterSignature : Signature u, ∃ afterQuery : Query u D,
      Nonempty (StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
        ⟨some (.select ⟨0, by omega⟩), workingState F c beforeSignature beforeQuery,
          tapes (SourceContextLoad.stageTapes F c base u) (loopSnapshot F c [])⟩
        (some ⟨some (.select ⟨r, by omega⟩), workingState F c afterSignature afterQuery,
          tapes (SourceContextLoad.stageTapes F c base u)
            (loopSnapshot F c (prefixBits (D := D) F c r))⟩)
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Ready, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.SlotCount, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.workingState, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.loopSnapshot, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.prefixBits

  51. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.prefixBits_eq_ofFn line 598
  52. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.prefixBits_eq_tupleBits line 609
  53. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.setupBudget line 620
  54. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.finishBudget line 630
  55. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.bodyBudget line 633
  56. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.setupInTime line 637

    Source documentation

    Actual context preparation and the shared right base are computed once.

    noncomputable def setupInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (base : Arena u Extra → List Bool) (h : Ready F c base) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some main, canonicalState initialQuery, base⟩
      (some ⟨some (.select ⟨0, by omega⟩),
        workingState F c (canonicalSignature u) initialQuery,
        tapes (SourceContextLoad.stageTapes F c base u) (loopSnapshot F c [])⟩)
      (setupBudget F c) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Ready, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.main, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.workingState, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.loopSnapshot, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.setupBudget

  57. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.finishInTime line 707

    Source documentation

    Physical cleanup and canonical finite-state reset complete the body.

    def finishInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery query : Query u D) (signature : Signature u)
    (exit : Option (Label u D Extra)) (base : Arena u Extra → List Bool) (h : Ready F c base)
    (bits : List Bool) :
    StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some (.select ⟨SlotCount u, by omega⟩), workingState F c signature query,
        tapes (SourceContextLoad.stageTapes F c base u) (loopSnapshot F c bits)⟩
      (some ⟨exit, canonicalState initialQuery, SourceTestAppend.resultTapes queryLayout base bits⟩)
      (finishBudget F c) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Ready, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.SlotCount, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.workingState, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.loopSnapshot, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.finishBudget

  58. theorem OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.bodyInTime line 768

    Source documentation

    One complete actual clause-tuple execution. The only changed tape is the reversed-output accumulator; every internal finite register is reset.

    theorem bodyInTime (F : Target.Formula) (c : ClauseContext F u)
    (initialQuery : Query u D) (exit : Option (Label u D Extra))
    (base : Arena u Extra → List Bool) (h : Ready F c base) :
    Nonempty (StateTransition.EvalsToInTime (TM2.step (program initialQuery exit))
      ⟨some main, canonicalState initialQuery, base⟩
      (some ⟨exit, canonicalState initialQuery,
        SourceTestAppend.resultTapes queryLayout base (SourceQueryOrder.tupleBits F u D c)⟩)
      (bodyBudget (D := D) F c)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Query, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Label, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.Ready, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.program, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.main, OAI.MaxCutGames.Foundations.Hastad.SourceTestAppend.resultTapes, OAI.MaxCutGames.Foundations.Hastad.SourceQueryOrder.tupleBits, OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.bodyBudget

  59. def OAI.MaxCutGames.Foundations.Hastad.SourceTupleBody.machine line 789