Seed.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Threshold reconstruction in the initial estimator

Deterministic reconstruction from Section 3 of the September 24, 2026 edit-distance manuscript. Concentration is kept separate: the thresholds can influence the approximate child costs, so no independence assumption about those approximate costs is made here.

def OAI.EditApproximation.thresholdContribution line 17
Source documentation
A threshold contribution of the coarse estimator.
```
noncomputable def thresholdContribution (threshold scale value : ℝ) : ℝ :=
…
```
theorem OAI.EditApproximation.thresholdContribution_nonneg line 20
theorem OAI.EditApproximation.thresholdContribution_mono line 27

theorem OAI.EditApproximation.threshold_sandwich line 40

Source documentation

Pathwise threshold sandwich. In particular, estimate may depend on threshold; the proof only uses its two deterministic error bounds.

theorem threshold_sandwich {threshold scale estimate lower upper lam : ℝ}
    (hscale : 0 ≤ scale) (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (hlower : (1 + lam) * lower - lam * threshold ≤ estimate)
    (hupper : estimate ≤ (1 - lam) * upper + lam * threshold) :
    thresholdContribution threshold scale lower ≤
        thresholdContribution threshold scale estimate ∧
      thresholdContribution threshold scale estimate ≤
        thresholdContribution threshold scale upper := by
…

Mentions: OAI.EditApproximation.thresholdContribution

theorem OAI.EditApproximation.coarse_threshold_sandwich line 63

Source documentation

The precise factors used in the manuscript's threshold sandwich.

theorem coarse_threshold_sandwich {threshold scale estimate trueCost f lam : ℝ}
    (hscale : 0 ≤ scale) (hf : 0 < f) (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (hlower : trueCost / f - lam * threshold ≤ estimate)
    (hupper : estimate ≤ f * trueCost + lam * threshold) :
    thresholdContribution threshold scale (trueCost / (f * (1 + lam))) ≤
        thresholdContribution threshold scale estimate ∧
      thresholdContribution threshold scale estimate ≤
        thresholdContribution threshold scale (f * trueCost / (1 - lam)) := by
…

Mentions: OAI.EditApproximation.thresholdContribution

theorem OAI.EditApproximation.coarse_reconstruction line 82

Source documentation

Combining the two true-cost concentration events with the pathwise sandwich updates the structural factor from f to f * (1 + lam) / (1 - lam). Neither event conditions on child accuracy.

theorem coarse_reconstruction {ι : Type*} (children : Finset ι)
    (threshold estimate trueCost : ι → ℝ) (scale allowance f lam : ℝ)
    (hscale : 0 ≤ scale) (hf : 0 < f) (hlam : 0 ≤ lam) (hlamone : lam < 1)
    (hchildLower : ∀ i ∈ children, trueCost i / f - lam * threshold i ≤ estimate i)
    (hchildUpper : ∀ i ∈ children, estimate i ≤ f * trueCost i + lam * threshold i)
    (hconcentrationLower :
      (1 - lam) * (∑ i ∈ children, trueCost i / (f * (1 + lam))) - allowance ≤
        ∑ i ∈ children, thresholdContribution (threshold i) scale
          (trueCost i / (f * (1 + lam))))
    (hconcentrationUpper :
      (∑ i ∈ children, thresholdContribution (threshold i) scale
        (f * trueCost i / (1 - lam))) ≤
…

Mentions: OAI.EditApproximation.thresholdContribution