CoarsePrecision.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Exact common precision of the coarse recurrence

Minima and threshold maxima select existing rationals. All computed arrays therefore share one denominator whose bit length grows linearly with depth.

theorem OAI.EditApproximation.coarse_rat_add_den_dvd line 21
theorem OAI.EditApproximation.coarse_rat_mul_nat_den_dvd line 25
theorem OAI.EditApproximation.coarse_rat_div_nat_den_dvd line 31
theorem OAI.EditApproximation.coarseThresholdContribution_den_dvd line 39

theorem OAI.EditApproximation.coarsePenaltyMinimum_den_dvd line 50

Source documentation

A complete transformed child minimum retains the common precision.

theorem coarsePenaltyMinimum_den_dvd (k : ℕ) (value : Fin (2 * k + 1) → ℚ)
    (shift : Fin (2 * k + 1)) (common : ℕ) (hvalue : ∀ next, (value next).den ∣ common) :
    (univ.inf' univ_nonempty (fun next => value next + 2 * Nat.dist shift.val next.val)).den ∣ common := by
…

theorem OAI.EditApproximation.coarseThresholdChildrenCost_den_dvd line 61

theorem OAI.EditApproximation.coarseThresholdEstimate_den_dvd line 85

Source documentation

The literal rational coarse estimator has a single common denominator, including every pruning outcome and every choice of threshold labels.

theorem coarseThresholdEstimate_den_dvd {B D : ℕ} {α : Type u} [DecidableEq α]
    (k q L : ℕ) (frame : List (Option α)) (tree : CoarseSourceTree B α D)
    (draws : CoarseThresholdDraws B D) (allowance : ℚ) (allowanceDen : ℕ)
    (hB : 0 < B) (hq : 0 < q) (hL : 0 < L) (hden : 0 < allowanceDen)
    (hallowance : allowance.den ∣ allowanceDen) (start : ℕ) (shift : Fin (2 * k + 1)) :
    (coarseThresholdEstimate k q (1 / L) frame tree draws allowance start shift).den ∣
      coarseCommonDenominator allowanceDen q L B D := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseThresholdEstimate, OAI.EditApproximation.coarseCommonDenominator

theorem OAI.EditApproximation.coarseCommonDenominator_bits line 128
Source documentation
The common-denominator representation needs only linearly many factor bit lengths per coarse depth.
```
theorem coarseCommonDenominator_bits (allowanceDen q L B D : ℕ) :
    Nat.size (coarseCommonDenominator allowanceDen q L B D) ≤
      Nat.size allowanceDen + Nat.size q + D * (Nat.size L + Nat.size B + Nat.size q) + 1 := by
…
```
Mentions: OAI.EditApproximation.coarseCommonDenominator
theorem OAI.EditApproximation.coarseChildThreshold_le_scale line 139
theorem OAI.EditApproximation.coarseChildAllowance_le line 151
theorem OAI.EditApproximation.coarseThresholdContribution_le_candidate line 159
theorem OAI.EditApproximation.coarseThresholdChildrenCost_le_width line 167

theorem OAI.EditApproximation.coarseThresholdEstimate_magnitude line 199

Source documentation

All actual coarse estimates have polynomial magnitude, independently of all accuracy events and all pruning outcomes.

theorem coarseThresholdEstimate_magnitude {B D : ℕ} {α : Type u} [DecidableEq α]
    (k : ℕ) (Q lam : ℚ) (frame : List (Option α))
    (tree : CoarseSourceTree B α D) (draws : CoarseThresholdDraws B D)
    (allowance : ℚ) (hQ : 1 ≤ Q) (hlam : 0 ≤ lam) (hlamone : lam ≤ 1)
    (ha : 0 ≤ allowance) (start : ℕ) (shift : Fin (2 * k + 1)) :
    coarseThresholdEstimate k Q lam frame tree draws allowance start shift ≤
      tree.word.length + B * allowance / Q * coarseInternalNodes B D := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseThresholdEstimate, OAI.EditApproximation.coarseInternalNodes

theorem OAI.EditApproximation.coarse_rational_encoding_bits line 247

theorem OAI.EditApproximation.coarseThresholdEstimate_encoding_bits line 258

Source documentation

Every root array cell actually produced at an integer allowance has an explicit magnitude and denominator bit bound, regardless of accuracy.

theorem coarseThresholdEstimate_encoding_bits {B D : ℕ} {α : Type u} [DecidableEq α]
    (k q L : ℕ) (frame : List (Option α)) (tree : CoarseSourceTree B α D)
    (draws : CoarseThresholdDraws B D) (hB : 0 < B) (hq : 0 < q) (hL : 0 < L)
    (start : ℕ) (shift : Fin (2 * k + 1)) :
    rationalEncodingBits (coarseThresholdEstimate k q (1 / L) frame tree draws k start shift) ≤
      Nat.size (tree.word.length + B * k * coarseInternalNodes B D) +
        2 * (Nat.size q + D * (Nat.size L + Nat.size B + Nat.size q) + 2) + 1 := by
…

Mentions: OAI.EditApproximation.CoarseSourceTree, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.rationalEncodingBits, OAI.EditApproximation.coarseThresholdEstimate, OAI.EditApproximation.coarseInternalNodes