OAI/Computability/TypeSystem/Bounds.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PureTypeSystem.ObservationValues.RawValue.level_symm line 15
2. theorem OAI.PureTypeSystem.ObservationValues.RawValue.level_trans line 22
3. theorem OAI.PureTypeSystem.ObservationValues.RawValue.level_fits line 27
4. theorem OAI.PureTypeSystem.ObservationValues.RawValue.level_eq_of_plain line 34
5. theorem OAI.PureTypeSystem.ObservationValues.RawValue.bounded_of_not_minus line 45
6. theorem OAI.PureTypeSystem.ObservationValues.Parameter.level_symm line 55
7. theorem OAI.PureTypeSystem.ObservationValues.Parameter.level_fits line 60
8. theorem OAI.PureTypeSystem.ObservationValues.Parameter.bounded_of_not_minus line 66
9. theorem OAI.PureTypeSystem.ObservationValues.Parameter.bounded_none line 73
10. theorem OAI.PureTypeSystem.ObservationValues.Value.level_asPlus line 78
11. theorem OAI.PureTypeSystem.ObservationValues.Value.level_asMinus line 85
12. theorem OAI.PureTypeSystem.ObservationValues.Value.bounded_asMinus line 91
13. theorem OAI.PureTypeSystem.ObservationValues.distinguished_bounded line 98
14. theorem OAI.PureTypeSystem.ObservationValues.withBase_bounded line 107
15. theorem OAI.PureTypeSystem.ObservationValues.tagPlain_level line 116
16. theorem OAI.PureTypeSystem.ObservationValues.Gate.level_iff line 126
17. theorem OAI.PureTypeSystem.ObservationValues.plusPayload_bounded line 136
18. theorem OAI.PureTypeSystem.ObservationValues.minusPayload_bounded line 144
19. theorem OAI.PureTypeSystem.ObservationValues.minusFrame_restrict line 151
20. def OAI.PureTypeSystem.ObservationValues.ActionBound line 165

    Source documentation

    The local induction hypotheses used at a lambda.

    def ActionBound (T : ActiveType Ω C) (k l : Nat) (act : LambdaAction (hw := hw) Ω C hno T) : Prop :=
    …

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType, OAI.PureTypeSystem.ObservationValues.LambdaAction

21. def OAI.PureTypeSystem.ObservationValues.ActionRelated line 168
22. theorem OAI.PureTypeSystem.ObservationValues.LambdaAction.frame_congr line 175
23. theorem OAI.PureTypeSystem.ObservationValues.ActionRelated.gates line 185
24. theorem OAI.PureTypeSystem.ObservationValues.minusContinue_bounded line 200
25. theorem OAI.PureTypeSystem.ObservationValues.minusContinue_level line 210
26. theorem OAI.PureTypeSystem.ObservationValues.lambdaExit_level line 233
27. theorem OAI.PureTypeSystem.ObservationValues.minusLambda_representable line 258

    Source documentation

    Uniform body estimates prove the exact minus lambda table is in the colimit, so no fallback in packMinus is used.

    theorem minusLambda_representable {T : ActiveType Ω C}
        (hT : FreeLayer P C (Ω.profile T.type) true) {k l : Nat} (hl : 1 ≤ l)
        {act : LambdaAction (hw := hw) Ω C hno T} (hb : ActionBound Ω C hno T k l act)
    …

    Mentions: OAI.PureTypeSystem.ObservationValues.ActiveType, OAI.PureTypeSystem.FreeLayer, OAI.PureTypeSystem.ObservationValues.LambdaAction, OAI.PureTypeSystem.ObservationValues.ActionBound

28. theorem OAI.PureTypeSystem.ObservationValues.Value.level_asPlain line 276
29. theorem OAI.PureTypeSystem.ObservationValues.ActualPlainKey.payload_bounded line 285
30. theorem OAI.PureTypeSystem.ObservationValues.plainLambda_level line 296
31. theorem OAI.PureTypeSystem.ObservationValues.plusContinue_level line 312
32. theorem OAI.PureTypeSystem.ObservationValues.plusLambda_level line 323
33. theorem OAI.PureTypeSystem.ObservationValues.minusLambdaBehavior_level line 343
34. theorem OAI.PureTypeSystem.ObservationValues.lambdaValue_bounded line 355
35. theorem OAI.PureTypeSystem.ObservationValues.lambdaValue_level line 366
36. theorem OAI.PureTypeSystem.ObservationValues.RawValue.level_eq_of_not_plus line 378
37. theorem OAI.PureTypeSystem.ObservationValues.Parameter.level_eq_of_not_plus line 388
38. theorem OAI.PureTypeSystem.ObservationValues.minusFrame_restrict_of_level line 398
39. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.plusParameter_bound line 413
40. theorem OAI.PureTypeSystem.ObservationValues.FrameKey.minusParameter_level line 428
41. theorem OAI.PureTypeSystem.ObservationValues.applyValue_bounded line 439
42. theorem OAI.PureTypeSystem.ObservationValues.applyValue_level line 456
43. theorem OAI.PureTypeSystem.ObservationValues.Environment.imageCompatible_symm line 509
44. theorem OAI.PureTypeSystem.ObservationValues.Environment.level_symm line 512
45. theorem OAI.PureTypeSystem.ObservationValues.Environment.level_cons line 515
46. theorem OAI.PureTypeSystem.ObservationValues.Value.cast_val line 536
47. theorem OAI.PureTypeSystem.ObservationValues.lambdaValue_level_of_type_eq line 540
48. theorem OAI.PureTypeSystem.ObservationValues.applyValue_level_of_type_eq line 552
49. theorem OAI.PureTypeSystem.ObservationValues.PreResult.parameter_eq line 572
50. theorem OAI.PureTypeSystem.ObservationValues.PreResult.parameter_bounded line 576
51. theorem OAI.PureTypeSystem.ObservationValues.PreResult.val_bounded line 585
52. theorem OAI.PureTypeSystem.ObservationValues.PreResult.parameter_level line 590
53. theorem OAI.PureTypeSystem.ObservationValues.PreResult.val_level line 603
54. theorem OAI.PureTypeSystem.ObservationValues.PreResult.baseRead_level line 611
55. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.domain_not_minus line 645
56. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.targetNF_eq line 657
57. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.testers_eq line 662
58. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.fibers_eq line 673
59. theorem OAI.PureTypeSystem.ObservationValues.ProductInstance.candidate_eq line 699
60. abbrev OAI.PureTypeSystem.ObservationValues.Evaluator line 712
61. structure OAI.PureTypeSystem.ObservationValues.Uniform line 717

    Source documentation

    The exact three uniform finite-bound assertions, expressed without identifying dependent candidate/value indices by extra axioms.

    structure Uniform {Γ : List (Expr S)} {M T : Expr S}
        (ev : Evaluator (hw := hw) Ω C hno Γ M T) (F : Nat → Nat) : Prop where
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.ObservationValues.Evaluator

