Update docs for BaseType

Signed-off-by: zeramorphic <[email protected]>

ConNF/BaseType/NearLitter.lean

@@ -11,7 +11,6 @@ In this file, we define near-litters, which are sets with small symmetric differ
 * `ConNF.IsNearLitter`: Proposition stating that a set is near a given litter.
 * `ConNF.NearLitter`: The type of near-litters.
 * `ConNF.Litter.toNearLitter`: Converts a litter to its corresponding near-litter.
-* `ConNF.localCardinal`: The set of near-litters to a given litter.
 * `ConNF.NearLitter.IsLitter`: Proposition stating that a near-litter comes directly from a litter:
     it is of the form `L.toNearLitter` for some litter `L`.
 -/
@@ -181,32 +180,9 @@ theorem mk_nearLitter : #NearLitter = #μ := by
     le_rfl
     Params.μ_isStrongLimit.ne_zero
 
-/-- The *local cardinal* of a litter is the set of all near-litters to that litter. -/
-def localCardinal (L : Litter) : Set NearLitter :=
-  {N : NearLitter | N.1 = L}
-
-@[simp]
-theorem mem_localCardinal {L : Litter} {N : NearLitter} : N ∈ localCardinal L ↔ N.1 = L :=
-  Iff.rfl
-
-theorem localCardinal_nonempty (L : Litter) : (localCardinal L).Nonempty :=
-  ⟨⟨L, litterSet _, isNearLitter_litterSet _⟩, rfl⟩
-
-theorem localCardinal_disjoint : Pairwise (Disjoint on localCardinal) :=
-  fun _ _ h => disjoint_left.2 fun _ h₁ h₂ => h <| h₁.symm.trans h₂
-
-theorem localCardinal_injective : Injective localCardinal := by
-  intro L₁ L₂ h₁₂
-  by_contra h
-  have := (localCardinal_disjoint h).inter_eq
-  rw [h₁₂, inter_self] at this
-  exact (localCardinal_nonempty _).ne_empty this
-
-theorem Litter.toNearLitter_mem_localCardinal (L : Litter) : L.toNearLitter ∈ localCardinal L :=
-  rfl
-
+/-- There aer `μ` near-litters to a given litter. -/
 @[simp]
