DependencyPathEnvelope.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

An explicit subpolynomial envelope for the finite dependency-path sum. The connection between this sum and an execution is a separate obligation.

theorem OAI.EditApproximation.nat_pow_eq_exp_log line 14
theorem OAI.EditApproximation.dependencyPathBudget_exp_bound line 18
theorem OAI.EditApproximation.computed_dependency_path_envelope line 61
theorem OAI.EditApproximation.computed_dependency_path_subpolynomial line 86
Source documentation
The entire displayed path bound is M^j times a subpolynomial factor, uniformly at all physical depths.
```
theorem computed_dependency_path_subpolynomial (C₁ C₂ : ℕ) (epsilon : ℝ)
    (hepsilon : 0 < epsilon) :
    ∀ᶠ N in atTop, ∀ j ≤ computedMaxTreeDepth N,
      (dependencyPathBudget j (computedDependencyIndexCount N)
        ((integerParameters N).M * inputSmallLog N ^ C₁)
        (inputHeight N ^ (C₂ * (coarseExponent (inputSmallLog N) + 1))) : ℝ) ≤
        ((integerParameters N).M : ℝ) ^ j * (N + 2 : ℝ) ^ epsilon := by
…
```
Mentions: OAI.EditApproximation.computedMaxTreeDepth, OAI.EditApproximation.dependencyPathBudget, OAI.EditApproximation.computedDependencyIndexCount, OAI.EditApproximation.integerParameters, OAI.EditApproximation.inputSmallLog, OAI.EditApproximation.inputHeight, OAI.EditApproximation.coarseExponent