CoarseInitial.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The executable initial integer estimate

The direct branches handle long targets and equality. The remaining branch evaluates the concrete coarse recurrence at every dyadic guess, takes the rational minimum, rounds up and clamps to the input length.

theorem OAI.EditApproximation.coarseStructuralFactor_le_two line 25
Source documentation
A finite Bernoulli-inequality bound for the exact structural factor. The paper's lam = 1/(64H) and D ≤ H satisfy these loose conditions.
```
theorem coarseStructuralFactor_le_two (lam : ℚ) (D : ℕ)
    (hlam : 0 ≤ lam) (hsmall : lam ≤ 1 / 4)
    (hdepth : 4 * (D : ℚ) * lam ≤ 1) : coarseStructuralFactor lam D ≤ 2 := by
…
```
Mentions: OAI.EditApproximation.coarseStructuralFactor
def OAI.EditApproximation.CoarseInitialAccuracyEvent line 64
theorem OAI.EditApproximation.coarseEntryTree_word line 72
theorem OAI.EditApproximation.coarse_good_dyadic_guess line 79
theorem OAI.EditApproximation.coarseInitialValue_le_length line 84
theorem OAI.EditApproximation.coarseInitialValue_zero line 95
Source documentation
Every original zero-cost instance returns zero on every execution.
```
theorem coarseInitialValue_zero {α : Type u} [DecidableEq α]
    (B D : ℕ) (Q lam : ℚ) (N : ℕ) (x y : List α)
    (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B D)
    (hzero : edit x y = 0) : coarseInitialValue B D Q lam N x y draws = 0 := by
…
```
Mentions: OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseInitialValue
theorem OAI.EditApproximation.coarseInitialCandidate_lower line 105
Source documentation
Every dyadic candidate lies above the original edit cost on its literal pathwise event, even when the guess is below the true distance.
```
theorem coarseInitialCandidate_lower {α : Type u} [DecidableEq α]
    (B D : ℕ) (Q lam : ℚ) (x y : List α)
    (i : CoarseGuessIndex (coarseEntryWidth x y)) (draws : CoarseThresholdDraws B D)
    (hcapacity : coarseEntryWidth x y ≤ B ^ D)
    (hQ : 0 ≤ Q) (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (hfactor : coarseStructuralFactor lam D ≤ 2)
    (hevent : let k := coarseGuess (coarseEntryWidth x y) i
…
```
Mentions: OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseStructuralFactor, OAI.EditApproximation.coarseGuess
theorem OAI.EditApproximation.coarseInitialCandidate_upper line 147
Source documentation
A dyadic guess in [d,2d) has the manuscript's coarse polynomial distortion after actual threshold reconstruction and fresh padding.
```
theorem coarseInitialCandidate_upper {α : Type u} [DecidableEq α]
    (B D : ℕ) (Q lam : ℚ) (x y : List α)
    (i : CoarseGuessIndex (coarseEntryWidth x y)) (draws : CoarseThresholdDraws B D)
    (hcapacity : coarseEntryWidth x y ≤ B ^ D)
    (hQ : 0 ≤ Q) (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (hfactor : coarseStructuralFactor lam D ≤ 2)
    (hevent : let k := coarseGuess (coarseEntryWidth x y) i
…
```
Mentions: OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseStructuralFactor, OAI.EditApproximation.coarseGuess

theorem OAI.EditApproximation.coarseInitialValue_bounds line 191

Source documentation

On the proved finite-tree events, the executable initial table entry is an integer between the actual edit cost and its stated coarse factor.

theorem coarseInitialValue_bounds {α : Type u} [DecidableEq α]
    (B D : ℕ) (Q lam : ℚ) (N : ℕ) (x y : List α)
    (draws : CoarseGuessIndex (coarseEntryWidth x y) → CoarseThresholdDraws B D)
    (hcapacity : coarseEntryWidth x y ≤ B ^ D) (hN : coarseEntryWidth x y ≤ N)
    (hQ : 0 ≤ Q) (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (hfactor : coarseStructuralFactor lam D ≤ 2)
    (hevent : CoarseInitialAccuracyEvent B D Q lam x y draws) :
    edit x y ≤ coarseInitialValue B D Q lam N x y draws ∧
      coarseInitialValue B D Q lam N x y draws ≤ (25 + 16 * B * D) * edit x y := by
…

Mentions: OAI.EditApproximation.CoarseGuessIndex, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseThresholdDraws, OAI.EditApproximation.coarseStructuralFactor, OAI.EditApproximation.CoarseInitialAccuracyEvent, OAI.EditApproximation.coarseInitialValue

instance OAI.EditApproximation.coarseInitialMeasure_isProbabilityMeasure line 249
Source documentation
Independent finite coarse streams for the listed dyadic guesses.
```
instance coarseInitialMeasure_isProbabilityMeasure (B D n : ℕ) [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)] :
    IsProbabilityMeasure (coarseInitialMeasure B D n) := by
…
```
Mentions: OAI.EditApproximation.coarseInitialMeasure

theorem OAI.EditApproximation.coarseInitialAccuracyEvent_failure line 257

Source documentation

The dyadic seed event has an explicit finite failure bound under the scalar Bernstein hypothesis.

theorem coarseInitialAccuracyEvent_failure {B D : ℕ} [NeZero B] {α : Type u} [DecidableEq α]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (Q lam : ℚ) (x y : List α)
    (hQ : 2 ≤ Q) (hlam : 0 < lam) (hlamone : lam < 1)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (coarseInitialMeasure B D (coarseEntryWidth x y)).real
      {draws | ¬ CoarseInitialAccuracyEvent B D Q lam x y draws} ≤
      (Nat.clog 2 (coarseEntryWidth x y) + 1 : ℕ) * (coarseInternalNodes B D : ℝ) *
        (4 * (2 * 2 ^ Nat.clog 2 (coarseEntryWidth x y) + 1 : ℕ) *
          Real.exp (-(lam : ℝ) * Q / 12)) := by
…

Mentions: OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.coarseInitialMeasure, OAI.EditApproximation.coarseEntryWidth, OAI.EditApproximation.CoarseInitialAccuracyEvent, OAI.EditApproximation.coarseInternalNodes