LocalRecords.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

Record

def OAI.PartitionConsistency.CohenForcing.Condition.pullback line 19
Source documentation
Pull back just the coordinates in an injective diagram.
```
def pullback (d : Condition I κ) (r : A ↪ I) : Condition A κ where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.mem_pullback line 30
theorem OAI.PartitionConsistency.CohenForcing.Condition.permute_eq_of_pullback_eq line 35
Source documentation
The recorded partial function determines the original supported Cohen condition up to the specified coordinate permutation.
```
theorem permute_eq_of_pullback_eq (r s : A ↪ I) (π : Equiv.Perm I)
    (hπ : ∀ x, π (r x) = s x) (d c : Condition I κ)
    (hd : d.support ⊆ Set.range r) (hc : c.support ⊆ Set.range s)
    (h : d.pullback r = c.pullback s) : d.permute π = c := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.graph_code line 63
Source documentation
A countable graph can be enumerated after adjoining none, including when the condition is empty.
```
private theorem graph_code (d : Condition I κ) :
    ∃ f : ℕ → Option ((I × κ) × Bool),
      Set.range f = Set.insert none (Option.some '' d.graph) := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
theorem OAI.PartitionConsistency.CohenForcing.Condition.cardinal_le line 72
Source documentation
There are at most μ countable Cohen conditions on a space of size at most μ when μ is a fixed point of countable exponentiation.
```
theorem cardinal_le {μ : Cardinal.{u}} (hω : Cardinal.aleph0 ≤ μ)
    (hμ : μ ^ Cardinal.aleph0 = μ) (hI : Cardinal.mk I ≤ μ)
    (hκ : Cardinal.mk κ ≤ μ) : Cardinal.mk (Condition I κ) ≤ μ := by
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
abbrev OAI.PartitionConsistency.ProductForcing.LocalRecord line 116
Source documentation
The actual triple (b,x,t⁻¹d) in the local-quotient proof.
```
abbrev LocalRecord := M × M × CohenForcing.Condition M κ
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition
structure OAI.PartitionConsistency.ProductForcing.LocalWitness line 120
Source documentation
A local representation by the covariant family, with its literal stronger diagram and supported Cohen condition.
```
structure LocalWitness (F : GenericFilter (CohenForcing.Condition I κ))
    (r : Diagram M I) (C : I → (system (M := M) hμ).Name) (τ : LocalName hμ c r) where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.LocalName
