OAI/Computability/MaxCut/PCP/ProfileBridge.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.positionEncoding line 12
2. def OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.names line 15
3. def OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.nameWords line 19
4. def OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.reindexProfile line 23
5. theorem OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.computed_profile_eq line 27
6. theorem OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.prepared_signature_eq line 35
7. theorem OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.nameWords_length_le_input line 45

   Source documentation

   Every isolated unary variable-name field is bounded by the true CNF input encoding, including formulas with unused declared variable names.

   theorem nameWords_length_le_input (F : Formula) {u : ℕ} (c : ClauseContext F u)
       (i : Fin (positionEncoding u).size) :
       (nameWords F c i).length ≤ (formulaBits F).length := by
   …

   Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.positionEncoding, OAI.MaxCutGames.Foundations.Hastad.SourceProfileBridge.nameWords

8. def OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.positions line 63

   Source documentation

   An explicit computable enumeration, without an arbitrary finite-type equivalence. Slots occur first, second, third within each clause coordinate.

   def positions (u : ℕ) : List (Position u) :=
   …

9. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.mem_positions line 66
10. def OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.fillSigns line 70

    Source documentation

    The mathematical result of the individual finite sign-register writes.

    def fillSigns {u : ℕ} (values initial : Position u → Bool)
        (cells : List (Position u)) : Position u → Bool :=
    …

11. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.fillSigns_apply line 74
12. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.fillSigns_positions line 88
13. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.State line 96
14. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.Alphabet line 97
15. def OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.finish line 99
16. def OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.peekChain line 106

    Source documentation

    Each statement reads only the head of one supplied polarity field. The other signature fields and the entire ambient-register component are copied.

    def peekChain (field : Position u → K) (exit : Option Λ) :
        List (Position u) → TM2.Stmt (Alphabet (K := K)) Λ (State u τ)
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.Alphabet, OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.State

17. def OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.statement line 114
18. def OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.readSigns line 120

    Source documentation

    The head defaults make the finite program total on malformed tapes too; the correctness theorem below supplies the actual unary-field representation.

    def readSigns (field : Position u → K) (tapes : K → List Bool) : Position u → Bool :=
    …

19. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.stepAux_peekChain line 123
20. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.stepAux_statement line 136
21. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.peekChain_pushBound line 143
22. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.statement_pushBound line 151
23. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.readSigns_of_unary line 156
24. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.loadStep line 166

    Source documentation

    Exact actual caller-program step. Every stored field and unread suffix is preserved, as are sameName, selected, and all ambient registers.

    theorem loadStep (field : Position u → K) (entryLabel : Λ) (exit : Option Λ)
        (program : Λ → TM2.Stmt (Alphabet (K := K)) Λ (State u τ))
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.Alphabet, OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.State

25. def OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.loadInTime line 177
26. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.loaded_ofContext line 196

    Source documentation

    The actual context signature is recovered when equality and selected-slot data have already been loaded by their separate verified preparation stages.

    theorem loaded_ofContext (F : Target.Formula) (c : SourceContexts.ClauseContext F u)
        (selected : SourceContexts.SlotContext u) (initial : Signature u)
        (hnames : initial.sameName = contextNameProfile F c)
        (hselected : initial.selected = selected) :
        {initial with signs := (ofContext F c selected).signs} = ofContext F c selected := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Target.Formula, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.ClauseContext, OAI.MaxCutGames.Foundations.Hastad.SourceContexts.SlotContext

27. def OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.loadContextInTime line 208
28. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Width line 234
29. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Arena line 235
30. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.ProfileState line 236
31. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.State line 237
32. abbrev OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.ProfileLabel line 238
33. inductive OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Label line 240
34. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.variableField line 247
35. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.polarityField line 250
36. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.place line 253
37. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.unplace line 257
38. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.unplace_place line 267
39. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.place_injective line 280
40. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.place_unplace line 285
41. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.fill line 317
42. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.fill_place line 323
43. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.fill_self line 328
44. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.fill_frame line 336
45. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.fill_update line 343
46. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.placedLabel line 366
47. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.placedConfiguration line 370
48. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.placedStatement line 376
49. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.placed_stepAux line 391
50. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.signStateEquiv line 419

    Source documentation

    Reassociate finite registers without adding a transition.

    def signStateEquiv (u : ℕ) (τ : Type) :
        SourceSignLoad.State u (ProfileState u × τ) ≃ State u τ where
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceSignLoad.State, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.ProfileState, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.State

51. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.commitStatement line 426
52. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.program line 432
53. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.placed_step line 437
54. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.stepAux_commit line 454
55. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.profileInTime line 467

    Source documentation

    The actual profile execution, placed in the loaded context arena.

    def profileInTime (tapes : Arena u Extra → List Bool)
        (hwork : ∀ w : Fin 3, tapes (place (.inr w)) = [])
        (initialProfile : MachineFieldProfile.Profile (Width u))
        (initial : Signature u) (ambient : τ) (L : ℕ)
        (hL : ∀ i, (tapes (place (.inl i))).length ≤ L) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (.profile (MachineFieldProfile.labelAt (MachineFieldProfile.allPairs (Width u)) 0 0)),
            (MachineFieldProfile.normalState initialProfile, (initial, ambient)), tapes⟩
          (some ⟨some .commit,
            (MachineFieldProfile.normalState
              (MachineFieldProfile.equalityProfile (fun i => tapes (place (.inl i)))),
              (initial, ambient)), tapes⟩)
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Arena, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.place, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Width, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.program

56. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.commitInTime line 487
57. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.prepareInTime line 502

    Source documentation

    Actual preparation from isolated name fields and unary sign fields. The conclusion preserves every tape and arbitrary caller metadata.

    def prepareInTime (F : Formula) (c : ClauseContext F u) (selected : SlotContext u)
        (tapes : Arena u Extra → List Bool)
        (hwork : ∀ w : Fin 3, tapes (place (.inr w)) = [])
        (hnames : ∀ i, tapes (place (.inl i)) = nameWords F c i)
        (suffix : Position u → List Bool)
        (hsigns : ∀ p, tapes (polarityField p) =
          encodeWord (if positiveAt (clauseAt F (c p.1)) p.2 then 1 else 0) ++ suffix p)
        (initialProfile : MachineFieldProfile.Profile (Width u))
        (initial : Signature u) (hselected : initial.selected = selected) (ambient : τ) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (.profile (MachineFieldProfile.labelAt (MachineFieldProfile.allPairs (Width u)) 0 0)),
            (MachineFieldProfile.normalState initialProfile, (initial, ambient)), tapes⟩
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Arena, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.place, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.polarityField, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Width, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.program

58. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.loaded_name_field line 541
59. theorem OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.loaded_sign_field line 560

    Source documentation

    Unary sign fields may retain arbitrary old suffixes: only the leading sign bit is read.

    theorem loaded_sign_field (F : Formula) (c : ClauseContext F u)
        (base : Arena u Extra → List Bool) (p : Position u) :
        SourceContextLoad.stageTapes F c base u (polarityField p) =
          encodeWord (if positiveAt (clauseAt F (c p.1)) p.2 then 1 else 0) ++
            base (polarityField p) := by
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Arena, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.polarityField

60. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.loadedPrepareInTime line 575

    Source documentation

    Exactly the loaded context signature is computed by the concrete finite program. Scratch is reset and all loaded fields and caller tapes are preserved.

    def loadedPrepareInTime (F : Formula) (c : ClauseContext F u) (selected : SlotContext u)
        (base : Arena u Extra → List Bool)
        (hindex : base .index = []) (hwork : base .work = []) (hscratch : base .scratch = [])
        (hbase : ∀ p : Position u, base (variableField p) = [])
        (initialProfile : MachineFieldProfile.Profile (Width u))
        (initial : Signature u) (hselected : initial.selected = selected) (ambient : τ) :
        StateTransition.EvalsToInTime (TM2.step program)
          ⟨some (.profile (MachineFieldProfile.labelAt (MachineFieldProfile.allPairs (Width u)) 0 0)),
            (MachineFieldProfile.normalState initialProfile, (initial, ambient)),
            SourceContextLoad.stageTapes F c base u⟩
          (some ⟨none,
            (MachineFieldProfile.normalState (MachineFieldProfile.equalityProfile (nameWords F c)),
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Arena, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.variableField, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Width, OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.program, OAI.MaxCutGames.Foundations.Hastad.SourceContextLoad.stageTapes

61. def OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.machine line 607

    Source documentation

    Finiteness of tape addresses and registers constructs an actual TM2; its execution bound is established above by the concrete transitions.

    def machine (u : ℕ) (Extra τ : Type) [DecidableEq Extra] [Fintype Extra] [Fintype τ]
        (initialProfile : MachineFieldProfile.Profile (Width u))
        (initial : Signature u) (ambient : τ) : FinTM2 where
    …

    Mentions: OAI.MaxCutGames.Foundations.Hastad.SourceSignaturePrepare.Width