TailGraphs.lean`

40 declarations, 0 contain sorry, 0 declared as axioms

TailCode

def OAI.PartitionConsistency.ProductForcing.ChainCode line 21
Source documentation
The ground code set in the paper: at position i a literal local normalized name supported on the i-th chain diagram.
```
def ChainCode {q : Diagram M I} {v : Vertex q} (C : Vertex.Chain v) :=
…
```
instance OAI.PartitionConsistency.ProductForcing.(instance at line 24) line 24
def OAI.PartitionConsistency.ProductForcing.ChainCode.At line 40
Source documentation
A literal HS name represents a point of the glued component at w. The name, rather than its check-name code, is used in this predicate.
```
def At (F : GenericFilter (CohenForcing.Condition I κ)) (w : Vertex q)
    (τ : (system (M := M) (I := I) (κ := κ) hμ).Name) (b : (D[F]).Glued hj v) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.ChainCode.Represents line 48
Source documentation
Eventual representation is explicitly insensitive to all entries in a finite initial segment.
```
def Represents (F : GenericFilter (CohenForcing.Condition I κ))
    (a : ChainCode hμ c C) (b : (D[F]).Glued hj v) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.at_unique line 55
Source documentation
A functioning name at one vertex has only one glued value.
```
theorem at_unique {F : GenericFilter (CohenForcing.Condition I κ)} {w : Vertex q}
    {τ : (system (M := M) (I := I) (κ := κ) hμ).Name} {b b' : (D[F]).Glued hj v}
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.represents_unique line 68
Source documentation
The same code cannot name different classes merely by choosing different finite tails.
```
theorem represents_unique {F : GenericFilter (CohenForcing.Condition I κ)}
    {a : ChainCode hμ c C} {b b' : (D[F]).Glued hj v}
    (h : Represents hμ c hcard hsize hmerger hj E hE C F a b)
    (h' : Represents hμ c hcard hsize hmerger hj E hE C F a b') : b = b' := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Represents
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.exists_representing_code line 79
Source documentation
Every glued class has a code of genuine local name representatives. This is a set-sized countable choice in the ambient ordinary computation; it is not yet a claim that an external filter is generic.
```
theorem exists_representing_code (F : GenericFilter (CohenForcing.Condition I κ))
    (b : (D[F]).Glued hj v) :
    ∃ a : ChainCode hμ c C, Represents hμ c hcard hsize hmerger hj E hE C F a b := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Represents
def OAI.PartitionConsistency.ProductForcing.ChainCode.transport line 94
Source documentation
Transport of the glued component to the moved Cohen filter, retaining its original chosen root.
```
def transport (F : GenericFilter (CohenForcing.Condition I κ))
    (g : Vertex.componentStabilizer hj v) :
    (D[F]).Glued hj v ≃
      (D[F.move (CohenForcing.Condition.permuteOrderIso g.val.val)]).Glued hj v :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.CohenForcing.Condition.permuteOrderIso
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.at_transport_iff line 103
Source documentation
This equality is about the actual transported name. In particular it does not identify movement of a check-name with movement of its code.
```
theorem at_transport_iff (F : GenericFilter (CohenForcing.Condition I κ))
    (g : Vertex.componentStabilizer hj v) (w : Vertex q)
    (τ : (system (M := M) (I := I) (κ := κ) hμ).Name) (b : (D[F]).Glued hj v) :
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.tail_fixed line 152
Source documentation
Eventual literal fixation of every entry of every individual code. The bound concerns the chain, not an invariance of its ground code wellorder.
```
theorem tail_fixed (k : C.tailFixer hj) : ∃ N, ∀ i, N ≤ i →
    k.val.val • C.vertex i = C.vertex i ∧
      ∀ τ : LocalName hμ c (C.vertex i).diagram, k.val.val.val • τ.name = τ.name := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.represents_same_code line 170
Source documentation
Source lemma least-code-covariance, at the level of functioning codes: the very same code represents the transported point at the moved filter. Only a finite prefix may cease working.
```
theorem represents_same_code (F : GenericFilter (CohenForcing.Condition I κ))
    (k : C.tailFixer hj) (a : ChainCode hμ c C) (b : (D[F]).Glued hj v) :
    Represents hμ c hcard hsize hmerger hj E hE C
      (F.move (CohenForcing.Condition.permuteOrderIso k.val.val.val)) a
      (transport hμ c hcard hsize hmerger hj E hE F k.val b) ↔
    Represents hμ c hcard hsize hmerger hj E hE C F a b := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.ProductForcing.ChainCode.Represents, OAI.PartitionConsistency.CohenForcing.Condition.permuteOrderIso, OAI.PartitionConsistency.ProductForcing.ChainCode.transport
def OAI.PartitionConsistency.ProductForcing.ChainCode.leastCode line 194
Source documentation
The least code is chosen in a single fixed wellordering of the set of all chain codes, not a fresh ordering at each filter.
```
def leastCode (F : GenericFilter (CohenForcing.Condition I κ)) (b : (D[F]).Glued hj v) :
    ChainCode hμ c C :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.leastCode_represents line 200
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.leastCode_injective line 206
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.leastCode_covariance line 216
Source documentation
Invariance of the actual minima follows from literal equality of the sets of functioning codes. No invariance of the ground wellordering under movement of all entries is asserted or needed.
```
theorem leastCode_covariance (F : GenericFilter (CohenForcing.Condition I κ))
    (k : C.tailFixer hj) (b : (D[F]).Glued hj v) :
    leastCode hμ c hcard hsize hmerger hj E hE C
      (F.move (CohenForcing.Condition.permuteOrderIso k.val.val.val))
      (transport hμ c hcard hsize hmerger hj E hE F k.val b) =
    leastCode hμ c hcard hsize hmerger hj E hE C F b := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.leastCode, OAI.PartitionConsistency.CohenForcing.Condition.permuteOrderIso, OAI.PartitionConsistency.ProductForcing.ChainCode.transport
def OAI.PartitionConsistency.ProductForcing.ChainCode.LT line 233
Source documentation
The wellordering of the glued classes induced by their least codes.
```
def LT (F : GenericFilter (CohenForcing.Condition I κ))
    (b b' : (D[F]).Glued hj v) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
instance OAI.PartitionConsistency.ProductForcing.ChainCode.leastCode_isWellOrder line 238
def OAI.PartitionConsistency.ProductForcing.ChainCode.leastCodeOrderIso line 248
Source documentation
The order-isomorphism form of least-code-covariance.
```
def leastCodeOrderIso (F : GenericFilter (CohenForcing.Condition I κ)) (k : C.tailFixer hj) :
    LT hμ c hcard hsize hmerger hj E hE C F ≃r
      LT hμ c hcard hsize hmerger hj E hE C
        (F.move (CohenForcing.Condition.permuteOrderIso k.val.val.val)) where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.ChainCode.LT, OAI.PartitionConsistency.CohenForcing.Condition.permuteOrderIso
abbrev OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.ProductEntries line 273
Source documentation
Literal children suffice to name the Cartesian product of two sets, at arbitrary ranks. The activation test retains both membership values.
```
abbrev ProductEntries (X Y : S.Name) := Edges X.raw × Edges Y.raw
```
Mentions: OAI.PartitionConsistency.SetForcingNames.Edges
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.productEntry line 275
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.productTest line 278
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.productSupport line 281
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.productSupport_mem line 285
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.product_permute line 288
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.cartesianName line 312
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.cartesianName_fixed line 316

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_cartesianName line 323

Source documentation

Exact Cartesian membership, including the assertion that every member is an actual ordered pair. All witnesses remain HS names.

theorem mem_cartesianName (X Y ν : S.Name) (p : P) :
    S.atomic.MemF p ν (S.cartesianName X Y) ↔
      ∀ q, q ≤ p → ∃ r, r ≤ q ∧ ∃ x y : S.Name,
        S.atomic.MemF r x X ∧ S.atomic.MemF r y Y ∧ S.atomic.EqF r ν (x.opair y) := by
…

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.opair_mem_cartesianName line 351
Source documentation
The Cartesian name has precisely the usual membership value on pairs.
```
theorem opair_mem_cartesianName (X Y x y : S.Name) (p : P) :
    S.atomic.MemF p (x.opair y) (S.cartesianName X Y) ↔
      S.atomic.MemF p x X ∧ S.atomic.MemF p y Y := by
…
```
structure OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation line 370
Source documentation
A regular, equality-respecting binary forcing relation. This auxiliary structure is used to construct an actual bounded set graph by collection; it is not an assumed function or an assumed semantic model.
```
structure BinaryRelation where
…
```

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_mapsTo line 379

Source documentation

Unpacking an internal map leaves its full set-function conjunct intact.

theorem forces_mapsTo {n} (v : Fin n → S.Name) (p : P) (f a b : Fin n) :
    S.Forces v p (SetLanguage.mapsTo f a b) ↔
      S.Forces ![v f,v a] p (SetLanguage.functionOn 0 1) ∧
      ∀ x y : S.Name, ∀ q, q ≤ p → S.atomic.MemF q x (v a) →
        ∀ r, r ≤ q → S.App r (v f) x y → S.atomic.MemF r y (v b) := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.mapsTo, OAI.PartitionConsistency.SetLanguage.functionOn

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_surjection line 396

Source documentation

Unpacking the graph-surjection sentence keeps all witnesses internal.

theorem forces_surjection {n} (v : Fin n → S.Name) (p : P) (f a b : Fin n) :
    S.Forces v p (SetLanguage.surjection f a b) ↔
      S.Forces ![v f,v a,v b] p (SetLanguage.mapsTo 0 1 2) ∧
      ∀ y : S.Name, ∀ q, q ≤ p → S.atomic.MemF q y (v b) →
        ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ x : S.Name,
          S.atomic.MemF s x (v a) ∧ S.App s (v f) x y := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.surjection, OAI.PartitionConsistency.SetLanguage.mapsTo

def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.test line 418
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.test_permute line 422
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.graph line 445
Source documentation
The actual HS name for the bounded relation on X × Y.
```
def graph : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.graph_fixed line 448
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.mem_graph line 452
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.app_graph line 484
Source documentation
Every application of this internal graph is exactly a related bounded pair. No external function is substituted for an internal set graph.
```
theorem app_graph (x y : S.Name) (p : P) :
    S.App p (R.graph X Y H hH hX hY hR) x y ↔
      S.atomic.MemF p x X ∧ S.atomic.MemF p y Y ∧ R.holds p x y := by
…
```

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.graph_functionOn line 512

Source documentation

Totality and uniqueness produce the internal function formula, including its prohibition of non-pairs and out-of-domain graph entries.

theorem graph_functionOn (p : P)
    (htotal : ∀ x : S.Name, ∀ q, q ≤ p → S.atomic.MemF q x X →
      ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ y : S.Name, S.atomic.MemF s y Y ∧ R.holds s x y)
    (hone : ∀ q, q ≤ p → ∀ x y z : S.Name, R.holds q x y → R.holds q x z →
      S.atomic.EqF q y z) :
    S.Forces ![R.graph X Y H hH hX hY hR,X] p (SetLanguage.functionOn 0 1) := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.functionOn

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.graph_mapsTo line 539

Source documentation

The same actual graph takes all its values in the specified codomain.

theorem graph_mapsTo (p : P)
    (htotal : ∀ x : S.Name, ∀ q, q ≤ p → S.atomic.MemF q x X →
      ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ y : S.Name, S.atomic.MemF s y Y ∧ R.holds s x y)
    (hone : ∀ q, q ≤ p → ∀ x y z : S.Name, R.holds q x y → R.holds q x z →
      S.atomic.EqF q y z) :
    S.Forces ![R.graph X Y H hH hX hY hR,X,Y] p (SetLanguage.mapsTo 0 1 2) := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.mapsTo

theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.BinaryRelation.graph_surjection line 554

Source documentation

Dense local inverse witnesses give an internal surjection, not an externally indexed family of maps.

theorem graph_surjection (p : P)
    (htotal : ∀ x : S.Name, ∀ q, q ≤ p → S.atomic.MemF q x X →
      ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ y : S.Name, S.atomic.MemF s y Y ∧ R.holds s x y)
    (hone : ∀ q, q ≤ p → ∀ x y z : S.Name, R.holds q x y → R.holds q x z →
      S.atomic.EqF q y z)
    (honto : ∀ y : S.Name, ∀ q, q ≤ p → S.atomic.MemF q y Y →
      ∀ r, r ≤ q → ∃ s, s ≤ r ∧ ∃ x : S.Name, S.atomic.MemF s x X ∧ R.holds s x y) :
    S.Forces ![R.graph X Y H hH hX hY hR,X,Y] p (SetLanguage.surjection 0 1 2) := by
…

Mentions: OAI.PartitionConsistency.SetLanguage.surjection