AtomicForcing.lean`

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.PartitionConsistency.SetForcingNames.Child.rank_lt line 10
Source documentation
An edge of a literal name decreases the rank of its name component.
```
theorem Child.rank_lt {τ σ : ZFSet.{u}} (h : Child τ σ) : τ.rank < σ.rank := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.Child
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.pairRanks line 20
Source documentation
The rank multiset, rather than a lexicographic ordering, permits the swaps in the recursive clauses of atomic forcing.
```
noncomputable def pairRanks (σ τ : ZFSet.{u}) : Multiset Ordinal.{u} := {σ.rank} + {τ.rank}
```
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.PairLower line 22
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.pairLower_wf line 25
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.rank_replace line 28
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.pairLower_right line 33
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.pairLower_left line 36
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.pairLower_swap line 40
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.relations line 49
Source documentation
Ordinary atomic set forcing, on actual sets of Kuratowski pairs. The first component is membership and the second is equality. No truth values or atomic laws are supplied as parameters.
```
noncomputable def relations : ZFSet.{u} × ZFSet.{u} → (P → Prop) × (P → Prop) :=
…
```
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.MemAt line 60
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.EqAt line 61
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.mem_iff line 65
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.eq_iff line 74
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.mem_mono line 81
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.eq_mono line 85
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.eq_symm line 91
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.mem_of_dense line 95
Source documentation
Atomic membership is unchanged by closing densely below a condition.
```
theorem mem_of_dense {p : P} {σ τ : ZFSet.{u}}
    (h : ∀ q, q ≤ p → ∃ r, r ≤ q ∧ MemAt code r σ τ) : MemAt code p σ τ := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.AtomicForcing.MemAt
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.eq_of_dense line 104
Source documentation
Atomic equality also has the dense-closure property.
```
theorem eq_of_dense {p : P} {σ τ : ZFSet.{u}}
    (h : ∀ q, q ≤ p → ∃ r, r ≤ q ∧ EqAt code r σ τ) : EqAt code p σ τ := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.AtomicForcing.EqAt
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.mem_of_edge_eq line 117
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.eq_refl line 124
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.tripleRanks line 134
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.TripleLower line 137
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.tripleLower_wf line 141
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.atomic_laws line 148
Source documentation
All three substitution rules are proved together. The induction measure is invariant under permutations, while replacing a name by a child decreases it. In particular transitivity is a consequence, not an assumed atomic law.
```
theorem atomic_laws (a b c : ZFSet.{u}) :
    (∀ p : P, EqAt code p a b → EqAt code p b c → EqAt code p a c) ∧
    (∀ p : P, EqAt code p a b → MemAt code p a c → MemAt code p b c) ∧
    (∀ p : P, EqAt code p b c → MemAt code p a b → MemAt code p a c) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.AtomicForcing.EqAt, OAI.PartitionConsistency.SetForcingNames.AtomicForcing.MemAt
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.eq_trans line 194
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.mem_congr_left line 197
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.mem_congr_right line 201
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.data line 207
Source documentation
The constructed atomic forcing relations instantiate the external quotient machinery on any specified set of name codes.
```
noncomputable def data (code : P → ZFSet.{u}) (N : Set ZFSet.{u}) : ForcingQuotient.AtomicData P N where
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.AtomicData
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.exists_no_mem line 228
Source documentation
Failure of membership has a strengthening that forces its negation.
```
theorem exists_no_mem {p : P} {σ τ : ZFSet.{u}} (h : ¬ MemAt code p σ τ) :
    ∃ q, q ≤ p ∧ ∀ r, r ≤ q → ¬ MemAt code r σ τ := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.AtomicForcing.MemAt
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.memberDecisions line 236
Source documentation
Conditions which either contain an atomic membership witness or exclude membership at every strengthening.
```
def memberDecisions (code : P → ZFSet.{u}) (σ τ : ZFSet.{u}) : Set P :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.memberDecisions_dense line 240
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.Apart line 252
Source documentation
A named member of σ which a condition forces not to belong to τ. This is a concrete witness to inequality, not a postulated decision law.
```
def Apart (code : P → ZFSet.{u}) (p : P) (σ τ : ZFSet.{u}) : Prop :=
…
```
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.equalityDecisions line 256
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.equalityDecisions_dense line 259
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.activeCodes line 280
Source documentation
The set of active literal condition codes.
```
def activeCodes (code : P → ZFSet.{u}) (G : GenericFilter P) : Set ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.mem_evaluate_active_iff line 283
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.EdgeClosed line 296
Source documentation
A collection of literal names is hereditary for edges using conditions in P. Countability and this property impose no bound on name-rank.
```
def EdgeClosed (code : P → ZFSet.{u}) (N : Set ZFSet.{u}) : Prop :=
…
```
def OAI.PartitionConsistency.SetForcingNames.AtomicForcing.IsAtomicGeneric line 301
Source documentation
Precisely the two families of dense sets needed for the atomic truth lemma. Their existence and density were proved above.
```
def IsAtomicGeneric (code : P → ZFSet.{u}) (N : Set ZFSet.{u})
    (G : GenericFilter P) : Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.atomic_truth line 310