def OAI.PartitionConsistency.ProductForcing.LocalWitness.record line 136
theorem OAI.PartitionConsistency.ProductForcing.LocalWitness.equal_of_record_eq line 143
Source documentation
Equal records identify the actual local quotient values. This proof uses only name symmetry and reflection to the root, not an action on an already evaluated extension.
```
theorem equal_of_record_eq [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (hC : ∀ π ∈ SupportFilter.Fix r.range, ∀ j, π • C j = C (π j))
    {τ σ : LocalName hμ c r} (w : LocalWitness hμ F r C τ) (z : LocalWitness hμ F r C σ)
    (hrecord : w.record = z.record) : LocalQuotient.ofName F τ = LocalQuotient.ofName F σ := by
…
```
Mentions: OAI.PartitionConsistency.SupportFilter.Fix, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.LocalWitness, OAI.PartitionConsistency.ProductForcing.LocalQuotient.ofName
def OAI.PartitionConsistency.ProductForcing.LocallyRepresented line 187
Source documentation
Local quotient values actually represented by a member of the specified family at a stronger diagram. This is a subcollection of the unrestricted local quotient, not a replacement definition for eligible E-classes.
```
def LocallyRepresented (F : GenericFilter (CohenForcing.Condition I κ))
    (r : Diagram M I) (C : I → (system (M := M) hμ).Name) :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
instance OAI.PartitionConsistency.ProductForcing.(instance at line 192) line 192
theorem OAI.PartitionConsistency.ProductForcing.locallyRepresented_cardinal_le line 202
Source documentation
The record argument bounds the entire represented collection, not merely a preselected list of representatives. No genericity of F is used in this coding bound. To apply it to D_F(r), eligibility still has to be shown to give one of these witnesses.
```
theorem locallyRepresented_cardinal_le [Infinite M] [Infinite I]
    (hpower : μ ^ Cardinal.aleph0 = μ) (hcard : Cardinal.mk M ≤ μ)
    (hκ : Cardinal.mk κ ≤ μ)
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (F : GenericFilter (CohenForcing.Condition I κ)) (r : Diagram M I)
    (C : I → (system (M := M) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.separate_bounded line 245
Source documentation
Every separation name is a normalization over the bounding name.
```
theorem separate_bounded {n} (σ : S.Name) (v : Fin n → S.Name) (φ : Formula (n+1)) :
    (S.separate σ v φ).raw ⊆ S.subsetBound σ := by
…
```
Mentions: OAI.PartitionConsistency.Formula
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.separate_move_le line 254
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.separate_move line 283
Source documentation
Literal covariance, not only fixedness, of the canonical Separation name. The very same formula is used at the moved parameter tuple.
```
theorem separate_move {n} (σ : S.Name) (v : Fin n → S.Name)
    (φ : Formula (n+1)) (g : Γ) :
    g • S.separate σ v φ = S.separate (g • σ) (fun i => g • v i) φ := by
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.relationClass line 299
Source documentation
The canonical name for {y ∈ A | (x,y) ∈ E}. No equivalence-relation axiom is needed to construct this set.
```
def relationClass (A E x : S.Name) : S.Name :=
…
```
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.mem_relationClass line 302
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.relationClass_bounded line 308
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.relationClass_move line 312
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.relationClass_congr line 319
def OAI.PartitionConsistency.SetLanguage.classOfFormula line 336
Source documentation
τ is precisely the E-class of x relative to A, expanded in pure first-order membership syntax. Slots are τ,A,E,x.
```
def classOfFormula : Formula 4 :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.classOf line 339
def OAI.PartitionConsistency.SetLanguage.isClassFormula line 343
Source documentation
τ is the E-class of some element of A. Slots are τ,A,E.
```
def isClassFormula : Formula 3 :=
…
```
Mentions: OAI.PartitionConsistency.Formula
def OAI.PartitionConsistency.SetLanguage.isClass line 346
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_classOf line 357
theorem OAI.PartitionConsistency.SetForcingNames.SymmetricSystem.forces_isClass line 379
def OAI.PartitionConsistency.ProductForcing.labelClass line 403
Source documentation
The actual canonical class of a label, supported by any diagram supporting E and containing that label's index.
```
def labelClass (E : (system (M := M) (I := I) (κ := κ) hμ).Name) (j : I) :
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.labelClass_move line 407
def OAI.PartitionConsistency.ProductForcing.localLabelClass line 412
theorem OAI.PartitionConsistency.ProductForcing.forces_localLabelClass_isClass line 420
theorem OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.mul_le_mul_left_iff line 442
Source documentation
Left multiplication, unlike right multiplication, preserves and reflects left divisibility in a left-cancellative monoid.
```
theorem mul_le_mul_left_iff (n x y : LeftDivOrder M) :
    n * x ≤ n * y ↔ x ≤ y := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.LeftDivOrder
theorem OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.le_mul_right line 450
theorem OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.isLUB_mul_left line 454
Source documentation
Conditional joins commute with left multiplication. This uses the least-upper-bound property, not a global lattice structure.
```
theorem isLUB_mul_left (n : LeftDivOrder M) {x y j : LeftDivOrder M}
    (h : IsLUB {x,y} j) : IsLUB {n*x,n*y} (n*j) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.LeftDivOrder
theorem OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.isLUB_cones line 478
Source documentation
The right-cone formulation of a conditional join.
```
theorem isLUB_cones {x y j : LeftDivOrder M} (h : IsLUB {x,y} j)
    (z : LeftDivOrder M) : x ≤ z ∧ y ≤ z ↔ j ≤ z := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.LeftDivOrder
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.sub_mono line 499
Source documentation
Strengthening reverses containment of ranges but preserves the monoid left-divisibility order of subdiagram indices.
```
theorem sub_mono (r : Diagram M I) {n m : LeftDivOrder M} (h : n ≤ m) :
    r.sub n ≤ r.sub m := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.self_le_sub line 504
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.range_inter_of_isLUB line 506
structure OAI.PartitionConsistency.LocalDiagramSystem.System line 531
Source documentation
A covariant diagram system with injective restriction and the actual support-intersection property. This is purely diagrammatic infrastructure; no counting, choice or partition principle is part of this definition.
```
structure System where
…
```
def OAI.PartitionConsistency.LocalDiagramSystem.System.Available line 549
Source documentation
Availability is existence of the same symbolic element at the specified subdiagram. It is not an independently assigned ideal.
```
def Available (r : Diagram M I) (x : D.Obj r) (n : M) : Prop :=
…
```
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.available_one line 552
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.available_lower line 561
Source documentation
Retention of representatives under two successive inclusions.
```
theorem available_lower {r : Diagram M I} {x : D.Obj r}
    {n m : LeftDivOrder M} (hnm : n ≤ m) (hm : D.Available r x m) :
    D.Available r x n := by
…
```

theorem OAI.PartitionConsistency.LocalDiagramSystem.System.available_join line 570

Source documentation

Availability at two roots descends to their exact intersection.

theorem available_join {r : Diagram M I} {x : D.Obj r}
    {n m k : LeftDivOrder M} (hn : D.Available r x n) (hm : D.Available r x m)
    (hjoin : IsLUB {n,m} k) : D.Available r x k := by
…

def OAI.PartitionConsistency.LocalDiagramSystem.System.availability line 585
Source documentation
Source availability-ideal lemma, common to symbolic elements and labels. The proof uses the already specified inclusion and intersection maps.
```
def availability (r : Diagram M I) (a : M) (x : D.Obj r) :
    ConeIdeal (show LeftDivOrder M from a) where
…
```
theorem OAI.PartitionConsistency.LocalDiagramSystem.System.mem_availability line 598
def OAI.PartitionConsistency.LocalDiagramSystem.labelSystem line 606
Source documentation
Label ranges form the literal system underlying the label availability ideals. Restriction is simply inclusion, not a choice of representatives.
```
def labelSystem : System.{u,u} M I where
…
```
def OAI.PartitionConsistency.ProductForcing.allLocalSystem line 633
Source documentation
The normalized names and the proved support descent instantiate the intersection calculus. Eligibility as an E-class is a later subcollection.
```
def allLocalSystem [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ)
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (F : GenericFilter (CohenForcing.Condition I κ)) :
    LocalDiagramSystem.System.{u,u+1} M I where
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition