GraphFusion.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

IndexedGraph

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedGraph line 16
Source documentation
The canonical internal graph of a small ground-indexed name family. Uniform support is used only to prove that this actual set name is HS.
```
def indexedGraph (X : ZFSet.{u}) (f : X → S.Name) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hfix : ∀ g ∈ H, ∀ x, g • f x = f x) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedGraph_fixed line 22

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_indexedGraph line 30

Source documentation

The complete membership value of the graph.

theorem mem_indexedGraph (X : ZFSet.{u}) (f : X → S.Name) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hfix : ∀ g ∈ H, ∀ x, g • f x = f x) (ν : S.Name) (p : P) :
    S.atomic.MemF p ν (S.indexedGraph X f H hH hfix) ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ x : X,
        S.atomic.EqF r ν ((Name.check x.val).opair (f x)) := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.app_indexedGraph line 51

Source documentation

Every value asserted by the graph is one of its prescribed values, with both the input and output transported by forced equality.

theorem app_indexedGraph (X : ZFSet.{u}) (f : X → S.Name) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hfix : ∀ g ∈ H, ∀ x, g • f x = f x) (x y : S.Name) (p : P) :
    S.App p (S.indexedGraph X f H hH hfix) x y ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ i : X,
        S.atomic.EqF r x (Name.check i.val) ∧ S.atomic.EqF r y (f i) := by
…

Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedGraph_app_at line 59
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.indexedGraph_functionOn line 67
Source documentation
The ground-indexed name-family graph satisfies the unmodified internal set-function formula. This includes the assertion that it has no junk entries.
```
theorem indexedGraph_functionOn (X : ZFSet.{u}) (f : X → S.Name) (H : Subgroup Γ) (hH : H ∈ S.filter)
    (hfix : ∀ g ∈ H, ∀ x, g • f x = f x) (p : P) :
    S.Forces ![S.indexedGraph X f H hH hfix,Name.check X] p (SetLanguage.functionOn 0 1) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.functionOn
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.check_unorderedPair line 110
Source documentation
Check names commute, up to forced equality, with unordered pairs.
```
theorem check_unorderedPair (x y : ZFSet.{u}) (p : P) :
    S.atomic.EqF p (Name.check {x,y}) ((Name.check x).pair (Name.check y)) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.check_opair line 127
Source documentation
ZFSet.pair is the actual Kuratowski pair.
```
theorem check_opair (x y : ZFSet.{u}) (p : P) :
    S.atomic.EqF p (Name.check (ZFSet.pair x y)) ((Name.check x).opair (Name.check y)) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.groundGraph line 138
