DiagramPlacements.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

ProbePlacement

theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permutation_over_root line 18
Source documentation
A pointwise isomorphism of small whole diagrams extends to a ground permutation, fixing any subdiagram at the same position in both.
```
theorem permutation_over_root (hsize : Cardinal.mk M < Cardinal.mk I)
    (s t p : Diagram M I) (b : M) (hs : s.sub b = p) (ht : t.sub b = p) :
    ∃ π : Equiv.Perm I, s.permute π = t ∧ ∀ j ∈ p.range, π j = j := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.range_inter_sub line 39
Source documentation
Exact intersections of right cones are exactly the corresponding intersections of ranges inside any fixed injective diagram.
```
theorem range_inter_sub (r : Diagram M I) (a b c : M)
    (h : ∀ z, a ∣ z ∧ b ∣ z ↔ c ∣ z) :
    (r.sub a).range ∩ (r.sub b).range = (r.sub c).range := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram, OAI.PartitionConsistency.DiagramForcing.Diagram.range
def OAI.PartitionConsistency.ProductForcing.RootProbes line 64
Source documentation
The part of probe saturation used for simultaneous ordinal choice. This is a purely algebraic statement about the actual monoid, and will be instantiated by its executed saturation, not assumed at the endpoint.
```
def RootProbes (e : M) (K : Type u) : Prop :=
…
```
theorem OAI.PartitionConsistency.ProductForcing.transported_name_supported line 73
Source documentation
A supporting diagram also supports all names obtained by a pointwise change of coordinates onto that diagram.
```
theorem transported_name_supported
    (s t : Diagram M I) (π : Equiv.Perm I) (hπ : s.permute π = t)
    (τ : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.witness_placement line 85
Source documentation
Place an arbitrary-rank witness inside the previously chosen q. Only the existing Cohen condition is strengthened. Uncountably many probes are used to choose a copy whose nonroot support misses that condition.
```
theorem witness_placement [Uncountable K]
    (hsize : Cardinal.mk M < Cardinal.mk I) (e : M) (hprobes : RootProbes e K)
    {n} (φ : Formula (n+1)) (v : Fin n → (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.RootProbes, OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.localized_existential line 156
Source documentation
Existential witnesses, at any name rank, can all be localized onto the one diagram q chosen before the formula's quantified value. The density here is in the Cohen coordinate alone.
```
theorem localized_existential [Infinite M] [Infinite I] [Uncountable K]
    (hcard : Cardinal.mk M = μ) (hsize : Cardinal.mk M < Cardinal.mk I)
    (hmerger : HasFiniteMergers M) (e : M)
    (he : Cardinal.mk ((Set.range (fun x : M => e * x))ᶜ : Set M) = Cardinal.mk M)
    (hprobes : RootProbes e K)
    {n} (φ : Formula (n+1)) (v : Fin n → (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.RootProbes, OAI.PartitionConsistency.Formula, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.SmallPlacements.extend_permutation_off line 226
Source documentation
Extend a prescribed small partial placement to a permutation while putting every unused coordinate of the larger small set outside a forbidden small set. The prescribed part is left unchanged.
```
theorem extend_permutation_off (hμ : aleph0 ≤ μ) (hsize : μ < #I)
    {s v K : Set I} (hs : #s ≤ μ) (hv : #v ≤ μ) (hK : #K ≤ μ)
    (f : s ↪ I) :
    ∃ π : Equiv.Perm I, (∀ x : s, π x = f x) ∧ Disjoint (π '' (v \ s)) K := by
…
```

theorem OAI.PartitionConsistency.SmallPlacements.paste_placements line 250

Source documentation

Two pointwise placements on independent sets can be pasted whenever both source and target intersections are the fixed root.

theorem paste_placements {s₀ s₁ p : Set I} (hinter : s₀ ∩ s₁ = p)
    (α β : Equiv.Perm I) (hα : ∀ j ∈ p, α j = j) (hβ : ∀ j ∈ p, β j = j)
    (himage : (α '' s₀) ∩ (β '' s₁) = p) :
    ∃ f : (s₀ ∪ s₁ : Set I) ↪ I,
      (∀ j (hj : j ∈ s₀), f ⟨j,Or.inl hj⟩ = α j) ∧
      (∀ j (hj : j ∈ s₁), f ⟨j,Or.inr hj⟩ = β j) := by
…

theorem OAI.PartitionConsistency.SmallPlacements.extend_two_placements line 286

Source documentation

Place the rest of a diagram after both of its independent subdiagrams have been placed, with all leftover coordinates fresh.

theorem extend_two_placements (hμ : aleph0 ≤ μ) (hsize : μ < #I)
    {s₀ s₁ p v K : Set I} (hs₀ : #s₀ ≤ μ) (hs₁ : #s₁ ≤ μ) (hv : #v ≤ μ) (hK : #K ≤ μ)
    (hinter : s₀ ∩ s₁ = p) (α β : Equiv.Perm I)
    (hα : ∀ j ∈ p, α j = j) (hβ : ∀ j ∈ p, β j = j)
    (himage : (α '' s₀) ∩ (β '' s₁) = p) :
    ∃ π : Equiv.Perm I, (∀ j ∈ s₀, π j = α j) ∧ (∀ j ∈ s₁, π j = β j) ∧
      Disjoint (π '' (v \ (s₀ ∪ s₁))) K := by
…

theorem OAI.PartitionConsistency.SmallPlacements.image_inter_of_fresh line 301

Source documentation

Compute an overlap when every coordinate not already prescribed was placed freshly.

theorem image_inter_of_fresh {s₀ s₁ v K : Set I} (h₀ : s₀ ⊆ v) (h₁ : s₁ ⊆ v)
    (π : Equiv.Perm I) (hfresh : Disjoint (π '' (v \ (s₀ ∪ s₁))) K) :
    (π '' v) ∩ K = ((π '' s₀) ∪ (π '' s₁)) ∩ K := by
…

theorem OAI.PartitionConsistency.SmallPlacements.inter_eq_of_between line 317
Source documentation
If an overlap with a larger forbidden set is exact, then so is its overlap with any intermediate set containing the indicated root.
```
theorem inter_eq_of_between {A K t r : Set I} (h : A ∩ K = r)
    (hrt : r ⊆ t) (htK : t ⊆ K) : A ∩ t = r := by
…
```

theorem OAI.PartitionConsistency.SmallPlacements.three_copy_placement line 329

Source documentation

The simultaneous three-copy placement needed in support descent. The two prescribed copies of s₀ may be compared through one fresh shared copy of s₁. All extra coordinates avoid the entire forbidden set, not merely the ranges of the diagrams.

theorem three_copy_placement (hμ : aleph0 ≤ μ) (hsize : μ < #I)
    {s₀ s₁ p v K : Set I} (h₀ : s₀ ⊆ v) (h₁ : s₁ ⊆ v)
    (hv : #v ≤ μ) (hK : #K ≤ μ) (hinter : s₀ ∩ s₁ = p)
    (α β : Equiv.Perm I) (hα : ∀ j ∈ p, α j = j) (hβ : ∀ j ∈ p, β j = j)
    (hind : (α '' s₀) ∩ (β '' s₀) = p)
    (hαK : α '' s₀ ⊆ K) (hβK : β '' s₀ ⊆ K) :
    ∃ π ρ : Equiv.Perm I,
      (∀ j ∈ s₀, π j = α j) ∧ (∀ j ∈ s₀, ρ j = β j) ∧
      (∀ j ∈ s₁, π j = ρ j) ∧
      (π '' v) ∩ K = α '' s₀ ∧ (ρ '' v) ∩ K = β '' s₀ ∧
      (π '' v) ∩ (ρ '' v) = π '' s₁ := by
…

theorem OAI.PartitionConsistency.CohenForcing.Condition.permute_eq_of_agree line 400
Source documentation
Moving a condition only depends on the permutation on its support.
```
theorem permute_eq_of_agree (d : Condition I κ) (α β : Equiv.Perm I)
    (h : ∀ j ∈ d.support, α j = β j) : d.permute α = d.permute β := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.compatible_permute_of_trigger line 410
Source documentation
Compatibility with a moved condition only uses its already prescribed part when all shared coordinates are in that part.
```
theorem compatible_permute_of_trigger (d c : Condition I κ) (π : Equiv.Perm I)
    {s v : Set I} (hd : d.support ⊆ v)
    (hov : (π '' v) ∩ c.support ⊆ π '' s) (hc : c ≤ (d.restrict s).permute π) :
    Compatible c (d.permute π) := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.permute, OAI.PartitionConsistency.CohenForcing.Condition.Compatible
theorem OAI.PartitionConsistency.CohenForcing.Condition.compatible_permutes_of_overlap line 426
Source documentation
Two moved copies agree on their overlap when their placements agree pointwise there, even if their supports outside it are arbitrary.
```
theorem compatible_permutes_of_overlap (d : Condition I κ) (π ρ : Equiv.Perm I)
    {s v : Set I} (hd : d.support ⊆ v)
    (hov : (π '' v) ∩ (ρ '' v) ⊆ π '' s) (hs : ∀ j ∈ s, π j = ρ j) :
    Compatible (d.permute π) (d.permute ρ) := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.Compatible
theorem OAI.PartitionConsistency.CohenForcing.Condition.Compatible.union_left line 443
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.permute_eq_of_agree line 459
Source documentation
Pointwise agreement on a diagram's range is literal agreement of the moved diagrams, so transports of all its supported names agree as well.
```
theorem permute_eq_of_agree (s : Diagram M I) (π ρ : Equiv.Perm I)
    (h : ∀ j ∈ s.range, π j = ρ j) : s.permute π = s.permute ρ := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.ExactOverlap.of_common line 464
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.common_extension_three line 470

theorem OAI.PartitionConsistency.ProductForcing.descent_comparison_placement line 491

Source documentation

The three-copy compatibility step of support descent, including the Cohen coordinate and an arbitrary potential counterexample condition.

theorem descent_comparison_placement [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (p s₀ s₁ v : Diagram M I) (hinter : s₀.range ∩ s₁.range = p.range)
    (hv₀ : v ≤ s₀) (hv₁ : v ≤ s₁)
    (α β : Equiv.Perm I) (hα : ∀ j ∈ p.range, α j = j) (hβ : ∀ j ∈ p.range, β j = j)
    (hind : (s₀.permute α).range ∩ (s₀.permute β).range = p.range)
    (d c : CohenForcing.Condition I κ) (hd : d.support ⊆ v.range) (t : Diagram M I)
    (htα : t ≤ s₀.permute α) (htβ : t ≤ s₀.permute β)
    (hcα : c ≤ (d.restrict s₀.range).permute α) (hcβ : c ≤ (d.restrict s₀.range).permute β) :
    ∃ π ρ : Equiv.Perm I, s₀.permute π = s₀.permute α ∧
      s₀.permute ρ = s₀.permute β ∧ s₁.permute π = s₁.permute ρ ∧
      ∃ q : Condition M I κ, q ≤ (c,t) ∧ q ≤ permute π (d,v) ∧ q ≤ permute ρ (d,v) := by
…

Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.permute, OAI.PartitionConsistency.ProductForcing.Condition