AvailableRecords.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Eligible

def OAI.PartitionConsistency.ProductForcing.EligibleName line 18
Source documentation
Actual forcing eligibility, not the existence of a preselected class representative or a coding witness.
```
def EligibleName (F : GenericFilter (CohenForcing.Condition I κ)) (r : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name) (τ : LocalName hμ c r) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.ProductForcing.eligibleName_transport line 23
theorem OAI.PartitionConsistency.ProductForcing.eligibleName_congr line 46
def OAI.PartitionConsistency.ProductForcing.Eligible line 54
Source documentation
The class assertion descends to the actual local name quotient.
```
def Eligible (F : GenericFilter (CohenForcing.Condition I κ)) (r : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name) : LocalQuotient (c := c) hμ F r → Prop :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.LocalQuotient
theorem OAI.PartitionConsistency.ProductForcing.eligible_ofName line 59
theorem OAI.PartitionConsistency.ProductForcing.eligible_restrict line 63
theorem OAI.PartitionConsistency.ProductForcing.eligible_restrict_iff line 77
Source documentation
Decision of the class test at its supporting root reflects eligibility from every stronger diagram. No assertion of E being an equivalence relation or of nonwellorderability is needed for this logical step.
```
theorem eligible_restrict_iff [Infinite M] [Infinite I]
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (F : GenericFilter (CohenForcing.Condition I κ)) (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.EligibleClasses line 101
Source documentation
D_F(r), before restricting diagrams to lie below a fixed supporting root. Its only membership test is the forcing assertion that a name is a class of some element of A.
```
def EligibleClasses (F : GenericFilter (CohenForcing.Condition I κ)) (r : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name) :=
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
instance OAI.PartitionConsistency.ProductForcing.(instance at line 105) line 105
def OAI.PartitionConsistency.ProductForcing.eligibleLabel line 110
Source documentation
Every label in the range has its canonical eligible class name.
```
def eligibleLabel (F : GenericFilter (CohenForcing.Condition I κ)) (r : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.classRepresentationSet line 120
Source documentation
A genuinely dense set of Cohen conditions giving literal local records. The diagram may be strengthened and the condition's support put in it.
```
def classRepresentationSet (r : Diagram M I) (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.classRepresentationSet_denseBelow line 125
def OAI.PartitionConsistency.ProductForcing.classRepresentationDenseSet line 160
Source documentation
Padding the preceding local witness set with incompatible conditions is dense in the entire Cohen poset, as required for ordinary genericity.
```
def classRepresentationDenseSet (r : Diagram M I) (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.ProductForcing.classRepresentationDenseSet_dense line 164
theorem OAI.PartitionConsistency.ProductForcing.localWitness_of_meets line 176
Source documentation
Meeting this specific dense set supplies the record used in the local quotient bound. Arbitrary filters are not silently declared generic.
```
theorem localWitness_of_meets (F : GenericFilter (CohenForcing.Condition I κ))
    (r : Diagram M I) (E : (system (M := M) (I := I) (κ := κ) hμ).Name) (τ : LocalName hμ c r)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.LocalName
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.le_of_common_and_range line 199
Source documentation
Among two subdiagrams of the same larger diagram, range containment reflects the diagram order. Common embeddability is essential here.
```
theorem le_of_common_and_range {t r s : Diagram M I} (htr : t ≤ r) (hts : t ≤ s)
    (hrs : s.range ⊆ r.range) : r ≤ s := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram
theorem OAI.PartitionConsistency.DiagramForcing.Diagram.intersection_le_root line 208
Source documentation
An exact intersection of two roots which both extend q still extends q.
```
theorem intersection_le_root {p s₀ s₁ q : Diagram M I}
    (hs₀ : s₀ ≤ p) (h₀q : s₀ ≤ q) (h₁q : s₁ ≤ q)
    (hinter : s₀.range ∩ s₁.range = p.range) : p ≤ q := by
…
```
Mentions: OAI.PartitionConsistency.DiagramForcing.Diagram
theorem OAI.PartitionConsistency.ProductForcing.eligibleClasses_cardinal_le line 227
Source documentation
The local quotient bound for the actual E-class predicate. The meet assumption is only for the explicitly proved dense record sets; it must be supplied by ordinary forcing, not by declaring an arbitrary filter generic.
```
theorem eligibleClasses_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)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.eligibleSystem line 265
Source documentation
The actual symbolic class system below q. Outside the cone below q the object type is empty, so no meaningless eligibility assertions are needed. All maps retain representative names and all axioms are proved.
```
def eligibleSystem [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ)
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (F : GenericFilter (CohenForcing.Condition I κ)) (q : Diagram M I)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
def OAI.PartitionConsistency.ProductForcing.classAvailability line 295
Source documentation
The availability set of an eligible E-class is the source's actual ideal: it records existence of representatives at subdiagrams, not an ideal supplied as extra structure. This specializes the proved intersection calculus.
```
def classAvailability [Infinite M] [Infinite I]
    (hcard : Cardinal.mk M ≤ μ)
    (hsize : Cardinal.mk M < Cardinal.mk I) (hmerger : HasFiniteMergers M)
    (F : GenericFilter (CohenForcing.Condition I κ)) (q r : Diagram M I) (a : M)
    (hqa : r.sub a = q)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.mem_iff_mem_join line 317