62. theorem OAI.PureTypeSystem.ObservationValues.Uniform.val_bounded line 727
63. theorem OAI.PureTypeSystem.ObservationValues.Uniform.val_level line 732
64. theorem OAI.PureTypeSystem.ObservationValues.PreResult.lookup_parameter line 742
65. theorem OAI.PureTypeSystem.ObservationValues.PreResult.lookup_uniform line 758
66. theorem OAI.PureTypeSystem.ObservationValues.PreResult.sort_uniform line 775
67. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstractionAction_bounded line 794
68. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstractionAction_level line 806
69. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstraction_val_level line 832
70. theorem OAI.PureTypeSystem.ObservationValues.PreResult.abstraction_uniform line 844
71. def OAI.PureTypeSystem.ObservationValues.PreResult.appBound line 868
72. theorem OAI.PureTypeSystem.ObservationValues.PreResult.applicationValue_bounded line 871
73. theorem OAI.PureTypeSystem.ObservationValues.PreResult.applicationValue_level line 886
74. theorem OAI.PureTypeSystem.ObservationValues.PreResult.application_uniform line 918
75. theorem OAI.PureTypeSystem.ObservationValues.Base.update_congr line 938
76. theorem OAI.PureTypeSystem.ObservationValues.withBase_level_of_type_eq line 946
77. theorem OAI.PureTypeSystem.ObservationValues.distinguished_level_of_type_eq line 954
78. def OAI.PureTypeSystem.ObservationValues.PreResult.productBound line 962
79. theorem OAI.PureTypeSystem.ObservationValues.PreResult.productCandidate_level line 964
80. theorem OAI.PureTypeSystem.ObservationValues.PreResult.product_val_level line 995
81. theorem OAI.PureTypeSystem.ObservationValues.PreResult.product_uniform line 1020
82. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_uniform line 1059

    Source documentation

    The manuscript's finite-bound lemma for every stored typing tree. No normalization or candidate restriction is imposed on the raw environment.

    theorem preEvaluate_uniform {Γ : List (Expr S)} {M T : Expr S}
        (hC : IsComponent (PrimaryEdge P) C) (t : TypingTree P Γ M T) :
        ∃ F, Uniform (hw := hw) Ω C hno (preEvaluate Ω C hno t) F := by
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.ObservationValues.Uniform, OAI.PureTypeSystem.ObservationValues.preEvaluate

83. theorem OAI.PureTypeSystem.ObservationValues.RawValue.all_levels_eq line 1079
84. theorem OAI.PureTypeSystem.ObservationValues.Parameter.all_levels_eq line 1088
85. def OAI.PureTypeSystem.ObservationValues.Environment.Compatible line 1097
86. theorem OAI.PureTypeSystem.ObservationValues.Environment.Compatible.level line 1100
87. theorem OAI.PureTypeSystem.ObservationValues.Uniform.compatible line 1110
88. theorem OAI.PureTypeSystem.ObservationValues.preEvaluate_compatible line 1126

    Source documentation

    Compatible-image invariance, including arbitrary raw non-SN images.

    theorem preEvaluate_compatible {Γ : List (Expr S)} {M T : Expr S}
        (hC : IsComponent (PrimaryEdge P) C) (t : TypingTree P Γ M T)
        (e f : Environment (hw := hw) Ω C hno Γ) (hef : e.Compatible f) :
    …

    Mentions: OAI.PureTypeSystem.Expr, OAI.PureTypeSystem.IsComponent, OAI.PureTypeSystem.PrimaryEdge, OAI.PureTypeSystem.TypingTree, OAI.PureTypeSystem.ObservationValues.Environment