OAI/Computability/TypeSystem/Spaces.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

Set-theoretic free observation spaces. The four fixed sets are normal keys, tagged plain payloads, base observations, and exit observations. The construction is independent of any typing choices.

  1. inductive OAI.PureTypeSystem.FreeObservations.Payload line 16
  2. abbrev OAI.PureTypeSystem.FreeObservations.Frame line 21
  3. abbrev OAI.PureTypeSystem.FreeObservations.ContinueStack line 22
  4. abbrev OAI.PureTypeSystem.FreeObservations.ExitStack line 23
  5. structure OAI.PureTypeSystem.FreeObservations.Table line 25
  6. def OAI.PureTypeSystem.FreeObservations.Payload.map line 33
  7. theorem OAI.PureTypeSystem.FreeObservations.Payload.map_id line 38
  8. theorem OAI.PureTypeSystem.FreeObservations.Payload.map_comp line 39
  9. theorem OAI.PureTypeSystem.FreeObservations.Payload.map_injective line 42
  10. theorem OAI.PureTypeSystem.FreeObservations.Payload.map_surjective line 47
  11. def OAI.PureTypeSystem.FreeObservations.mapFrame line 59
  12. def OAI.PureTypeSystem.FreeObservations.mapContinue line 62
  13. def OAI.PureTypeSystem.FreeObservations.mapExit line 65
  14. theorem OAI.PureTypeSystem.FreeObservations.mapFrame_id line 68
  15. theorem OAI.PureTypeSystem.FreeObservations.mapFrame_comp line 71
  16. theorem OAI.PureTypeSystem.FreeObservations.mapContinue_id line 75
  17. theorem OAI.PureTypeSystem.FreeObservations.mapContinue_comp line 80
  18. theorem OAI.PureTypeSystem.FreeObservations.mapExit_id line 87
  19. theorem OAI.PureTypeSystem.FreeObservations.mapExit_comp line 90
  20. theorem OAI.PureTypeSystem.FreeObservations.mapFrame_injective line 94
  21. theorem OAI.PureTypeSystem.FreeObservations.mapFrame_surjective line 101
  22. theorem OAI.PureTypeSystem.FreeObservations.mapContinue_injective line 107
  23. theorem OAI.PureTypeSystem.FreeObservations.mapContinue_surjective line 111
  24. theorem OAI.PureTypeSystem.FreeObservations.mapExit_injective line 115
  25. theorem OAI.PureTypeSystem.FreeObservations.mapExit_surjective line 121
  26. def OAI.PureTypeSystem.FreeObservations.Table.relabel line 130
  27. theorem OAI.PureTypeSystem.FreeObservations.Table.relabel_id line 134
  28. theorem OAI.PureTypeSystem.FreeObservations.Table.relabel_comp line 137
  29. def OAI.PureTypeSystem.FreeObservations.Table.default line 141
  30. theorem OAI.PureTypeSystem.FreeObservations.Table.relabel_default line 145
  31. theorem OAI.PureTypeSystem.FreeObservations.Table.relabel_injective line 148
  32. theorem OAI.PureTypeSystem.FreeObservations.Table.relabel_surjective line 159
  33. theorem OAI.PureTypeSystem.FreeObservations.Table.relabel_range_iff line 168

    Source documentation

    Exact factorization through a surjective payload map, simultaneously at all finite lengths. No continuity/topology is assumed.

    theorem relabel_range_iff {f : X → Y} (hf : Function.Surjective f) (t : Table Q V B O X) :
    (∃ s, relabel f s = t) ↔
      (∀ a b, mapContinue f a = mapContinue f b → t.continuing a = t.continuing b) ∧
      (∀ a b, mapExit f a = mapExit f b → t.exiting a = t.exiting b) := by
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Table, OAI.PureTypeSystem.FreeObservations.Table.relabel, OAI.PureTypeSystem.FreeObservations.mapContinue, OAI.PureTypeSystem.FreeObservations.mapExit

  34. def OAI.PureTypeSystem.FreeObservations.Table.slice line 189

    Source documentation

    Prefix a continue frame. Its slicing operation commutes with relabeling.

    def slice (t : Table Q V B O X) (a : Frame Q V X) : Table Q V B O X where
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Table, OAI.PureTypeSystem.FreeObservations.Frame

  35. theorem OAI.PureTypeSystem.FreeObservations.Table.slice_relabel line 193
  36. def OAI.PureTypeSystem.FreeObservations.Stage line 199
  37. def OAI.PureTypeSystem.FreeObservations.step line 204
  38. theorem OAI.PureTypeSystem.FreeObservations.step_injective line 211
  39. def OAI.PureTypeSystem.FreeObservations.inclusion line 217
  40. theorem OAI.PureTypeSystem.FreeObservations.inclusion_self line 220
  41. theorem OAI.PureTypeSystem.FreeObservations.inclusion_succ line 223
  42. theorem OAI.PureTypeSystem.FreeObservations.inclusion_trans line 227
  43. instance OAI.PureTypeSystem.FreeObservations.stageDirectedSystem line 231
  44. theorem OAI.PureTypeSystem.FreeObservations.inclusion_injective line 236
  45. abbrev OAI.PureTypeSystem.FreeObservations.Minus line 254
  46. abbrev OAI.PureTypeSystem.FreeObservations.Plus line 256
  47. def OAI.PureTypeSystem.FreeObservations.embed line 259
  48. theorem OAI.PureTypeSystem.FreeObservations.embed_injective line 262
  49. theorem OAI.PureTypeSystem.FreeObservations.embed_inclusion line 265
  50. theorem OAI.PureTypeSystem.FreeObservations.embed_step line 269
  51. theorem OAI.PureTypeSystem.FreeObservations.exists_embed line 273
  52. theorem OAI.PureTypeSystem.FreeObservations.exists_embed_succ line 277
  53. def OAI.PureTypeSystem.FreeObservations.restrict line 282
  54. theorem OAI.PureTypeSystem.FreeObservations.restrict_surjective line 286
  55. theorem OAI.PureTypeSystem.FreeObservations.restrict_compat line 289
  56. theorem OAI.PureTypeSystem.FreeObservations.restrict_inclusion line 296
  57. def OAI.PureTypeSystem.FreeObservations.stageBehavior line 304
  58. theorem OAI.PureTypeSystem.FreeObservations.stageBehavior_injective line 309
  59. theorem OAI.PureTypeSystem.FreeObservations.stageBehavior_step line 314
  60. theorem OAI.PureTypeSystem.FreeObservations.stageBehavior_inclusion line 325
  61. def OAI.PureTypeSystem.FreeObservations.behavior line 334
  62. theorem OAI.PureTypeSystem.FreeObservations.behavior_embed line 338
  63. theorem OAI.PureTypeSystem.FreeObservations.behavior_injective line 342
  64. def OAI.PureTypeSystem.FreeObservations.plusDefault line 346
  65. def OAI.PureTypeSystem.FreeObservations.minusDefault line 348
  66. theorem OAI.PureTypeSystem.FreeObservations.behavior_default line 351
  67. theorem OAI.PureTypeSystem.FreeObservations.behavior_range_iff line 356

    Source documentation

    The finite bound is ONE stage for ALL finite input lengths.

    theorem behavior_range_iff (t : Table Q V B O (Plus Q V B O)) :
    (∃ x, behavior Q V B O x = t) ↔ ∃ r,
      (∀ a a', mapContinue (restrict Q V B O r) a = mapContinue (restrict Q V B O r) a' →
        t.continuing a = t.continuing a') ∧
      (∀ a a', mapExit (restrict Q V B O r) a = mapExit (restrict Q V B O r) a' →
        t.exiting a = t.exiting a') := by
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Table, OAI.PureTypeSystem.FreeObservations.Plus, OAI.PureTypeSystem.FreeObservations.behavior, OAI.PureTypeSystem.FreeObservations.mapContinue, OAI.PureTypeSystem.FreeObservations.restrict, OAI.PureTypeSystem.FreeObservations.mapExit

  68. theorem OAI.PureTypeSystem.FreeObservations.slice_range line 371

    Source documentation

    Slicing represented behaviors preserves the same finite stage.

    theorem slice_range (x : Minus Q V B O) (a : Frame Q V (Plus Q V B O)) :
    ∃ y, behavior Q V B O y = (behavior Q V B O x).slice a := by
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Minus, OAI.PureTypeSystem.FreeObservations.Frame, OAI.PureTypeSystem.FreeObservations.Plus, OAI.PureTypeSystem.FreeObservations.behavior

  69. def OAI.PureTypeSystem.FreeObservations.minusSlice line 377
  70. theorem OAI.PureTypeSystem.FreeObservations.behavior_minusSlice line 380
  71. structure OAI.PureTypeSystem.PlainSpaces.Schema line 396
  72. inductive OAI.PureTypeSystem.PlainSpaces.Schema.Path line 404
  73. inductive OAI.PureTypeSystem.PlainSpaces.Schema.Slot line 410

    Source documentation

    The occurrence of a payload along a raw finite path. Certificates of a particular domain introduce no computational information.

    inductive Slot : {n : N} → F.Path n → N → Type u
  | head {n : N} {a : F.Key n} {p : F.Path (F.target n a)} {d : N}
      (h : F.domain n a = some d) : Slot (.cons a p) d
  | tail {n : N} {a : F.Key n} {p : F.Path (F.target n a)} {d : N}
      (s : Slot p d) : Slot (.cons a p) d

/-- A domain can be used after any finite number of continuation frames. -/
  74. inductive OAI.PureTypeSystem.PlainSpaces.Schema.Dependency line 417

    Source documentation

    A domain can be used after any finite number of continuation frames.

    inductive Dependency : N → N → Prop
  | head {n : N} (a : F.Key n) {d : N} (h : F.domain n a = some d) : Dependency d n
  | tail {n d : N} (a : F.Key n) (h : Dependency d (F.target n a)) : Dependency d n

namespace Slot
variable {F}

    Mentions: OAI.PureTypeSystem.PlainSpaces.Schema.Slot

  75. theorem OAI.PureTypeSystem.PlainSpaces.Schema.Slot.dependency line 423
  76. abbrev OAI.PureTypeSystem.PlainSpaces.Schema.Parameters line 429
  77. abbrev OAI.PureTypeSystem.PlainSpaces.Schema.FrameParameters line 432
  78. abbrev OAI.PureTypeSystem.PlainSpaces.Schema.Table line 435
  79. def OAI.PureTypeSystem.PlainSpaces.Schema.Space line 438
  80. theorem OAI.PureTypeSystem.PlainSpaces.Schema.space_eq line 441
  81. def OAI.PureTypeSystem.PlainSpaces.Schema.unfold line 445
  82. def OAI.PureTypeSystem.PlainSpaces.Schema.Parameters.nil line 451
  83. def OAI.PureTypeSystem.PlainSpaces.Schema.Parameters.head line 453
  84. def OAI.PureTypeSystem.PlainSpaces.Schema.Parameters.tail line 457
  85. def OAI.PureTypeSystem.PlainSpaces.Schema.Parameters.cons line 461
  86. theorem OAI.PureTypeSystem.PlainSpaces.Schema.Parameters.head_cons line 466
  87. theorem OAI.PureTypeSystem.PlainSpaces.Schema.Parameters.tail_cons line 468
  88. theorem OAI.PureTypeSystem.PlainSpaces.Schema.Parameters.cons_head_tail line 470
  89. theorem OAI.PureTypeSystem.PlainSpaces.Schema.Parameters.nil_unique line 475
  90. def OAI.PureTypeSystem.PlainSpaces.Schema.prefixEquiv line 481

    Source documentation

    Splitting all-path tables at their first frame.

    noncomputable def prefixEquiv (hw : WellFounded F.Dependency) (B : Type u) (n : N) :
    F.Space hw B n ≃ B × ((a : F.Key n) → F.FrameParameters (F.Space hw B) a →
      F.Space hw B (F.target n a)) where
…
  91. def OAI.PureTypeSystem.PlainSpaces.Schema.distinguished line 509

    Source documentation

    Constant tables give compatible distinguished parameters with no additional choice of an inhabitant at any recursive node.

    noncomputable def distinguished (hw : WellFounded F.Dependency) {B : Type u} (b : B) (n : N) :
    F.Space hw B n := (F.unfold hw B n).symm (fun _ _ => b)
  92. theorem OAI.PureTypeSystem.PlainSpaces.Schema.distinguished_base line 512
  93. theorem OAI.PureTypeSystem.PlainSpaces.Schema.distinguished_next line 516
  94. def OAI.PureTypeSystem.FreeObservations.InStage line 530

    Source documentation

    Membership in a specified finite minus stage, not just in the limit.

    def InStage (n : ℕ) (x : Minus Q V B O) : Prop :=
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Minus

  95. def OAI.PureTypeSystem.FreeObservations.Agree line 534

    Source documentation

    The finite observation equivalence on unrestricted plus tables.

    def Agree (n : ℕ) (p q : Plus Q V B O) : Prop :=
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Plus

  96. theorem OAI.PureTypeSystem.FreeObservations.InStage.mono line 539
  97. theorem OAI.PureTypeSystem.FreeObservations.InStage.not_zero line 544
  98. theorem OAI.PureTypeSystem.FreeObservations.InStage.exists_stage line 548
  99. theorem OAI.PureTypeSystem.FreeObservations.Agree.mono line 555
  100. theorem OAI.PureTypeSystem.FreeObservations.Agree.refl line 560
  101. theorem OAI.PureTypeSystem.FreeObservations.Agree.symm line 562
  102. theorem OAI.PureTypeSystem.FreeObservations.Agree.trans line 564
  103. theorem OAI.PureTypeSystem.FreeObservations.inStage_succ_iff line 571

    Source documentation

    Exact characterization at a specified stage, used for the uniform bound at a minus lambda.

    theorem inStage_succ_iff (b : B) (o : O) (n : ℕ) (x : Minus Q V B O) :
    InStage (n+1) x ↔
      (∀ a a', mapContinue (restrict Q V B O n) a = mapContinue (restrict Q V B O n) a' →
          (behavior Q V B O x).continuing a = (behavior Q V B O x).continuing a') ∧
      (∀ a a', mapExit (restrict Q V B O n) a = mapExit (restrict Q V B O n) a' →
          (behavior Q V B O x).exiting a = (behavior Q V B O x).exiting a') := by
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Minus, OAI.PureTypeSystem.FreeObservations.InStage, OAI.PureTypeSystem.FreeObservations.mapContinue, OAI.PureTypeSystem.FreeObservations.restrict, OAI.PureTypeSystem.FreeObservations.behavior, OAI.PureTypeSystem.FreeObservations.mapExit

  104. theorem OAI.PureTypeSystem.FreeObservations.exists_inStage_behavior line 586

    Source documentation

    A table with the uniform finite invariance is represented at exactly the promised next stage. This is stronger than mere totality in the colimit.

    theorem exists_inStage_behavior (b : B) (o : O) (n : ℕ)
    (t : Table Q V B O (Plus Q V B O))
    (hc : ∀ a a', mapContinue (restrict Q V B O n) a = mapContinue (restrict Q V B O n) a' →
      t.continuing a = t.continuing a')
    (he : ∀ a a', mapExit (restrict Q V B O n) a = mapExit (restrict Q V B O n) a' →
      t.exiting a = t.exiting a') :
    ∃ x, InStage (n+1) x ∧ behavior Q V B O x = t := by
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Table, OAI.PureTypeSystem.FreeObservations.Plus, OAI.PureTypeSystem.FreeObservations.mapContinue, OAI.PureTypeSystem.FreeObservations.restrict, OAI.PureTypeSystem.FreeObservations.mapExit, OAI.PureTypeSystem.FreeObservations.InStage, OAI.PureTypeSystem.FreeObservations.behavior

  105. theorem OAI.PureTypeSystem.FreeObservations.inStage_minusSlice line 597

    Source documentation

    Slicing remains in the same finite minus stage.

    theorem inStage_minusSlice (b : B) (o : O) {n : ℕ} {x : Minus Q V B O} (hx : InStage n x)
    (a : Frame Q V (Plus Q V B O)) : InStage n (minusSlice x a) := by
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Minus, OAI.PureTypeSystem.FreeObservations.InStage, OAI.PureTypeSystem.FreeObservations.Frame, OAI.PureTypeSystem.FreeObservations.Plus, OAI.PureTypeSystem.FreeObservations.minusSlice

  106. def OAI.PureTypeSystem.FreeObservations.lambdaTable line 611

    Source documentation

    A raw lambda table. Its body is selected by a continuing first frame; its exit operation is selected by the unique terminal frame. Gates and invalid-frame defaults can be included in these two functions.

    def lambdaTable (base : B)
    (body : Frame Q V (Plus Q V B O) → Minus Q V B O)
    (exit : Frame Q V (Plus Q V B O) → O) : Table Q V B O (Plus Q V B O) where
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Frame, OAI.PureTypeSystem.FreeObservations.Plus, OAI.PureTypeSystem.FreeObservations.Minus, OAI.PureTypeSystem.FreeObservations.Table

  107. theorem OAI.PureTypeSystem.FreeObservations.lambdaTable_representable line 623

    Source documentation

    The representability step at a minus lambda. The finite level is uniform across all first frames and all stack lengths, not a pointwise bound.

    theorem lambdaTable_representable (b : B) (o : O) (n : ℕ) (base : B)
    (body : Frame Q V (Plus Q V B O) → Minus Q V B O)
    (exit : Frame Q V (Plus Q V B O) → O)
    (hb : ∀ a, InStage (n+1) (body a))
    (hc : ∀ a a', mapFrame (restrict Q V B O n) a = mapFrame (restrict Q V B O n) a' →
      body a = body a')
    (he : ∀ a a', mapFrame (restrict Q V B O n) a = mapFrame (restrict Q V B O n) a' →
      exit a = exit a') :
    ∃ x, InStage (n+1) x ∧ behavior Q V B O x = lambdaTable base body exit := by
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Frame, OAI.PureTypeSystem.FreeObservations.Plus, OAI.PureTypeSystem.FreeObservations.Minus, OAI.PureTypeSystem.FreeObservations.InStage, OAI.PureTypeSystem.FreeObservations.mapFrame, OAI.PureTypeSystem.FreeObservations.restrict, OAI.PureTypeSystem.FreeObservations.behavior, OAI.PureTypeSystem.FreeObservations.lambdaTable

  108. def OAI.PureTypeSystem.FreeObservations.FrameBound line 666
  109. def OAI.PureTypeSystem.FreeObservations.ContinueBound line 669
  110. def OAI.PureTypeSystem.FreeObservations.ExitBound line 672
  111. theorem OAI.PureTypeSystem.FreeObservations.FrameBound.mono line 677
  112. theorem OAI.PureTypeSystem.FreeObservations.FrameBound.exists_preimage line 680
  113. theorem OAI.PureTypeSystem.FreeObservations.FrameBound.embed line 690
  114. theorem OAI.PureTypeSystem.FreeObservations.ContinueBound.mono line 704
  115. theorem OAI.PureTypeSystem.FreeObservations.ContinueBound.exists_preimage line 707
  116. theorem OAI.PureTypeSystem.FreeObservations.ContinueBound.embed line 716
  117. theorem OAI.PureTypeSystem.FreeObservations.ContinueBound.cons line 722
  118. theorem OAI.PureTypeSystem.FreeObservations.Agree.continuing line 732
  119. theorem OAI.PureTypeSystem.FreeObservations.Agree.exiting line 737
  120. theorem OAI.PureTypeSystem.FreeObservations.Agree.of_observations line 745
  121. theorem OAI.PureTypeSystem.FreeObservations.Agree.slice line 754
  122. theorem OAI.PureTypeSystem.FreeObservations.Agree.all_levels_eq line 762
  123. theorem OAI.PureTypeSystem.FreeObservations.minusSlice_eq_of_restrict line 791
  124. theorem OAI.PureTypeSystem.FreeObservations.minusExit_eq_of_restrict line 805
  125. def OAI.PureTypeSystem.FreeObservations.plusLambdaTable line 815

    Source documentation

    The unrestricted plus-side analogue of the minus lambda table.

    def plusLambdaTable (base : B) (body : Frame Q V (Minus Q V B O) → Plus Q V B O)
    (exit : Frame Q V (Minus Q V B O) → O) : Plus Q V B O where
…

    Mentions: OAI.PureTypeSystem.FreeObservations.Frame, OAI.PureTypeSystem.FreeObservations.Minus, OAI.PureTypeSystem.FreeObservations.Plus

  126. theorem OAI.PureTypeSystem.FreeObservations.plusLambdaTable_agree line 824