Helper for Proposition 4.1.18: subtracting a fixed reference value preserves the monotone objective decrease along a cubic-regularization trajectory.
Helper for Proposition 4.1.18: an explicit target hit bounds the least hitting index from above.
Helper for Proposition 4.1.18: if the initial iterate misses the target set, then the least hitting index is at least one.
Helper for Proposition 4.1.18: any subunit real upper bound on a least hitting index forces
that least index to be 0.
Helper for Proposition 4.1.18: if the least ε-hitting index has a subunit real upper
bound, then the initial gap already satisfies the target.
Helper for Proposition 4.1.18: once an antitone sequence enters a threshold region, every later term stays in that same region.
Helper for Proposition 4.1.18: an attained maximal radius over the initial sublevel-set image immediately gives the usual pointwise radius bound on that sublevel set.
Helper for Proposition 4.1.18: a one-step second-phase bound yields the exact lower bound on
the displayed logb 4 tail potential corresponding to the ratio (4 * ω₀) / Δ.
Helper for Proposition 4.1.18: the cleaner tail potential
logb 4 ((4 * ω) / δ) grows by a pure multiplicative factor 3 / 2 under the second-phase
recurrence.
Helper for Proposition 4.1.18: under the exact 1 / 3 second-phase recurrence, the same
logb 4 ((4 * ω) / δ) potential gains an additive logb 4 (3 / 2) term before the familiar
3 / 2 geometric factor appears.
Helper for Proposition 4.1.18: after shifting by 2 * logb 4 (3 / 2), the exact 1 / 3
second-phase recurrence still yields a clean geometric 3 / 2 growth law along any positive
tail segment.
Helper for Proposition 4.1.18: once a positive gap is already below ω / 3, the normalized
tail potential logb 4 ((4 * ω) / δ) starts at least at level 1.
Helper for Proposition 4.1.18: if a second-phase potential owner already grows like 3 ^ j,
then the tail reaches the displayed target within the source-facing logb 3 term up to the
unavoidable integer ceiling slack.
Helper for Proposition 4.1.18: along any positive second-phase tail, the normalized logb 4
potential grows at least geometrically with ratio 3 / 2.
Helper for Proposition 4.1.18: if a monotone second-phase tail is still positive at the
chosen horizon j, then the same logb 4 potential already satisfies the geometric lower bound
at that horizon.
Helper for Proposition 4.1.18: under the chapter's second-phase recurrence, entering the
threshold δ ≤ (4 / 9) * ω only certifies the next gap at the sharper level
δNext ≤ (4 / 27) * ω.
Helper for Proposition 4.1.18: the exact second-phase potential owner proved in this file
reaches the target ε with the valid base-3 / 2 double-logarithmic budget.
Helper for Proposition 4.1.18: once a monotone nonnegative gap sequence is already below
ω / 3, the second-phase superlinear recurrence reaches any target ε ∈ (0, ω] within the
displayed double-logarithmic budget.
Helper for Proposition 4.1.18: the exact 1 / 3 local-model tail step still yields the
already verified base-3 / 2 tail budget once the tail gaps are known to stay nonnegative.
Helper for Proposition 4.1.18: the currently verified proposition-level tail budget uses the
base-(3 / 2) double-logarithmic owner once the trajectory has entered ω / 3.
Helper for Proposition 4.1.18: the currently proved three-phase witness bounds add up to the
displayed 25 / 4 coefficient together with two unavoidable ceiling slacks coming from the
intermediate-entry and tail witnesses.
Helper for Proposition 4.1.18: if the middle phase absorbs the two ceiling slacks left by the
intermediate-entry and tail witnesses, then the three-phase witness closes the displayed
25 / 4 bound exactly.
Helper for Proposition 4.1.18: for the verified repaired bound, the middle phase only needs
to absorb one of the two ceiling slacks, leaving the tail's unavoidable +1 term explicit.
Helper for Proposition 4.1.18: on targets at least 1, the sharper source-facing
logb 3 term is dominated by the verified same-file 1 + logb (3 / 2) tail owner.
Helper for Proposition 4.1.18: on every target at least 1, the currently verified
1 + logb (3 / 2) tail owner is strictly larger than the source-facing logb 3 term. This
records the exact tail mismatch left in the two historical theorems.
Helper for Proposition 4.1.18: on the small-χ scalar parameters μ = 1, L = D = 1 / 10,
and ε = 50 / 9, the displayed plain bound is already strictly below 1.
Helper for Proposition 4.1.18: any proof of the displayed plain global bound on a subunit budget branch already forces the initial iterate to hit the target accuracy.
Helper for Proposition 4.1.18: the proposition threshold ω₀ = μ^3 / (18 L^2) is exactly the
(4 / 9)-fraction of the star-convex first/second-phase scale μ^3 / (8 L^2).
Helper for Proposition 4.1.18: the displayed logarithmic tail constant is exactly 4 * ω₀
in the plain strong-convex setting.
Helper for Proposition 4.1.18: the plain displayed logarithmic target is always at least 1
whenever ε ∈ (0, ω₀].
Helper for Proposition 4.1.18: a global minimizer of a strongly convex function is a valid star center on the whole space.
Helper for Proposition 4.1.18: strong convexity and a chosen global minimizer produce the
canonical quadratic-growth witness UsesConstant Set.univ f xStar μ.
Helper for Proposition 4.1.18: strong convexity turns the current objective gap into the
distance bound ‖method k - xStar‖ ≤ sqrt ((2 / μ) * (f (method k) - f xStar)).
Helper for Proposition 4.1.18: the cubic feasible-comparison estimate plus strong convexity
at xStar yield the local scalar model used in the strong first-phase count.
Helper for Proposition 4.1.18: the proposition threshold ω₀ = μ^3 / (18 L^2) converts the
strong-convexity radius Real.sqrt ((2 / μ) * gap) into the normalized scalar
Real.sqrt (gap / ω₀).
Helper for Proposition 4.1.18: the local comparison inequality rewrites entirely in terms of
the normalized plain gap (f (method k) - f xStar) / ω₀.
Helper for Proposition 4.1.18: once the plain strong-convex cubic-regularization gap reaches
the proposition threshold ω₀, the accepted step satisfies the chapter's second-phase
superlinear estimate with the natural scale μ^3 / (8 L^2).
Helper for Proposition 4.1.18: once the plain trajectory reaches ω₀, the current
second-phase API only certifies a one-step drop to ω₀ / 3.
Helper for Proposition 4.1.18: once the plain strong-convex gap is already at the sharper
threshold ω₀ / 3, the remaining tail to accuracy ε is controlled by the shared
double-logarithmic estimate.
Helper for Proposition 4.1.18: the currently verified plain tail term uses the
base-(3 / 2) logarithm once the gap is below ω₀ / 3.
Helper for Proposition 4.1.18: comparing the first accepted cubic step with the minimizer
xStar immediately yields the coarse source scale (L / 2) * D^3.
Helper for Proposition 4.1.18: if the characteristic ratio χ = (L * D) / μ is at most
1 / 3, then the first cubic-regularization step already reaches the sharper threshold
ω₀ / 3.
Helper for Proposition 4.1.18: the initial bounded-sublevel radius D gives the plain
one-step gap model Δₖ₊₁ ≤ (1 - α) Δₖ + (L / 2) α^3 D^3 used for the inverse-square phase.
Helper for Proposition 4.1.18: after the first accepted cubic step, the shifted plain
strong-convex gaps satisfy the inverse-square bound with scale (3 / 2) * L * D^3.
Helper for Proposition 4.1.18: the first-step estimate together with the shifted inverse-square
phase already yields an explicit entry index for the intermediate strong-convex scale
(3 / 2) * μ * D^2.
Helper for Proposition 4.1.18: in the normalized large-phase variables, the endpoint choice
α = 1 / β is feasible whenever β ≥ 1.
Helper for Proposition 4.1.18: the positive threshold ω₀ cancels against its normalized
quotient.
Helper for Proposition 4.1.18: in normalized fourth-root variables, the strong-convex
large-phase scalar model drops by 1 / 6 in one step.
Helper for Proposition 4.1.18: while the gap stays above ω₀, the normalized fourth root of
the strong-convex gap drops by 1 / 6 at each step.
Helper for Proposition 4.1.18: starting from any current gap upper bound g, the normalized
fourth root of the plain strong-convex gap decreases linearly while the trajectory remains above
the threshold ω₀.
Helper for Proposition 4.1.18: from any current upper bound g on the plain strong-convex
gap, one reaches the threshold ω₀ within at most 6 * (g / ω₀)^(1/4) further steps.
Helper for Proposition 4.1.18: after normalizing the current strong-convex first/second-phase
budget, the quarter-root term is exactly 27 * χ^2. This isolates the quantitative normal form
of the verified middle-phase route.
Helper for Proposition 4.1.18: the current coarse middle-phase owner
1 + 6 * (27 * a^2)^(1/4) is strictly larger than the displayed 13 / 4 * sqrt a budget on
every nonnegative parameter a. This is the scalar obstruction behind the historical
25 / 4 prefix coefficient.
Helper for Proposition 4.1.18: after rewriting the verified middle-phase ratio in terms of
χ, the current first/second-phase route is strictly larger than the displayed 13 / 4 * sqrt χ
budget. Arithmetic alone therefore cannot close the historical prefix coefficient from this
route.
Helper for Proposition 4.1.18: after the inverse-square entry phase has already reduced the
plain gap to (3 / 2) * μ * D^2, the verified first-phase threshold hit plus one local
ω₀ -> ω₀ / 3 step give a coarse witness for the sharper threshold.
Helper for Proposition 4.1.18: in the large-χ branch where the displayed middle-phase
budget is at least 2, after the inverse-square entry phase has already reduced the plain gap to
(3 / 2) * μ * D^2, the existing coarse threshold witness follows from the sharp middle-phase
budget by a one-time scalar domination.
Helper for Proposition 4.1.18: the middle-phase route currently closes through the same coarse
ω₀ -> ω₀ / 3 witness extracted from the verified first-phase threshold hit.
Helper for Proposition 4.1.18: even on the large-prefix-budget branch, the currently verified
plain prefix route only supplies existence of a witness reaching the sharper threshold ω₀ / 3;
the displayed 25 / 4 * sqrt χ - 1 budget remains the statement-side gap.
Helper for Proposition 4.1.18: once the plain branch supplies a prefix witness at the
threshold ω₀ / 3 within the displayed 25 / 4 * sqrt χ budget and the exact source-facing
tail owner from that witness, the historical global bound is just least-index assembly.
Proposition 4.1.18 (1): verified public theorem closing the dependency-closed plain bound coming from the same-file first/second-phase route.
Wrapper for Proposition 4.1.18 (1): theorem-shaped public entry exposing the current same-file plain bound.
Helper for Proposition 4.1.18: the current dependency-closed plain route already yields a
fully verified coarse global bound by combining the explicit intermediate-entry witness, the
current ω₀ -> ω₀ / 3 prefix witness, and the repaired base-(3 / 2) tail theorem.
Helper for Proposition 4.1.18: once the plain branch provides a prefix witness k₀ with the
displayed 25 / 4 * sqrt χ budget and gap threshold ω₀ / 3, the verified same-file theorem is
just least-index assembly plus the repaired base-(3 / 2) tail owner.
Canonical verified repaired companion: this is the fully checked same-file plain global bound currently available in the dependency-closed route.
Helper for Proposition 4.1.18: any proof of the displayed transformed global bound on a subunit budget branch already forces the initial transformed iterate to hit the target accuracy.
Helper for Proposition 4.1.18: the transformed proposition threshold
μ^3 / (18 * σ^6 * L^2) is the (4 / 9)-fraction of the natural local superlinear scale
μ^3 / (8 * σ^6 * L^2).
Helper for Proposition 4.1.18: the displayed transformed logarithmic tail constant is exactly
4 * ω₀.
Helper for Proposition 4.1.18: the transformed displayed logarithmic target is always at
least 1 whenever ε ∈ (0, ω₀].
Helper for Proposition 4.1.18: evaluating the transformed local comparison model at α = 1
removes the convex-combination term and leaves the local cubic superlinear bound around
problem.xStar.
Helper for Proposition 4.1.18: the transformed local cubic model rewrites into the same
normalized superlinear recurrence as the plain strong-convex theorem, with the proposition scale
μ^3 / (8 σ^6 L^2).
Helper for Proposition 4.1.18: once the transformed trajectory reaches ω₀, the current
second-phase API only certifies a one-step drop to ω₀ / 3.
Helper for Proposition 4.1.18: after the transformed trajectory enters the proposition
threshold ω₀, one more local step reaches ω₀ / 3. This isolates the verified transformed
prefix witness from the still-missing sharp 6.25 * sqrt ((σ / μ) * L * D) arithmetic.
Helper for Proposition 4.1.18: the transformed local comparison inequality rewrites in terms
of the proposition threshold ω₀ = μ^3 / (18 σ^6 L^2), yielding the same normalized scalar
surface as in the plain strong-convex branch.
Helper for Proposition 4.1.18: once the transformed strong-convex gap is already at the
sharper threshold ω₀ / 3, the remaining tail to accuracy ε is controlled by the same
double-logarithmic estimate.
Helper for Proposition 4.1.18: the currently verified transformed tail term uses the
base-(3 / 2) logarithm once the transformed gap is below ω₀ / 3.
Helper for Proposition 4.1.18: the transformed trajectory has a source-compatible witness
entering the threshold region ω₀ / 3; the missing part is only the sharp prefix budget.
Helper for Proposition 4.1.18: in the transformed large-prefix-budget branch, the currently
verified route still only supplies existence of a witness reaching ω₀ / 3; the displayed
25 / 4 * sqrt ((σ / μ) * L * D) - 1 budget remains the open statement-side issue.
Helper for Proposition 4.1.18: once the transformed branch supplies a threshold witness at
ω₀ / 3 within the displayed 25 / 4 * sqrt ((σ / μ) * L * D) budget and the exact
source-facing transformed tail owner from that witness, the historical bound is again just
least-index assembly.
Proposition 4.1.18 (2): verified public theorem closing the transformed bound obtained from
the explicit threshold-entry witness and the repaired base-(3 / 2) tail theorem.
Wrapper for Proposition 4.1.18 (2): theorem-shaped public entry exposing the current same-file transformed bound.
Helper for Proposition 4.1.18: once the transformed branch provides a prefix witness k₀
with the displayed 25 / 4 * sqrt ((σ / μ) * L * D) budget and gap threshold ω₀ / 3, the
verified same-file theorem is again just least-index assembly plus the repaired base-(3 / 2)
tail owner.
Canonical verified repaired companion: this is the fully checked same-file transformed global bound currently available in the dependency-closed route.