MergerCones.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

def OAI.PartitionConsistency.DiagramOrder.UniformMargin line 11
Source documentation
A uniformly strict bound on all missed costs. This is an equivalent, convenient form of the supremum margin for a strict comparison.
```
def UniformMargin (ρ ε : α → ℝ) (x y : α) : Prop :=
…
```
theorem OAI.PartitionConsistency.DiagramOrder.UniformMargin.supremum_lt line 17
theorem OAI.PartitionConsistency.DiagramOrder.UniformMargin.trans line 28
Source documentation
Margins compose across an intervening element. The proof controls the supremum, not merely each individual cost.
```
theorem trans (hxy : x < y) (hyz : y < z) (hε : ∀ a, 0 < ε a)
    (h₁ : UniformMargin ρ ε x y) (h₂ : UniformMargin ρ ε y z) :
    UniformMargin ρ ε x z := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.UniformMargin
theorem OAI.PartitionConsistency.DiagramOrder.HeightCost.uniform_margin line 44
Source documentation
The old margin supplies one uniform upper bound for every missed cost.
```
theorem uniform_margin (H : HeightCost α) {x y : α} (hxy : x < y) :
    UniformMargin H.height H.cost x y := by
…
```
Mentions: OAI.PartitionConsistency.DiagramOrder.HeightCost, OAI.PartitionConsistency.DiagramOrder.UniformMargin
def OAI.PartitionConsistency.MergerAlgebra.RightDivOrder line 61
Source documentation
Right divisibility in a free right monoid-set, used for the quotient letters, not for words in the new monoid.
```
def RightDivOrder (_M : Type u) (D : Type v) := D
…
```
instance OAI.PartitionConsistency.MergerAlgebra.RightDivOrder.(instance at line 67) line 67
instance OAI.PartitionConsistency.MergerAlgebra.RightDivOrder.(instance at line 69) line 69
lemma OAI.PartitionConsistency.MergerAlgebra.RightDivOrder.le_iff line 82
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.HasRep line 94
Source documentation
A coordinate of the quotient letter exists when the letter belongs to that prescribed copy. Each such representative is unique.
```
def HasRep (i : Fin n) (z : P.Copies hP) : Prop := ∃ x : M, P.copy hP i x = z
```
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordHeight line 96
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordCost line 100
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordHeight_copy line 106
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordCost_copy line 112
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordHeight_nonneg line 118
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordHeight_lt_one line 126
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordCost_pos line 134
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordCost_le_one line 142
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.hasRep_of_reaches line 152
Source documentation
A representation persists when its letter is multiplied on the right.
```
theorem hasRep_of_reaches {i : Fin n} {z w : P.Copies hP}
    (hz : P.HasRep hP i z) (hzw : Reaches M z w) : P.HasRep hP i w := by
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordHeight_mono line 159
Source documentation
Every summand of the finite average is nondecreasing.
```
theorem coordHeight_mono (i : Fin n) :
    Monotone (α := RightDivOrder M (P.Copies hP)) (P.coordHeight hP H i) := by
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.coordHeight_strict line 176
Source documentation
On every represented copy, a proper quotient-letter comparison makes that coordinate strictly increase.
```
theorem coordHeight_strict {i : Fin n} {z w : RightDivOrder M (P.Copies hP)}
    (hzw : z < w) (hz : P.HasRep hP i z) :
    P.coordHeight hP H i z < P.coordHeight hP H i w := by
…
```
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesHeight line 191
Source documentation
The literal finite average used in the merger height construction.
```
noncomputable def copiesHeight (z : P.Copies hP) : ℝ :=
…
```
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesCost line 196
Source documentation
A positive choice of costs below all the source's required finite bounds. The finite product is at most each represented old cost.
```
noncomputable def copiesCost (z : P.Copies hP) : ℝ :=
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesHeight_pos line 199
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesHeight_lt_one line 211
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesHeight_strictMono line 222

theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesHeight_gap line 234

Source documentation

Every coordinate increase is bounded by the increase of the average, after division by the number of copies.

