ProbeMargins.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

Probe extension: construction and preservation of real margins

structure OAI.PartitionConsistency.ProbeAlgebra.HeightIntervals line 14
Source documentation
Numerical intervals for the first-letter blocks. These inequalities are constructed from the old margin below, rather than supplied for the extension.
```
structure HeightIntervals {M : Type u} {S : Type v} [LeftCancelMonoid M] [IsConical M]
    (A : Alphabet M S) (H : HeightCost (LeftDivOrder M)) where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Alphabet
def OAI.PartitionConsistency.ProbeAlgebra.Path.letterIdeal line 36
Source documentation
The old first-letter divisors are a bounded ideal of the old monoid.
```
def letterIdeal (s : P.Letters) : ConeIdeal (α := LeftDivOrder M) (P.target s) where
…
```
def OAI.PartitionConsistency.ProbeAlgebra.Path.letterFloor line 49
Source documentation
The supremum of the heights of all old divisors of a new letter.
```
noncomputable def letterFloor (s : P.Letters) : ℝ :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.letter_heights_bdd line 52
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.height_le_letterFloor line 58
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.letterFloor_pos line 62
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.letterFloor_le line 65
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.letter_inside_cost line 72
Source documentation
Joining two old divisors inside the letter ideal provides the bound needed for missed divisors below an old-to-new comparison.
```
theorem letter_inside_cost (hM : HasConditionalJoins (LeftDivOrder M))
    {s : P.Letters} {x d : M} (hx : P.InCone x s) (hd : P.InCone d s) (hdx : ¬ d ∣ x) :
    H.cost d ≤ P.letterFloor H s - H.height x := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.target_outside_cost line 88
Source documentation
The height not yet used by the letter ideal controls every divisor of its target outside that ideal. The bound is uniform over the ideal.
```
theorem target_outside_cost {s : P.Letters} {d : M}
    (hd : d ∣ P.target s) (hdP : ¬ P.InCone d s) :
    H.cost d ≤ H.height (P.target s) - P.letterFloor H s := by
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.target_lt_exit line 106
Source documentation
The target is strictly below the exit: no right cancellation is used.
```
theorem target_lt_exit (s : P.Letters) :
    @LT.lt (LeftDivOrder M) _ (P.target s) (P.exit e s) := by
…
```

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.exists_letter_interval line 117

Source documentation

The source's two strict interval inequalities, with a single bound for all the old outside costs.

theorem exists_letter_interval (s : P.Letters) :
    ∃ u δ K : ℝ, 0 < δ ∧ P.letterFloor H s + δ < u ∧ 0 ≤ K ∧
      u + δ + K < H.height (P.exit e s) ∧
      ∀ d : M, d ∣ P.exit e s → ¬ P.InCone d s → H.cost d ≤ K := by
…

def OAI.PartitionConsistency.ProbeAlgebra.Path.heightIntervals line 144
Source documentation
Intervals for all the new letters of this actual probe extension.
```
noncomputable def heightIntervals (hM : HasConditionalJoins (LeftDivOrder M)) :
    HeightIntervals (P.alphabet he) H := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.HeightIntervals
def OAI.PartitionConsistency.ProbeAlgebra.Word.OldMinimum line 172
Source documentation
A least old cone containing a word's old right multiples. It is used only to choose a cost cap; the gate theorem proves its existence when needed.
```
def OldMinimum (w : Word A b) (g : M) : Prop :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.OldMinimum.unique line 175
def OAI.PartitionConsistency.ProbeAlgebra.Word.gateCap line 183
Source documentation
The cap is the cost of the actual least old right multiple, never that of an arbitrarily larger old multiple (costs need not be monotone).
```
noncomputable def gateCap (w : Word A b) : ℝ :=
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.gateCap_pos line 186
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.gateCap_le_one line 193
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.gateCap_eq line 200
def OAI.PartitionConsistency.ProbeAlgebra.Word.rawHeight line 210
Source documentation
Recursive heights on literal irreducibles; the same formula is harmless on unreduced strings.
```
noncomputable def rawHeight : Raw M S → ℝ
  | .old x => H.height x
  | .cons s w => V.offset s + V.scale s * rawHeight w

