OAI/ModelTheory/Categoricity/Main.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

A CH obstruction to a prescribed categoricity threshold

Under CH, a countable relational language admits an abstract elementary class with least Löwenheim–Skolem number aleph0, two nonisomorphic models of size beth (omega 2) = hanf aleph0, and categoricity, including existence, at every cardinal at least tailThreshold. Distinct base cardinalities separate the endpoint models, while finite-support row and column translations establish the included categoricity tail.

  1. abbrev OAI.CHObstruction.Arrays.Existence.RationalBase line 32
  2. instance OAI.CHObstruction.Arrays.Existence.(instance at line 34) line 34
  3. instance OAI.CHObstruction.Arrays.Existence.(instance at line 39) line 39
  4. instance OAI.CHObstruction.Arrays.Existence.(instance at line 44) line 44
  5. def OAI.CHObstruction.Arrays.Existence.countableData line 49
  6. theorem OAI.CHObstruction.Arrays.Existence.countableData_object line 63
  7. theorem OAI.CHObstruction.Arrays.Existence.countableData_index line 68
  8. theorem OAI.CHObstruction.Arrays.Existence.countableData_cardinal line 73
  9. theorem OAI.CHObstruction.Arrays.Existence.models line 79
  10. theorem OAI.CHObstruction.Arrays.Categoricity.aleph_one_lt line 89
  11. theorem OAI.CHObstruction.Arrays.Categoricity.index_eq line 92
  12. theorem OAI.CHObstruction.Arrays.Categoricity.countable line 103
  13. theorem OAI.CHObstruction.Arrays.Categoricity.tail line 110
  14. abbrev OAI.CHObstruction.Arrays.EndpointModels.Base line 132
  15. instance OAI.CHObstruction.Arrays.EndpointModels.tag_nonempty line 134
  16. theorem OAI.CHObstruction.Arrays.EndpointModels.tag_initial_countable line 136
  17. theorem OAI.CHObstruction.Arrays.EndpointModels.locallyCountable line 148
  18. theorem OAI.CHObstruction.Arrays.EndpointModels.base_cardinal line 160
  19. def OAI.CHObstruction.Arrays.EndpointModels.baseEquiv line 164
  20. theorem OAI.CHObstruction.Arrays.EndpointModels.endpoint_infinite line 167
  21. theorem OAI.CHObstruction.Arrays.EndpointModels.base_le_endpoint line 169
  22. def OAI.CHObstruction.Arrays.EndpointModels.data line 175
  23. theorem OAI.CHObstruction.Arrays.EndpointModels.data_colors line 190
  24. theorem OAI.CHObstruction.Arrays.EndpointModels.object line 195
  25. theorem OAI.CHObstruction.Arrays.EndpointModels.cardinal line 203
  26. theorem OAI.CHObstruction.Arrays.EndpointModels.twoModels line 209
  27. theorem OAI.CHObstruction.main line 233

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: OAI.CHObstruction.CH, Exists, Nat, And, Countable, Sigma, OAI.CHObstruction.ClassData, OAI.CHObstruction.ClassData.IsAEC, OAI.CHObstruction.ClassData.HasLSNumber, Cardinal.aleph0, Eq, Cardinal, OAI.CHObstruction.endpoint, OAI.CHObstruction.hanf, OAI.CHObstruction.ClassData.TwoModels, LE.le, OAI.CHObstruction.tailThreshold, OAI.CHObstruction.ClassData.Categorical

    Proof uses: Exists.intro, OAI.CHObstruction.Arrays.Language, And.intro, OAI.CHObstruction.Arrays.classData, OAI.CHObstruction.Arrays.AEC.isAEC, OAI.CHObstruction.Arrays.AEC.hasLSNumber, OAI.CHObstruction.ThresholdArithmetic.endpoint_eq_hanf, OAI.CHObstruction.Arrays.EndpointModels.twoModels, OAI.CHObstruction.Arrays.Categoricity.tail

    3 instances, coercions and auxiliary constants left out.

    Distinct definitions of this name: ComparatorChallenges/CHObstruction.lean:96 (same statement text; different proof or body). Qualify references as OAI.CHObstruction.main@path.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  28. theorem OAI.CHObstruction.endpoint_lt_tailThreshold line 242
  29. theorem OAI.CHObstruction.prescribed_transfer_fails line 253