Source documentation
The ordinary atomic truth lemma is proved by recursion on the literal names. This supplies the link between the atomic quotient and actual set interpretation in the transitive-ground route.
```
theorem atomic_truth {N : Set ZFSet.{u}} (hN : EdgeClosed code N)
    (G : GenericFilter P) (hG : IsAtomicGeneric code N G)
    {σ τ : ZFSet.{u}} (hσ : σ ∈ N) (hτ : τ ∈ N) :
    ((∃ p, p ∈ G ∧ MemAt code p σ τ) ↔
       evaluate (activeCodes code G) σ ∈ evaluate (activeCodes code G) τ) ∧
    ((∃ p, p ∈ G ∧ EqAt code p σ τ) ↔
       evaluate (activeCodes code G) σ = evaluate (activeCodes code G) τ) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.AtomicForcing.EdgeClosed, OAI.PartitionConsistency.SetForcingNames.AtomicForcing.IsAtomicGeneric, OAI.PartitionConsistency.SetForcingNames.AtomicForcing.MemAt, OAI.PartitionConsistency.SetForcingNames.evaluate, OAI.PartitionConsistency.SetForcingNames.AtomicForcing.activeCodes, OAI.PartitionConsistency.SetForcingNames.AtomicForcing.EqAt
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.exists_truth_generic line 379
Source documentation
Construct an external filter meeting both the actual atomic requirements and every standard-formula request on a countable collection of names. The additional dense sets may, for example, include every coded ground dense set. No assertion that target-theory axioms are forced is used here.
```
theorem exists_truth_generic (code : P → ZFSet.{u}) {N : Set ZFSet.{u}} (hc : N.Countable)
    {I : Type w} [Countable I] (D : I → Set P) (hD : ∀ i, Dense (D i)) (p : P) :
    ∃ G : GenericFilter P, p ∈ G ∧ (∀ i, ∃ q, q ∈ G ∧ q ∈ D i) ∧
      (data code N).IsGeneric G ∧ IsAtomicGeneric code N G := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.AtomicForcing.data, OAI.PartitionConsistency.SetForcingNames.AtomicForcing.IsAtomicGeneric
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.edge_map_orderIso line 409
Source documentation
The literal action transforms exactly the edges, including their condition codes. Injectivity prevents an edge using a different code from entering this fiber.
```
theorem edge_map_orderIso {f : ZFSet.{u} → ZFSet.{u}} (hf : Function.Injective f)
    (e : P ≃o P) (hcode : ∀ p, f (code p) = code (e p))
    {σ ν : ZFSet.{u}} {r : P} :
    ZFSet.pair ν (code (e r)) ∈ mapConditions f σ ↔
      ∃ ρ, ZFSet.pair ρ (code r) ∈ σ ∧ mapConditions f ρ = ν := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.mapConditions
theorem OAI.PartitionConsistency.SetForcingNames.AtomicForcing.atomic_symmetry line 425
Source documentation
Atomic symmetry on literal names. Conditions are moved together with the names; this makes no assertion that a generic filter is fixed by the action.
```
theorem atomic_symmetry {f : ZFSet.{u} → ZFSet.{u}} (hf : Function.Injective f)
    (e : P ≃o P) (hcode : ∀ p, f (code p) = code (e p)) (σ τ : ZFSet.{u}) :
    (∀ p, MemAt code p σ τ ↔
      MemAt code (e p) (mapConditions f σ) (mapConditions f τ)) ∧
    (∀ p, EqAt code p σ τ ↔
      EqAt code (e p) (mapConditions f σ) (mapConditions f τ)) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.AtomicForcing.MemAt, OAI.PartitionConsistency.SetForcingNames.mapConditions, OAI.PartitionConsistency.SetForcingNames.AtomicForcing.EqAt