/-- The recursive cost makes both the suffix scale and the old gate's
cost available simultaneously. -/
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Raw, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.cons, OAI.PartitionConsistency.ProbeAlgebra.Word.cost
def OAI.PartitionConsistency.ProbeAlgebra.Word.rawCost line 216
Source documentation
The recursive cost makes both the suffix scale and the old gate's cost available simultaneously.
```
noncomputable def rawCost : (w : Raw M S) → w.reduced A b → ℝ
  | .old x, _ => H.cost x
  | .cons s w, hw => min (V.scale s * rawCost w hw.1) (gateCap A b H ⟨.cons s w, hw⟩)
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Raw, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.cons, OAI.PartitionConsistency.ProbeAlgebra.Word.gateCap
def OAI.PartitionConsistency.ProbeAlgebra.Word.height line 220
def OAI.PartitionConsistency.ProbeAlgebra.Word.cost line 221
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.height_old line 223
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.height_cons line 224
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cost_old line 226
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cost_cons line 227
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.scale_lt_one line 231
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.height_bounds line 239
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cost_bounds line 257
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cost_le_scale line 268
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cost_le_gate line 277
Source documentation
Every new word's cost is at most that of its specific old gate.
```
theorem cost_le_gate {w : Word A b} {s : S} {g : M}
    (hw : head A b w = some s) (hg : Gate A b w s g) : cost A b H V w ≤ H.cost g := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.Gate, OAI.PartitionConsistency.ProbeAlgebra.Word.cost
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cost_old_factor line 285
Source documentation
Any divisor of an old element has a cost-dominating old divisor with exactly the same old-multiple profile.
```
theorem cost_old_factor (hOld : OldIntersections A b)
    {w : Word A b} {y : M} (hwy : w ∣ old A b y) :
    ∃ g : M, OldMinimum A b w g ∧ w ∣ old A b g ∧ g ∣ y ∧ cost A b H V w ≤ H.cost g := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.OldMinimum, OAI.PartitionConsistency.ProbeAlgebra.Word.cost
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cost_other_block_factor line 299
Source documentation
The cost of an outside-block divisor is controlled by an old member of that block's letter ideal.
```
theorem cost_other_block_factor (hOld : OldIntersections A b)
    {w z : Word A b} {s : S} (hw : head A b w ≠ some s)
    (hz : head A b z = some s) (hwz : w ∣ z) :
    ∃ g : M, w ∣ old A b g ∧ old A b g ∣ z ∧ cost A b H V w ≤ H.cost g := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.OldIntersections, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.cost
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.uniform_margin_old line 326
Source documentation
For old comparisons, gates dominate every new missed cost.
```
theorem uniform_margin_old {x y : LeftDivOrder M} (hxy : x < y) :
    UniformMargin (α := LeftDivOrder (Word A b)) (height A b H V) (cost A b H V)
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.height, OAI.PartitionConsistency.ProbeAlgebra.Word.cost
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.uniform_margin_old_new line 343
Source documentation
Margins from an old element into a new first-letter block: outside costs use the letter-ideal floor, inside costs use the suffix scale.
```
theorem uniform_margin_old_new {x : M} {w : Word A b} {s : S}
    (hw : head A b w = some s) (hxw : old A b x ∣ w) :
    UniformMargin (α := LeftDivOrder (Word A b)) (height A b H V) (cost A b H V)
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.height, OAI.PartitionConsistency.ProbeAlgebra.Word.cost
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.uniform_margin_new_old line 371
Source documentation
Margins from a new first-letter block to an old multiple. The old gate bounds all costs without presuming that costs are monotone.
```
theorem uniform_margin_new_old (hb : b ≠ 1) {w : Word A b} {s : S} {y : M}
    (hw : head A b w = some s) (hwy : w ∣ old A b y) :
    UniformMargin (α := LeftDivOrder (Word A b)) (height A b H V) (cost A b H V)
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.old, OAI.PartitionConsistency.ProbeAlgebra.Word.height, OAI.PartitionConsistency.ProbeAlgebra.Word.cost
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.cons_dvd_cons_iff line 406
Source documentation
Comparisons within one block are precisely suffix comparisons.
```
theorem cons_dvd_cons_iff (hb : b ≠ 1) (s : S) (Y Z : Word A b) (hY hZ) :
    cons A b s Y hY ∣ cons A b s Z hZ ↔ Y ∣ Z := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.cons
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.uniform_margin_same_head line 415
Source documentation
The uniform margin in one block is the suffix margin multiplied by its positive scale. All other-block divisors divide both endpoints.
```
theorem uniform_margin_same_head (hb : b ≠ 1) (s : S) (Y Z : Word A b) (hY hZ)
    (hmargin : UniformMargin (α := LeftDivOrder (Word A b))
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.new_ne_old line 442
Source documentation
Old elements and elements of a first-letter block are distinct.
```
theorem new_ne_old {w : Word A b} {s : S} (hw : head A b w = some s) (x : M) : w ≠ old A b x := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.head, OAI.PartitionConsistency.ProbeAlgebra.Word.old
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.uniform_margin line 450
Source documentation
Structural induction checks every strict comparison of irreducible words, using an intervening old gate precisely for different new blocks.
```
theorem uniform_margin (hb : b ≠ 1) (z : Word A b) :
    ∀ w : Word A b, @LT.lt (LeftDivOrder (Word A b)) _ w z →
      UniformMargin (α := LeftDivOrder (Word A b)) (height A b H V) (cost A b H V) w z := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.height, OAI.PartitionConsistency.ProbeAlgebra.Word.cost
def OAI.PartitionConsistency.ProbeAlgebra.Word.heightCost line 494
Source documentation
Extending height and cost data on the actual probe normal forms.
```
noncomputable def heightCost (hb : b ≠ 1) : HeightCost (LeftDivOrder (Word A b)) where
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word
theorem OAI.PartitionConsistency.ProbeAlgebra.Word.old_cost_supremum line 515
Source documentation
New divisors need not have old costs equal to theirs. Nevertheless, the cost-dominating old gates preserve exactly each old missed-cost supremum.
```
theorem old_cost_supremum (x y : LeftDivOrder M) :
    sSup (cost A b H V ''
      {d : LeftDivOrder (Word A b) | d ≤ old A b y ∧ ¬ d ≤ old A b x}) =
        sSup (H.cost '' {d : LeftDivOrder M | d ≤ y ∧ ¬ d ≤ x}) := by
…
```
Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.cost, OAI.PartitionConsistency.ProbeAlgebra.Word, OAI.PartitionConsistency.ProbeAlgebra.Word.old
def OAI.PartitionConsistency.ProbeAlgebra.Path.extensionHeightCost line 573
Source documentation
Source lem:mono-probe-heights: admissible heights and costs on the actual indexed probe extension, constructed by its normal forms and gates.
```
noncomputable def extensionHeightCost : HeightCost (LeftDivOrder (P.Extension he b)) :=
…
```
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.extensionHeightCost_height_old line 576
theorem OAI.PartitionConsistency.ProbeAlgebra.Path.extensionHeightCost_cost_old line 579

theorem OAI.PartitionConsistency.ProbeAlgebra.Path.extension_old_cost_supremum line 584

Source documentation

The exact supremum conservativity needed at limit stages of the tower, including the case where the set of missed divisors is empty.

theorem extension_old_cost_supremum (x y : LeftDivOrder M) :
    sSup ((P.extensionHeightCost he b hb H hM).cost ''
      {d : LeftDivOrder (P.Extension he b) | d ≤ Word.old (P.alphabet he) b y ∧
        ¬ d ≤ Word.old (P.alphabet he) b x}) =
      sSup (H.cost '' {d : LeftDivOrder M | d ≤ y ∧ ¬ d ≤ x}) :=
…

Mentions: OAI.PartitionConsistency.ProbeAlgebra.Word.old