ParameterSlack.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Explicit slack at the large-input cutoff

The cutoff is handled symbolically: no expression with an astronomically large exponent is expanded. The small-growth estimate supplies the induction step. This proves the generous polynomial-versus-binary bound used throughout the manuscript's numerical estimates.

theorem OAI.EditApproximation.polynomial_binary_growth_step line 16
theorem OAI.EditApproximation.astronomical_polynomial_bound line 38
theorem OAI.EditApproximation.astronomical_parameter_slack line 87

theorem OAI.EditApproximation.fourth_root_polynomial_slack line 93

Source documentation

The fourth-root scale has ample polynomial slack.

theorem fourth_root_polynomial_slack {ell H quarterRoot : ℝ}
    (hell : 1 ≤ ell) (hH : ell ^ 20000 ≤ H)
    (hroot : 0 ≤ quarterRoot) (hrootPower : quarterRoot ^ 4 = H) :
    ell ^ 5000 ≤ quarterRoot := by
…

theorem OAI.EditApproximation.refinement_error_envelope line 106

Source documentation

The five explicit terms in Section 8 are collectively below 1/ell. Here quarterRoot = H^(1/4) and q = p_*+21. The hypotheses are small consequences of the manuscript's large-input cutoff, not asymptotic notation or a presumed error bound.

theorem refinement_error_envelope {ell H quarterRoot q : ℝ}
    (hell : 64000000000000 ≤ ell) (hH : ell ^ 2 ≤ H)
    (hroot : ell ^ 4 ≤ quarterRoot) (hq : 0 ≤ q) (hqSquare : q ^ 2 ≤ ell) :
    52000 / H ^ 18 + 8040000 * ell ^ 4 / quarterRoot ^ 2 +
        200 * ell / quarterRoot + 1000000 * q / ell ^ 2 + 13200 / H ^ 2 < 1 / ell := by
…