DiagramOrder.lean`

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

class OAI.PartitionConsistency.DiagramOrder.IsConical line 9
Source documentation
Conicality is the condition from the source, not right cancellation.
```
class IsConical (M : Type*) [Monoid M] : Prop where
…
```
def OAI.PartitionConsistency.DiagramOrder.LeftDivOrder line 13
Source documentation
The underlying monoid, equipped with the left-divisibility order below.
```
def LeftDivOrder (M : Type*) := M
…
```
instance OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.(instance at line 17) line 17
instance OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.(instance at line 20) line 20
instance OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.(instance at line 23) line 23
instance OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.(instance at line 26) line 26
instance OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.(instance at line 42) line 42
theorem OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.le_iff line 46
theorem OAI.PartitionConsistency.DiagramOrder.LeftDivOrder.factor_unique line 49
structure OAI.PartitionConsistency.DiagramOrder.HeightCost line 60
Source documentation
Exact height and cost hypotheses from equation (mono-margin). For the strict comparisons used in that equation, the set of costs is nonempty and bounded; the real conditional supremum is therefore the ordinary one.
```
structure HeightCost (α : Type*) [PartialOrder α] where
…
```
theorem OAI.PartitionConsistency.DiagramOrder.HeightCost.point_margin line 74
Source documentation
Each missing divisor's positive cost is paid by the height increase.
```
theorem point_margin {x y d : α} (hxy : x < y) (hdy : d ≤ y) (hdx : ¬ d ≤ x) :
    H.cost d < H.height y - H.height x := by
…
```
theorem OAI.PartitionConsistency.DiagramOrder.HeightCost.strictMono_height line 82
theorem OAI.PartitionConsistency.DiagramOrder.HeightCost.directed_cofinal_sequence line 92
Source documentation
The central countability argument of lem:mono-countable-ideal. In fact, only nonemptiness and directedness of the set are needed. No cardinality assumption, inaccessible, or prechosen sequence is used.
```
theorem directed_cofinal_sequence {U : Set α} (hne : U.Nonempty)
    (hdir : DirectedOn (· ≤ ·) U) :
    ∃ f : ℕ → α, (∀ n, f n ∈ U) ∧ Monotone f ∧ ∀ d ∈ U, ∃ n, d ≤ f n := by
…
```
def OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins line 145
Source documentation
A conditional join exists exactly for pairs possessing a common upper bound. In the divisibility order this says that the intersection of two principal right cones, when nonempty, is a principal right cone.
```
def HasConditionalJoins (α : Type*) [PartialOrder α] : Prop :=
…
```
structure OAI.PartitionConsistency.DiagramOrder.ConeIdeal line 151
Source documentation
An ideal in the source's bounded cone: nonempty and downward closed, contained in the cone, and closed under its finite nonempty joins. Closure under binary joins suffices, since singleton joins add no new condition.
```
structure ConeIdeal (a : α) where
…
```
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.directed line 160
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.countable_cofinal_sequence line 169
Source documentation
Source lem:mono-countable-ideal, including the stipulated first entry. When α = LeftDivOrder M, the bottom element in this statement is 1.
```
theorem countable_cofinal_sequence [OrderBot α] (H : HeightCost α)
    (hj : HasConditionalJoins α) {a : α} (U : ConeIdeal a) :
    ∃ f : ℕ → α, f 0 = ⊥ ∧ (∀ n, f n ∈ U.carrier) ∧ Monotone f ∧
      ∀ d ∈ U.carrier, ∃ n, d ≤ f n := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HeightCost, OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.ConeIdeal
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.ext line 194
Source documentation
Equality of bounded ideals is equality of their underlying subsets.
```
@[ext] theorem ext {a : α} {U V : ConeIdeal a} (h : U.carrier = V.carrier) : U = V := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.ConeIdeal
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.carrier_of_cofinal line 202
Source documentation
A cofinal sequence determines an ideal without any choices of individual lower elements: the ideal is exactly the lower closure of the sequence.
```
theorem carrier_of_cofinal {a : α} (U : ConeIdeal a) {f : ℕ → α}
    (hf : ∀ n, f n ∈ U.carrier) (hcof : ∀ d ∈ U.carrier, ∃ n, d ≤ f n) :
    U.carrier = {d | ∃ n, d ≤ f n} := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.ConeIdeal
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.cardinal_bound line 214
Source documentation
The countable-cofinal-chain coding bound used when enumerating the monoid requirements. This proves the cardinal bound, but does not construct a monoid realizing those requirements.
```
theorem cardinal_bound [OrderBot α] (H : HeightCost α)
    (hj : HasConditionalJoins α) (a : α) :
    Cardinal.mk (ConeIdeal a) ≤ Cardinal.mk α ^ Cardinal.aleph0 := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HeightCost, OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.ConeIdeal
theorem OAI.PartitionConsistency.DiagramOrder.ConeIdeal.cardinal_le line 231
Source documentation
Under the scheduling bound μ^ℵ₀ = μ, there are at most μ ideals in each bounded cone of a monoid (or order) of size at most μ.
```
theorem cardinal_le [OrderBot α] (H : HeightCost α)
    (hj : HasConditionalJoins α) (a : α) {μ : Cardinal}
    (hα : Cardinal.mk α ≤ μ) (hμ : μ ^ Cardinal.aleph0 = μ) :
    Cardinal.mk (ConeIdeal a) ≤ μ := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HeightCost, OAI.PartitionConsistency.DiagramOrder.HasConditionalJoins, OAI.PartitionConsistency.DiagramOrder.ConeIdeal