-theorem mk_localCardinal (L : Litter) : #(localCardinal L) = #μ := by
+theorem mk_nearLitter_to (L : Litter) : #{N : NearLitter | N.1 = L} = #μ := by
   refine Eq.trans (Cardinal.eq.2 ⟨⟨?_, fun x => ⟨⟨L, x⟩, rfl⟩, ?_, ?_⟩⟩) (mk_nearLitter' L)
   · rintro ⟨x, rfl : x.1 = L⟩
     exact x.snd
@@ -226,6 +202,7 @@ theorem NearLitter.IsLitter.litterSet_eq {N : NearLitter} (h : N.IsLitter) :
     litterSet N.fst = N.snd :=
   by cases h; rfl
 
+/-- The main induction rule for near-litters that are litters. -/
 theorem NearLitter.IsLitter.exists_litter_eq {N : NearLitter} (h : N.IsLitter) :
     ∃ L : Litter, N = L.toNearLitter :=
   by obtain ⟨L⟩ := h; exact ⟨L, rfl⟩
@@ -266,6 +243,7 @@ theorem symmDiff_union_inter {α : Type _} {a b : Set α} : (a ∆ b) ∪ (a ∩
   simp only [mem_union, mem_symmDiff, mem_inter_iff]
   tauto
 
+/-- Near-litters to the same litter have `κ`-sized intersection. -/
 theorem NearLitter.mk_inter_of_fst_eq_fst {N₁ N₂ : NearLitter} (h : N₁.fst = N₂.fst) :
     #(N₁ ∩ N₂ : Set Atom) = #κ := by
   rw [← isNear_iff_fst_eq_fst] at h
@@ -281,6 +259,7 @@ theorem NearLitter.inter_nonempty_of_fst_eq_fst {N₁ N₂ : NearLitter} (h : N
   rw [← nonempty_coe_sort, ← mk_ne_zero_iff, mk_inter_of_fst_eq_fst h]
   exact mk_ne_zero κ
 
+/-- Near-litters to different litters have small intersection. -/
 theorem NearLitter.inter_small_of_fst_ne_fst {N₁ N₂ : NearLitter} (h : N₁.fst ≠ N₂.fst) :
     Small (N₁ ∩ N₂ : Set Atom) := by
   have := N₁.2.2

ConNF/BaseType/NearLitterPerm.lean

@@ -30,9 +30,8 @@ variable [Params.{u}] {L : Litter}
 
 /--
 A near-litter permutation is a permutation of atoms which sends near-litters to near-litters.
-It turns out that the images of near-litters near the same litter are themselves near
-the same litter. Hence a near-litter permutation induces a permutation of litters, and we keep that
-as data for simplicity.
+Then, the images of near-litters near the same litter must be near the same litter. Hence a
+near-litter permutation induces a permutation of litters, and we keep that as data for simplicity.
 
 This is sometimes called a -1-allowable permutation.
 The proposition `near` can be interpreted as saying that if `s` is an `L`-near-litter, then its
@@ -237,12 +236,6 @@ theorem smul_nearLitter_snd (π : NearLitterPerm) (N : NearLitter) :
     ((π • N).2 : Set Atom) = π • (N.2 : Set Atom) :=
   smul_nearLitter_coe π N
 
-@[simp]
-theorem smul_localCardinal (π : NearLitterPerm) (L : Litter) :
-    π • localCardinal L = localCardinal (π • L) := by
-  ext N
-  simp [mem_smul_set, ← eq_inv_smul_iff]
-
 @[simp]
 theorem NearLitter.mem_snd_iff (N : NearLitter) (a : Atom) : a ∈ (N.snd : Set Atom) ↔ a ∈ N :=
   Iff.rfl

ConNF/BaseType/Params.lean

@@ -26,7 +26,7 @@ used for lambda abstractions.
 
 Ordinals and cardinals are represented here as arbitrary types (not sets) with certain properties.
 For instance, `Λ` is an arbitrary type that has an ordering `<`, which is assumed to be a
-well-ordering (the `Λwo` term is a proof of this fact).
+well-ordering (the `Λ_isWellOrder` term is a proof of this fact).
 
 The prefix `#` denotes the cardinality of a type.
 -/
@@ -46,9 +46,8 @@ class Params where
   Λ_isLimit : (Ordinal.type ((· < ·) : Λ → Λ → Prop)).IsLimit
   /--
   The type indexing the atoms in each litter.
-  Its cardinality is regular, and is larger than `Λ` but smaller than `κ`.
-  It also has an additive monoid structure, which is covariant in both variables with respect to the
-  ordering.
+  It is well-ordered, has regular cardinality, and is larger than `Λ` but smaller than `κ`.
+  It also has an additive monoid structure induced by its well-ordering.
   -/
   κ : Type u
   [κ_linearOrder : LinearOrder κ]
@@ -80,12 +79,14 @@ class Params where
 export Params (Λ κ μ)
 
 /-!
-### Explicit parameters
+## Explicit parameters
 
 There exist valid parameters for the model. The smallest such parameters are
 * `Λ := ℵ_0`
 * `κ := ℵ_1`
 * `μ = ℶ_{ω_1}`.
+
+We begin by creating a few instances that allow us to use cardinals to satisfy the model parameters.
 -/
 
 theorem noMaxOrder_of_ordinal_type_eq {α : Type u} [Preorder α] [Infinite α] [IsWellOrder α (· < ·)]
@@ -209,6 +210,8 @@ noncomputable def sub_of_isWellOrder {α : Type _}
     (Ordinal.typein (· < ·) x - Ordinal.typein (· < ·) y)
       ((Ordinal.sub_le_self _ _).trans_lt (Ordinal.typein_lt_type _ _))
 
+/-- The smallest set of valid parameters for the model.
+They are instantiated in Lean's minimal universe `0`. -/
 noncomputable def minimalParams : Params.{0} where
   Λ := ℕ
   Λ_zero_le := zero_le
@@ -249,7 +252,7 @@ noncomputable def minimalParams : Params.{0} where
 
 variable [Params.{u}] {ι α β : Type u}
 
-/-! The types `Λ`, `κ`, `μ` are inhabited and infinite. -/
+/-! Here, we unpack the hypotheses on `Λ`, `κ`, `μ` into instances that Lean can see. -/
 
 theorem aleph0_le_mk_Λ : ℵ₀ ≤ #Λ := by
   have := Ordinal.card_le_card (Ordinal.omega_le_of_isLimit Params.Λ_isLimit)
@@ -288,6 +291,10 @@ instance : NoMaxOrder μ := by
   rw [← Params.μ_ord] at this
   exact noMaxOrder_of_ordinal_type_eq this
 
+/-!
+## The ordered structure on `κ`
+-/
+
 def κ_ofNat : ℕ → κ
   | 0 => 0
   | n + 1 => Order.succ (κ_ofNat n)
@@ -398,6 +405,10 @@ theorem κ_lt_sub_iff {i j k : κ} : k < i - j ↔ j + k < i := by
   rw [← Ordinal.typein_lt_typein (α := κ) (· < ·), ← Ordinal.typein_lt_typein (α := κ) (· < ·)]
   rw [Params.κ_add_typein, Params.κ_sub_typein, Ordinal.lt_sub]
 
+/-!
+## Type indices
+-/
+
 /-- Either the base type or a proper type index (an element of `Λ`).
 The base type is written `⊥`. -/
 @[reducible]
@@ -413,15 +424,16 @@ instance : WellFoundedRelation Λ :=
 instance : WellFoundedRelation TypeIndex :=
   IsWellOrder.toHasWellFounded
 
+/-- There are exactly `Λ` type indices. -/
 @[simp]
 theorem mk_typeIndex : #TypeIndex = #Λ :=
   mk_option.trans <| add_eq_left aleph0_le_mk_Λ <| one_le_aleph0.trans aleph0_le_mk_Λ
 
-/-- Principal segments (sets of the form `{y | y < x}`) have cardinality `< μ`. -/
+/-- Sets of the form `{y | y < x}` have cardinality `< μ`. -/
 theorem card_Iio_lt (x : μ) : #(Set.Iio x) < #μ :=
   card_typein_lt (· < ·) x Params.μ_ord.symm
 
-/-- Initial segments (sets of the form `{y | y ≤ x}`) have cardinality `< μ`. -/
+/-- Sets of the form `{y | y ≤ x}` have cardinality `< μ`. -/
 theorem card_Iic_lt (x : μ) : #(Set.Iic x) < #μ := by
   rw [← Set.Iio_union_right, mk_union_of_disjoint, mk_singleton]
   -- TODO: This isn't the morally correct proof because it uses the fact `μ` is a limit cardinal.

ConNF/BaseType/Small.lean

@@ -29,6 +29,10 @@ def Small (s : Set α) : Prop :=
 theorem Small.lt : Small s → #s < #κ :=
   id
 
+/-!
+## Criteria for smallness
+-/
+
 theorem Set.Subsingleton.small {α : Type _} {s : Set α} (hs : s.Subsingleton) : Small s :=
   hs.cardinal_mk_le_one.trans_lt <| one_lt_aleph0.trans_le Params.κ_isRegular.aleph0_le
 
@@ -98,6 +102,10 @@ theorem Small.pFun_image {α β : Type _} {s : Set α} (h : Small s) {f : α →
   rintro x ⟨y, ⟨z, hz₁, hz₂⟩, rfl⟩
   exact ⟨z, hz₁, Part.eq_some_iff.mpr hz₂⟩
 
+/-!
+## Nearness
+-/
+
 /-- Two sets are near if their symmetric difference is small. -/
 def IsNear (s t : Set α) : Prop :=
   Small (s ∆ t)

ConNF/NewTangle/Cloud.lean

@@ -47,8 +47,6 @@ variable [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt] [PositionedObject
   {γ : TypeIndex} [LtLevel γ] {β : Λ} [LtLevel β]
   (hγβ : γ ≠ β)
 
--- TODO: Remove `localCardinal`
-
 /-- The cloud map. We map each tangle to all typed near-litters near the `fuzz`ed tangle, and take
 the union over all tangles in the input. -/
 def cloud (s : Set (TSet γ)) : Set (TSet β) :=
@@ -85,15 +83,15 @@ theorem cloud_nonempty (hγβ : γ ≠ β) : (cloud hγβ s).Nonempty ↔ s.None
   simp_rw [nonempty_iff_ne_empty, Ne.def, cloud_eq_empty]
 
 theorem subset_cloud (t : Tangle γ) (ht : t.set_lt ∈ s) :
-    typedNearLitter '' localCardinal (fuzz hγβ t) ⊆ cloud hγβ s := by
+    typedNearLitter '' {N | N.1 = fuzz hγβ t} ⊆ cloud hγβ s := by
   rintro _ ⟨N, hN, rfl⟩
   exact ⟨t, ht, N, hN, rfl⟩
 
 theorem μ_le_mk_cloud : s.Nonempty → #μ ≤ #(cloud hγβ s) := by
   rintro ⟨t, ht⟩
   obtain ⟨t, rfl⟩ := exists_tangle_lt t
   refine' (Cardinal.mk_le_mk_of_subset <| subset_cloud t ht).trans_eq' _
-  rw [Cardinal.mk_image_eq, mk_localCardinal]
+  rw [Cardinal.mk_image_eq, mk_nearLitter_to]
   exact typedNearLitter.inj'
 
 theorem subset_of_cloud_subset (s₁ s₂ : Set (TSet γ)) (h : cloud hγβ s₁ ⊆ cloud hγβ s₂) :

docs/index.md

@@ -9,7 +9,7 @@
 
 In 1937, Quine proposed a set theory called "New Foundations", and since 2010, Randall Holmes has claimed to have a proof of its consistency.
 In this repository, we use the interactive theorem prover Lean to verify the difficult part of his proof, thus proving that New Foundations is indeed consistent.
-The proof is now complete, and the theorem statements can be found in `ConNF/Model/Result.lean`.
+The proof is now complete, and the theorem statements can be found in `ConNF/Model/Result.lean` ([source](https://github.com/leanprover-community/con-nf/blob/main/ConNF/Model/Result.lean), [docs](https://leanprover-community.github.io/con-nf/doc/ConNF/Model/Result.html)).
 
 See [our website](https://leanprover-community.github.io/con-nf/) for more information, the [documentation of our Lean code](https://leanprover-community.github.io/con-nf/doc/), and the [deformalisation paper](https://zeramorphic.github.io/con-nf-paper/main.l.pdf) that translates the Lean definitions into English.
 
@@ -91,4 +91,3 @@ Note, however, that this choice is arbitrary, and any other finite axiomatisatio
 ## Dependency graph
 
 ![dependency graph](https://leanprover-community.github.io/con-nf/depgraph.png)
-