CodeCardinals.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

CodeCardinal

def OAI.PartitionConsistency.ProductForcing.LocalWitness.below line 25
Source documentation
A stronger principal quotient retains every literal representation witness. In particular its three ground record entries do not change.
```
def below (w : LocalWitness hμ (principalFilter d) r A τ) (hed : e ≤ d) :
    LocalWitness hμ (principalFilter e) r A τ :=
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.LocalWitness
theorem OAI.PartitionConsistency.ProductForcing.LocalWitness.record_below line 29
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalType_cardinal_le line 45
Source documentation
Every decided value of the literal ordinal-type name has ground cardinality at most μ. Neither genericity nor a supply of representatives is an assumption: the needed records are obtained by density.
```
theorem ordinalType_cardinal_le (hpower : μ ^ Cardinal.aleph0 = μ)
    (hκ : Cardinal.mk κ ≤ μ) (b : M)
    (hb : Cardinal.mk ((Set.range (fun x : M => b*x))ᶜ : Set M) = Cardinal.mk M)
    (d : CohenForcing.Condition I κ) (θ : Ordinal.{u})
    (hθ : (system (M := M) (I := I) (κ := κ) hμ).atomic.EqF ((d,v.diagram) : Poset M I κ)
…
```
Mentions: OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.system, OAI.PartitionConsistency.ProductForcing.Poset
theorem OAI.PartitionConsistency.ProductForcing.ChainCode.rooted_of_same line 148
Source documentation
Changing a code within its forced equivalence class preserves its root representative. Equality is reflected along the actual chain arrows.
```
theorem rooted_of_same {a b : ChainCode hμ c C} {d : CohenForcing.Condition I κ}
    {τ : LocalName hμ c v.diagram} (ha : Rooted hμ c C a d τ) (hs : Same hμ c C d a b) :
    Rooted hμ c C b d τ := by
…
```
Mentions: OAI.PartitionConsistency.ProductForcing.ChainCode, OAI.PartitionConsistency.CohenForcing.Condition, OAI.PartitionConsistency.ProductForcing.LocalName, OAI.PartitionConsistency.ProductForcing.ChainCode.Rooted, OAI.PartitionConsistency.ProductForcing.ChainCode.Same

theorem OAI.PartitionConsistency.ProductForcing.ChainCode.ordinalType_lower_count line 166

Source documentation

For every probe row one can force a selected representative and its ordinal rank. Equal possible ranks in compatible conditions force two probe classes equal, contrary to the outside-list assertion and exact intersection.

theorem ordinalType_lower_count (e b : M) {K : Type u} [Uncountable K]
    (m : K × K → M) (hmb : ∀ i, m i*b = v.index*e)
    (hm : ∀ i (n : M), n ∣ v.index ∧ n ∣ m i ↔ n ∈ v.ideal.carrier)
    (hinter : ∀ i (n : M), n ∣ v.index → n ∉ v.ideal.carrier →
      ∀ z : M, n ∣ z ∧ m i ∣ z ↔ v.index*e ∣ z)
    (hind : ∀ i j, i ≠ j → ∀ z : M, m i ∣ z ∧ m j ∣ z ↔ v.index*e ∣ z)
    (E : (system (M := M) (I := I) (κ := κ) hμ).Name)
…

Mentions: OAI.PartitionConsistency.ProductForcing.system