Source documentation
An ideal can be recovered above any member by taking joins with it.
```
theorem mem_iff_mem_join {a : LeftDivOrder M} (U : ConeIdeal a)
    {n z j : LeftDivOrder M} (hn : n ∈ U.carrier) (hj : IsLUB {z,n} j) :
    z ∈ U.carrier ↔ j ∈ U.carrier :=
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.LeftDivOrder, OAI.PartitionConsistency.DiagramOrder.ConeIdeal
def OAI.PartitionConsistency.DiagramOrder.ConeIdeal.contract line 323
Source documentation
Contraction of an actual bounded ideal, with no new choice of an ideal.
```
def contract {a : LeftDivOrder M} (U : ConeIdeal a)
    {n c : LeftDivOrder M} (hn : n ∈ U.carrier) (hnc : n*c = a) : ConeIdeal c where
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.LeftDivOrder, OAI.PartitionConsistency.DiagramOrder.ConeIdeal
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.mem_contract line 339
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.eq_of_contract_eq line 345
Source documentation
In a monoid with conditional joins the contraction remembers the full ideal, provided that its contraction index belongs to that ideal.
```
theorem eq_of_contract_eq (hj : HasConditionalJoins (LeftDivOrder M))
    {a n c : LeftDivOrder M} {U V : ConeIdeal a} (hnU : n ∈ U.carrier)
    (hnV : n ∈ V.carrier) (hnc : n*c = a)
    (h : U.contract hnU hnc = V.contract hnV hnc) : U = V := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.LeftDivOrder, OAI.PartitionConsistency.DiagramOrder.ConeIdeal
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.contract_one line 358
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.contract_contract line 366
Source documentation
Two contractions equal contraction at the product, literally on their carriers.
```
theorem contract_contract {a n c m b : LeftDivOrder M} (U : ConeIdeal a)
    (hn : n ∈ U.carrier) (hnc : n*c = a)
    (hm : m ∈ (U.contract hn hnc).carrier) (hmb : m*b = c) :
    (U.contract hn hnc).contract hm hmb =
      U.contract hm (by rw [mul_assoc,hmb,hnc]) := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.LeftDivOrder, OAI.PartitionConsistency.DiagramOrder.ConeIdeal, OAI.PartitionConsistency.DiagramOrder.ConeIdeal.contract

theorem OAI.PartitionConsistency.LocalDiagramSystem.System.restrict_range_iff line 385

Source documentation

Inclusion from a fixed earlier level preserves and reflects being in any later range.

theorem restrict_range_iff {r s t : Diagram M I} (hrs : r ≤ s) (hst : s ≤ t)
    (y : D.Obj s) :
    (∃ z : D.Obj t, D.restrict (hrs.trans hst) z = D.restrict hrs y) ↔
      ∃ z : D.Obj t, D.restrict hst z = y := by