theorem copiesHeight_gap (_hn : 0 < n) (i : Fin n)
    {z w : RightDivOrder M (P.Copies hP)} (hzw : z ≤ w) :
    (P.coordHeight hP H i w - P.coordHeight hP H i z) / n ≤
      P.copiesHeight hP H w - P.copiesHeight hP H z := by
…

theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesCost_pos line 246
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesCost_le_cap line 253
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesCost_le_one line 257
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesCost_le_copy line 267
Source documentation
The chosen cost satisfies the bound from every copy representing the letter, not just from the representative used to construct it.
```
theorem copiesCost_le_copy (hn : 0 < n) (i : Fin n) (x : M) :
    P.copiesCost hP H (P.copy hP i x) ≤ H.cost x / n := by
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copy_le_copy_iff line 280
Source documentation
Comparisons within a represented copy are precisely old comparisons.
```
theorem copy_le_copy_iff (i : Fin n) (x y : M) :
    @LE.le (RightDivOrder M (P.Copies hP)) _ (P.copy hP i x) (P.copy hP i y) ↔
      @LE.le (LeftDivOrder M) _ x y := by
…
```

theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copies_coordinate_margin line 289

Source documentation

A strict bound for the missed costs that have a representative in a specified copy. Crucially it is one bound for that whole class of divisors.

theorem copies_coordinate_margin (hn : 0 < n)
    {z w : RightDivOrder M (P.Copies hP)} (hzw : z < w) (i : Fin n) :
    ∃ c : ℝ, c < P.copiesHeight hP H w - P.copiesHeight hP H z ∧
      ∀ d : RightDivOrder M (P.Copies hP), d ≤ w → ¬ d ≤ z →
        P.HasRep hP i d → P.copiesCost hP H d ≤ c := by
…

theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copies_uniform_margin line 337
Source documentation
Finiteness of the copies converts their separate strict bounds into a single strict bound for the complete missed-cost supremum.
```
theorem copies_uniform_margin (hn : 0 < n)
    {z w : RightDivOrder M (P.Copies hP)} (hzw : z < w) :
    UniformMargin (α := RightDivOrder M (P.Copies hP))
…
```
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.copiesHeightCost line 351
Source documentation
Actual heights and costs on the prescribed quotient, satisfying the strict supremum margin.
```
noncomputable def copiesHeightCost (hn : 0 < n) :
    HeightCost (RightDivOrder M (P.Copies hP)) where
