AssignedGraphs.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

AssignedGraph

def OAI.PartitionConsistency.ProductForcing.ChainCode.GraphWitness line 25
Source documentation
A bounded graph entry is witnessed by a genuine local assignment, with forced equality to its literal label and its normalized class name.
```
def GraphWitness (p : Poset M I κ) (x y : (S).Name) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset
def OAI.PartitionConsistency.ProductForcing.ChainCode.GraphHolds line 32
Source documentation
Density closure of the literal entry relation.
```
def GraphHolds (p : Poset M I κ) (x y : (S).Name) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphWitness_mono line 35
def OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation line 41
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphWitness_holds line 61
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphWitness_bounds line 67
Source documentation
Each literal entry really has its value in the quotient set.
```
theorem graphWitness_bounds {p : Poset M I κ} {x y : (S).Name}
    (h : GraphWitness hμ c hcard hsize hmerger hj H E hE p x y) :
    (S).atomic.MemF p x (labelSet hμ c) ∧ (S).atomic.MemF p y (quotientName hμ c E) := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.ChainCode.GraphWitness, OAI.PartitionConsistency.ProductForcing.labelSet, OAI.PartitionConsistency.ProductForcing.quotientName
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphWitness_move line 78
Source documentation
Moving the condition, diagram, name and label together preserves the literal graph predicate. The change of Cohen computation is essential.
```
theorem graphWitness_move (g : Vertex.RootGroup q) {p : Poset M I κ} {x y : (S).Name}
    (h : GraphWitness hμ c hcard hsize hmerger hj H E hE p x y) :
    GraphWitness hμ c hcard hsize hmerger hj H E hE ((S).move g.val p) (g • x) (g • y) := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.ChainCode.GraphWitness
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation_move line 90
def OAI.PartitionConsistency.ProductForcing.ChainCode.assignmentGraph line 100
Source documentation
The collected graph is a set-sized HS name with the single support D_q.
```
def assignmentGraph : (S).Name :=
…
```
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation_one line 109
Source documentation
Single-valuedness is proved at common extensions of actual diagram entries; no common preassigned component is assumed.
```
theorem graphRelation_one [Uncountable κ] (hc : Function.Injective c)
    {p : Poset M I κ} {x y z : (S).Name}
    (h : (graphRelation hμ c hcard hsize hmerger hj H E hE).holds p x y)
    (h' : (graphRelation hμ c hcard hsize hmerger hj H E hE).holds p x z) :
    (S).atomic.EqF p y z := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation_inj line 136
Source documentation
Equal graph values have equal labels, even before the cardinality conditions used to prove totality have been imposed.
```
theorem graphRelation_inj {p : Poset M I κ} {x y z : (S).Name}
    (h : (graphRelation hμ c hcard hsize hmerger hj H E hE).holds p x z)
    (h' : (graphRelation hμ c hcard hsize hmerger hj H E hE).holds p y z) :
    (S).atomic.EqF p x y := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation_total line 189
Source documentation
All label coordinates can be covered by strengthened diagrams. Thus dense local totality gives totality of the one actual graph.
```
theorem graphRelation_total (x : (S).Name) (p : Poset M I κ)
    (hp : p ≤ (d₀,q)) (hx : (S).atomic.MemF p x (labelSet hμ c)) :
    ∀ r, r ≤ p → ∃ s, s ≤ r ∧ ∃ y : (S).Name,
      (S).atomic.MemF s y (quotientName hμ c E) ∧
      (graphRelation hμ c hcard hsize hmerger hj H E hE).holds s x y := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.labelSet, OAI.PartitionConsistency.ProductForcing.quotientName, OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation_onto line 218
Source documentation
Every actual quotient member is locally a canonical class of some label. After placing that label in a diagram and stabilizing availability, the onto assertion for its exact fiber supplies a graph preimage.
```
theorem graphRelation_onto (y : (S).Name) (p : Poset M I κ)
    (hp : p ≤ (d₀,q)) (hy : (S).atomic.MemF p y (quotientName hμ c E)) :
    ∀ r, r ≤ p → ∃ s, s ≤ r ∧ ∃ x : (S).Name,
      (S).atomic.MemF s x (labelSet hμ c) ∧
      (graphRelation hμ c hcard hsize hmerger hj H E hE).holds s x y := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.ProductForcing.quotientName, OAI.PartitionConsistency.ProductForcing.labelSet, OAI.PartitionConsistency.ProductForcing.ChainCode.graphRelation
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.assignmentGraph_bijection line 253
Source documentation
Under the explicitly stated dense count and selector facts the actual HS graph is a bijection. These facts are discharged for the concrete monoid and forcing in the construction, rather than being model axioms.
```
theorem assignmentGraph_bijection [Uncountable κ] (hc : Function.Injective c) :
    (S).Forces ![assignmentGraph hμ c hcard hsize hmerger hj H E hE,
      labelSet hμ c,quotientName hμ c E] ((d₀,q) : Poset M I κ)
      ((SetLanguage.surjection 0 1 2).conj (SetLanguage.injection 0 1 2)) := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode.assignmentGraph, OAI.PartitionConsistency.ProductForcing.labelSet, OAI.PartitionConsistency.ProductForcing.quotientName, OAI.PartitionConsistency.ProductForcing.Poset, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.injection
def OAI.PartitionConsistency.CountableHull.Arity line 285
def OAI.PartitionConsistency.CountableHull.evaluate line 289

theorem OAI.PartitionConsistency.CountableHull.exists_closed line 296

Source documentation

Closure under any small family of countably-ary operations has size at most a fixed point of countable exponentiation.

theorem exists_closed {μ : Cardinal.{u}} (hω : Cardinal.aleph0 ≤ μ)
    (hpower : μ ^ Cardinal.aleph0 = μ) (hA : Cardinal.mk A ≤ μ)
    (base : X) (op : A → (ℕ → X) → X) :
    ∃ S : Set X, Cardinal.mk S ≤ μ ∧ base ∈ S ∧
      ∀ a f, (∀ n, f n ∈ S) → op a f ∈ S := by
…

theorem OAI.PartitionConsistency.CohenForcing.Condition.exists_code line 341
def OAI.PartitionConsistency.CohenForcing.Condition.code line 348
theorem OAI.PartitionConsistency.CohenForcing.Condition.code_range line 351
theorem OAI.PartitionConsistency.CohenForcing.Condition.enriched_graph_injective line 355
theorem OAI.PartitionConsistency.CohenForcing.Condition.code_injective line 365
def OAI.PartitionConsistency.CohenForcing.Condition.decode line 371
theorem OAI.PartitionConsistency.CohenForcing.Condition.decode_code line 375
def OAI.PartitionConsistency.CohenForcing.Condition.compatibleChoice line 381
theorem OAI.PartitionConsistency.CohenForcing.Condition.compatibleChoice_spec line 384
def OAI.PartitionConsistency.CohenForcing.Condition.flip line 390
def OAI.PartitionConsistency.CohenForcing.Condition.restrictedGraph line 394
theorem OAI.PartitionConsistency.CohenForcing.Condition.antichain_cardinal_le line 403
Source documentation
Every pairwise incompatible set of countable binary conditions has size at most any infinite fixed point of countable exponentiation. In particular the forcing is (2^ℵ₀)⁺-c.c., irrespective of its coordinate set.
```
theorem antichain_cardinal_le {μ : Cardinal.{u}} (hω : Cardinal.aleph0 ≤ μ)
    (hpower : μ ^ Cardinal.aleph0 = μ) (A : Set (Condition I κ))
    (hA : ∀ p ∈ A, ∀ q ∈ A, Compatible p q → p = q) : Cardinal.mk A ≤ μ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.Compatible
theorem OAI.PartitionConsistency.CohenForcing.Condition.antichain_continuum line 461
Source documentation
The source chain condition, with its precise successor-continuum bound.
```
theorem antichain_continuum (A : Set (Condition I κ))
    (hA : ∀ p ∈ A, ∀ q ∈ A, Compatible p q → p = q) :
    Cardinal.mk A ≤ Cardinal.continuum :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.Compatible
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ChainBound line 484
Source documentation
A chain bound on the concrete forcing order. Compatibility here means existence of a common stronger condition, not agreement of two names.
```
def ChainBound (ν : Cardinal.{u}) : Prop :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ChainBound.cardinal_le line 489
Source documentation
A separating family of conditions injects into an antichain.
```
theorem ChainBound.cardinal_le {ν : Cardinal.{u}} (hcc : ChainBound (P := P) ν)
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ChainBound
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ChainBound.cardinal_le_mul line 505
Source documentation
Counting an indexed relation whose witnesses with compatible conditions and equal records must have the same value.
```
theorem ChainBound.cardinal_le_mul {ν : Cardinal.{u}} (hcc : ChainBound (P := P) ν)
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ChainBound
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.possibleValues_cardinal_le line 530
Source documentation
For a fixed ground argument of an internal function, the possible values which belong to a ground set form a set of size at most the chain bound. Only the actual function-on formula supplies single-valuedness.
```
theorem possibleValues_cardinal_le {A B : Type u}
    (a : A → ZFSet.{u}) (b : B → ZFSet.{u}) (hb : Function.Injective b)
    (f : S.Name) (p : P)
    (hf : S.Forces ![f,Name.check (ZFSet.range a)] p (SetLanguage.functionOn 0 1))
    {ν : Cardinal.{u}} (hcc : ChainBound (P := P) ν) (i : A) :
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.functionOn, OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ChainBound
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.cardinal_le_of_forces_surjection line 558
Source documentation
A forced surjection between two ground sets bounds the ground size of the codomain by the domain size times the forcing's chain bound. This is the possible-values proof of cardinal preservation, with no cardinal-preservation premise hidden in the definition of a forcing extension.
```
theorem cardinal_le_of_forces_surjection {A B : Type u}
    (a : A → ZFSet.{u}) (b : B → ZFSet.{u}) (hb : Function.Injective b)
    (f : S.Name) (p : P)
    (hf : S.Forces ![f,Name.check (ZFSet.range a),Name.check (ZFSet.range b)] p
      (SetLanguage.surjection 0 1 2))
    {ν : Cardinal.{u}} (hcc : ChainBound (P := P) ν) :
…
```
Mentions: OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.Name.check, OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ChainBound