…

theorem OAI.PartitionConsistency.LocalDiagramSystem.System.range_congr line 397

Source documentation

Equality of target diagrams is sufficient to compare the ranges; all order proofs are irrelevant.

theorem range_congr {r s t : Diagram M I} (x : D.Obj r)
    (hrs : r ≤ s) (hrt : r ≤ t) (h : s = t) :
    (∃ y : D.Obj s, D.restrict hrs y = x) ↔
      ∃ y : D.Obj t, D.restrict hrt y = x := by
…

theorem OAI.PartitionConsistency.LocalDiagramSystem.System.available_sub_iff line 405

Source documentation

Availability transforms by multiplication of the subdiagram indices.

theorem available_sub_iff (r : Diagram M I) (n m : M) (y : D.Obj (r.sub n)) :
    D.Available (r.sub n) y m ↔
      D.Available r (D.restrict (r.self_le_sub n) y) (n*m) := by
…

theorem OAI.PartitionConsistency.LocalDiagramSystem.System.available_restrict line 412
Source documentation
An included element is available at its original diagram.
```
theorem available_restrict (r : Diagram M I) (n : M) (y : D.Obj (r.sub n)) :
    D.Available r (D.restrict (r.self_le_sub n) y) n := ⟨y,rfl⟩
```

theorem OAI.PartitionConsistency.LocalDiagramSystem.System.availability_sub line 417

Source documentation

The availability ideal at a contracted diagram is exactly the contracted availability ideal.

theorem availability_sub (r : Diagram M I) (a n c : M) (hnc : n*c = a)
    (y : D.Obj (r.sub n)) :
    D.availability (r.sub n) c y =
      (D.availability r a (D.restrict (r.self_le_sub n) y)).contract
        ⟨⟨c,hnc⟩,D.available_restrict r n y⟩ hnc := by
…

def OAI.PartitionConsistency.LocalDiagramSystem.System.Fiber line 434
Source documentation
Exact fibers, defined using the proved availability ideal rather than an arbitrarily assigned classification.
```
def Fiber (r : Diagram M I) (a : M) (U : ConeIdeal (show LeftDivOrder M from a)) :=
…
```

def OAI.PartitionConsistency.LocalDiagramSystem.System.fiberRestrict line 438

Source documentation

The inclusion map underlying a contraction between exact fibers.

def fiberRestrict (hj : HasConditionalJoins (LeftDivOrder M))
    (r : Diagram M I) (a n c : M) (U : ConeIdeal (show LeftDivOrder M from a))
    (hn : (show LeftDivOrder M from n) ∈ U.carrier) (hnc : n*c = a)
    (y : D.Fiber (r.sub n) c (U.contract hn hnc)) : D.Fiber r a U :=
…

theorem OAI.PartitionConsistency.LocalDiagramSystem.System.fiberRestrict_bijective line 448

Source documentation

Source contraction-identification lemma, common to label and symbolic systems. Bijectivity uses the full-ideal reconstruction by joins.

theorem fiberRestrict_bijective (hj : HasConditionalJoins (LeftDivOrder M))
    (r : Diagram M I) (a n c : M) (U : ConeIdeal (show LeftDivOrder M from a))
    (hn : (show LeftDivOrder M from n) ∈ U.carrier) (hnc : n*c = a) :
    Function.Bijective (D.fiberRestrict hj r a n c U hn hnc) := by
…

def OAI.PartitionConsistency.LocalDiagramSystem.System.fiberEquiv line 470

Source documentation

A canonical fiber equivalence. Its forward map is inclusion, not an independent chosen bijection.

noncomputable def fiberEquiv (hj : HasConditionalJoins (LeftDivOrder M))
    (r : Diagram M I) (a n c : M) (U : ConeIdeal (show LeftDivOrder M from a))
    (hn : (show LeftDivOrder M from n) ∈ U.carrier) (hnc : n*c = a) :
    D.Fiber (r.sub n) c (U.contract hn hnc) ≃ D.Fiber r a U :=
…