…
```

def OAI.PartitionConsistency.MergerAlgebra.Word.wordHeight line 371

Source documentation

Word heights with the source's parameters θ = φ = 1/4.

noncomputable def wordHeight : Word M D → ℝ
  | old x => H.height x
  | snoc w z => wordHeight w + (1 - wordHeight w) * (1 / 4 + HD.height z / 4)

/-- Positive costs satisfying both of the required last-letter bounds. -/

Mentions: OAI.PartitionConsistency.MergerAlgebra.Word

def OAI.PartitionConsistency.MergerAlgebra.Word.wordCost line 376
Source documentation
Positive costs satisfying both of the required last-letter bounds.
```
noncomputable def wordCost : Word M D → ℝ
  | old x => H.cost x
  | snoc w z => (1 - wordHeight H HD w) * min (1 / 8) (HD.cost z / 4)
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.Word.wordHeight
theorem OAI.PartitionConsistency.MergerAlgebra.Word.wordHeight_old line 380
theorem OAI.PartitionConsistency.MergerAlgebra.Word.wordHeight_snoc line 381
theorem OAI.PartitionConsistency.MergerAlgebra.Word.wordCost_old line 384
theorem OAI.PartitionConsistency.MergerAlgebra.Word.wordCost_snoc line 385
theorem OAI.PartitionConsistency.MergerAlgebra.Word.wordHeight_bounds line 388
theorem OAI.PartitionConsistency.MergerAlgebra.Word.wordCost_pos line 401
theorem OAI.PartitionConsistency.MergerAlgebra.Word.wordCost_le_one line 408
theorem OAI.PartitionConsistency.MergerAlgebra.Word.prefix_lt_snoc line 419
Source documentation
Every proper one-letter extension is a strict divisibility comparison.
```
theorem prefix_lt_snoc (w : Word M D) (z : D) :
    @LT.lt (LeftDivOrder (Word M D)) _ w (snoc w z) := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.uniform_margin_snoc line 430
Source documentation
The uniform bound for the new divisors appearing at one extra letter.
```
theorem uniform_margin_snoc (w : Word M D) (z : D) :
    UniformMargin (α := LeftDivOrder (Word M D))
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.uniform_margin_same_prefix line 450
Source documentation
For equal-length words with a common prefix, all shorter divisors are shared and the only new missed costs are controlled by the last-letter margin.
```
theorem uniform_margin_same_prefix (w : Word M D) {z t : RightDivOrder M D}
    (hzt : z < t) :
    UniformMargin (α := LeftDivOrder (Word M D))
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word, OAI.PartitionConsistency.MergerAlgebra.RightDivOrder
theorem OAI.PartitionConsistency.MergerAlgebra.Word.uniform_margin_old line 477
Source documentation
A comparison between old words has exactly its old missed costs, because no new word divides an old word.
```
theorem uniform_margin_old {x y : LeftDivOrder M} (hxy : x < y) :
    UniformMargin (α := LeftDivOrder (Word M D))
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.word_uniform_margin line 493
Source documentation
Induction through the literal normal forms verifies every strict comparison, not just the comparisons between the adjoined roots.
```
theorem word_uniform_margin (y : Word M D) :
    ∀ x : Word M D, @LT.lt (LeftDivOrder (Word M D)) _ x y →
      UniformMargin (α := LeftDivOrder (Word M D))
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
def OAI.PartitionConsistency.MergerAlgebra.Word.wordHeightCost line 523
Source documentation
Extension of the old height and cost to the actual merger monoid.
```
noncomputable def wordHeightCost : HeightCost (LeftDivOrder (Word M D)) where
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.old_missed_costs line 543
Source documentation
The set of costs of divisors missed by an old comparison is literally unchanged, since every divisor of an old word is itself an old word.
```
theorem old_missed_costs (x y : LeftDivOrder M) :
    (wordHeightCost H HD).cost ''
        {d : LeftDivOrder (Word M D) | d ≤ old y ∧ ¬ d ≤ old x} =
      H.cost '' {d : LeftDivOrder M | d ≤ y ∧ ¬ d ≤ x} := by
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word.wordHeightCost, OAI.PartitionConsistency.MergerAlgebra.Word
theorem OAI.PartitionConsistency.MergerAlgebra.Word.old_cost_supremum line 563
Source documentation
In particular, the old missed-cost supremum is exactly preserved.
```
theorem old_cost_supremum (x y : LeftDivOrder M) :
    sSup ((wordHeightCost H HD).cost ''
      {d : LeftDivOrder (Word M D) | d ≤ old y ∧ ¬ d ≤ old x}) =
        sSup (H.cost '' {d : LeftDivOrder M | d ≤ y ∧ ¬ d ≤ x}) :=
…
```
Mentions: OAI.PartitionConsistency.MergerAlgebra.Word.wordHeightCost, OAI.PartitionConsistency.MergerAlgebra.Word
def OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.mergerHeightCost line 580
Source documentation
The height and cost extension for the literal finite nonempty merger, not an assumed extension and not merely a margin on the adjoined roots.
```
noncomputable def mergerHeightCost (hn : 0 < n) :
    HeightCost (LeftDivOrder (P.Merger hP)) :=
…
```
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.merger_height_old line 584
theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.merger_cost_old line 587

theorem OAI.PartitionConsistency.DiagramForcing.OverlapPrescription.merger_old_cost_supremum line 591

Source documentation

Combining the old-divisor calculation with the constructed margins.

theorem merger_old_cost_supremum (hn : 0 < n) (x y : LeftDivOrder M) :
    sSup ((P.mergerHeightCost hP H hn).cost ''
      {d : LeftDivOrder (P.Merger hP) | d ≤ Word.old y ∧ ¬ d ≤ Word.old x}) =
        sSup (H.cost '' {d : LeftDivOrder M | d ≤ y ∧ ¬ d ≤ x}) :=
…