Source documentation
A ground function is represented by a literal set of ordered pairs.
```
def groundGraph (X : ZFSet.{u}) (g : X → ZFSet.{u}) : ZFSet.{u} :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_groundGraph line 141
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_check_groundGraph line 145
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.check_groundGraph_app line 160

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.functionOn_entries line 167

Source documentation

Membership in an internal function graph can only come from its actual ordered pairs, whose first coordinates lie in its domain.

theorem functionOn_entries {n} (v : Fin n → S.Name) (p : P) (f d : Fin n)
    (hf : S.Forces v p (SetLanguage.functionOn f d))
    (ν : S.Name) {q : P} (hqp : q ≤ p) (hν : S.atomic.MemF q ν (v f)) :
    ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ x y : S.Name,
      S.atomic.MemF s x (v d) ∧ S.atomic.EqF s ν (x.opair y) := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.functionOn

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.functionOn_eq_check_groundGraph line 184
Source documentation
A forced function on a ground domain with all values prescribed by one ground function is equal to the check name of that function's set graph.
```
theorem functionOn_eq_check_groundGraph (X : ZFSet.{u}) (g : X → ZFSet.{u})
    (f : S.Name) (p : P)
    (hf : S.Forces ![f,Name.check X] p (SetLanguage.functionOn 0 1))
    (hg : ∀ i : X, S.App p f (Name.check i.val) (Name.check (g i))) :
    S.atomic.EqF p f (Name.check (groundGraph X g)) := by
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.functionOn, OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.groundGraph
theorem OAI.PartitionConsistency.CohenForcing.Condition.countable_fusion line 235
Source documentation
Every countable family of downward-persistent dense requirements below a Cohen condition can be met by one condition, by actual countable closure.
```
theorem countable_fusion {A : Type v} [Countable A]
    (d : Condition I κ) (R : A → Condition I κ → Prop)
    (hmono : ∀ i q r, r ≤ q → R i q → R i r)
    (hdense : ∀ i q, q ≤ d → ∃ r, r ≤ q ∧ R i r) :
    ∃ r, r ≤ d ∧ ∀ i, R i r := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.ProductForcing.mapsTo_value_at_root line 274
Source documentation
Each ground input of an internal ground-codomain map can be decided without changing its supporting root; only the Cohen coordinate is changed.
```
theorem mapsTo_value_at_root [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (X Y : ZFSet.{u}) (f : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.countable_ground_map_at_root line 315
Source documentation
Countably many prescribed ground inputs of a root-supported function can all be decided by a single extension. In particular no countable ground sequence is added by the symmetric product system.
```
theorem countable_ground_map_at_root [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (X Y : ZFSet.{u}) [Countable X]
    (f : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.countable_ground_map_dense line 351
Source documentation
Dense ground-map decision for an arbitrary starting condition. The support of the map and the coordinates of the condition are absorbed by one actual extension of the diagram; closure is used only in the Cohen coordinate after making that extension.
```
theorem countable_ground_map_dense [Infinite M] [Infinite I]
    (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)
    (X Y : ZFSet.{u}) [Countable X]
    (f : (system (M := M) (I := I) (κ := κ) hμ).Name) (t : Poset M I κ)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ConcreteSystem.countable_ground_map_dense line 390
Source documentation
The concrete ground-independent system adds no maps from a countable ground set to a ground set: every such forced map is densely a ground graph. This does not assert the as-yet-unproved Partition Principle.
```
theorem countable_ground_map_dense (X Y : ZFSet) [Countable X]
    (f : S.Name) (t : P)
    (hf : S.Forces ![f,Name.check X,Name.check Y] t (SetLanguage.mapsTo 0 1 2)) :
    ∃ s, s ≤ t ∧ ∃ g : X → Y,
      S.atomic.EqF s f (Name.check (groundGraph X (fun i => (g i).val))) :=
…
```
Mentions: OAI.PartitionConsistency.ConcreteSystem.P, OAI.PartitionConsistency.SetLanguage.mapsTo
theorem OAI.PartitionConsistency.DiagramOrder.HeightCost.dense_stable_ideal line 420
Source documentation
A monotone system of directed bounded ideals in a height-and-cost order is locally constant on a dense set in any countably closed forcing. The heights of possible future elements are approximated during a descending construction. Positive costs exclude every still-missing element at its countable lower bound.
```
theorem dense_stable_ideal (hclosed : ∀ f : ℕ → P, Antitone f → ∃ p, ∀ n, p ≤ f n)
    (hj : HasConditionalJoins α) {a : α} (U : P → ConeIdeal a)
    (hmono : ∀ {p q : P}, q ≤ p → (U p).carrier ⊆ (U q).carrier) (p : P) :
    ∃ q, q ≤ p ∧ ∀ r, r ≤ q → U r = U q := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.ConeIdeal
def OAI.PartitionConsistency.ForcingQuotient.principalFilter line 471
Source documentation
The directed filter generated by one condition; it is NOT called generic and no meeting property is attributed to it.
```
def principalFilter (p : P) : GenericFilter P where
…
```
Mentions: OAI.PartitionConsistency.ForcingQuotient.GenericFilter
theorem OAI.PartitionConsistency.ForcingQuotient.mem_principalFilter line 477
theorem OAI.PartitionConsistency.ForcingQuotient.AtomicData.eqG_principal line 479
theorem OAI.PartitionConsistency.CohenForcing.Condition.countably_closed_below line 494
Source documentation
Passing to a cone preserves countable closure.
```
theorem countably_closed_below (d : Condition I κ) (f : ℕ → Set.Iic d) (hf : Antitone f) :
    ∃ p : Set.Iic d, ∀ n, p ≤ f n := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
def OAI.PartitionConsistency.ProductForcing.ForcedAvailable line 517
Source documentation
Availability when only equality forced by d is used. Each witness is an actual normalized name on the required subdiagram.
```
def ForcedAvailable (d : CohenForcing.Condition I κ) (r : Diagram M I)
    (τ : LocalName hμ c r) (n : M) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName
def OAI.PartitionConsistency.ProductForcing.localAvailability line 525
Source documentation
The availability ideal of a specified local name with respect to any directed filter. No dense-set meeting assumptions are required for this purely algebraic ideal assertion.
```
def localAvailability (F : GenericFilter (CohenForcing.Condition I κ))
    (r : Diagram M I) (a : M) (τ : LocalName hμ c r) : ConeIdeal (show LeftDivOrder M from a) :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.mem_localAvailability line 530
def OAI.PartitionConsistency.ProductForcing.forcedAvailability line 549
Source documentation
The principal-filter availability ideal, built from the already proved intersection/descent calculus. Its definition assumes no stability.
```
def forcedAvailability (d : CohenForcing.Condition I κ) (r : Diagram M I)
    (a : M) (τ : LocalName hμ c r) : ConeIdeal (show LeftDivOrder M from a) :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.mem_forcedAvailability line 553
theorem OAI.PartitionConsistency.ProductForcing.ForcedAvailable.mono line 569
theorem OAI.PartitionConsistency.ProductForcing.forcedAvailability_mono line 577
theorem OAI.PartitionConsistency.ProductForcing.forcedAvailability_congr line 587
Source documentation
Forced equality identifies the two actual ideals, not just their cardinalities.
```
theorem forcedAvailability_congr (d : CohenForcing.Condition I κ) (r : Diagram M I)
    (a : M) (τ σ : LocalName hμ c r)
    (heq : (system hμ).atomic.EqF ((d,r) : Poset M I κ) τ.name σ.name) :
    forcedAvailability hμ c hcard hsize hmerger d r a τ =
      forcedAvailability hμ c hcard hsize hmerger d r a σ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.forcedAvailability
theorem OAI.PartitionConsistency.ProductForcing.forcedAvailability_dense_stable line 605
Source documentation
The set of available subdiagrams of every local name can be made permanently constant by strengthening only its Cohen coordinate.
```
theorem forcedAvailability_dense_stable (H : HeightCost (LeftDivOrder M))
    (hj : HasConditionalJoins (LeftDivOrder M)) (d : CohenForcing.Condition I κ)
    (r : Diagram M I) (a : M) (τ : LocalName hμ c r) :
    ∃ e, e ≤ d ∧ ∀ f, f ≤ e →
      forcedAvailability hμ c hcard hsize hmerger f r a τ =
        forcedAvailability hμ c hcard hsize hmerger e r a τ :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.forcedAvailability
theorem OAI.PartitionConsistency.ProductForcing.localAvailability_eq_of_stable line 618
Source documentation
Once availability is stable below d, its value in EVERY directed filter containing d is the same ground ideal. This does not posit an ambient fully generic filter or identify distinct forcing extensions.
```
theorem localAvailability_eq_of_stable
    (d : CohenForcing.Condition I κ) (r : Diagram M I) (a : M) (τ : LocalName hμ c r)
    (hstable : ∀ f, f ≤ d →
      forcedAvailability hμ c hcard hsize hmerger f r a τ =
        forcedAvailability hμ c hcard hsize hmerger d r a τ)
    (F : GenericFilter (CohenForcing.Condition I κ)) (hd : d ∈ F) :
    localAvailability hμ c hcard hsize hmerger F r a τ =
      forcedAvailability hμ c hcard hsize hmerger d r a τ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.forcedAvailability, OAI.PartitionConsistency.ProductForcing.localAvailability