Polynomial growth of the slack-amplified final clock

The power-of-two slack factor is bounded by the product of the three iterated clocks appearing under its logarithms. Consequently the explicit slack amplification remains polynomial and yields admissible conditional-gap parameters.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.clockIterate_add_one_polynomiallyBounded {clock : ℕ → ℕ} (hclock : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (time : ℕ), clock time ≤ coefficient * (time + 1) ^ exponent) (iterations : ℕ) : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (time : ℕ), clockIterate clock iterations time + 1 ≤ coefficient * (time + 1) ^ exponent

Adding one to a fixed polynomially bounded clock iterate preserves an explicit polynomial bound.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.pow_slackExponent_le_product (clock : ℕ → ℕ) (additive compilerLoss outputLength conditionLength time : ℕ) : 2 ^ slackExponent clock additive compilerLoss outputLength conditionLength time ≤ (clockIterate clock 2 (totalTime outputLength conditionLength time) + 1) * (clockIterate clock 3 (totalTime outputLength conditionLength time) + 1) * (clockIterate clock 4 (totalTime outputLength conditionLength time) + 1) * 2 ^ additive * 2 ^ compilerLoss

The power-of-two slack factor is controlled by a product of the three iterated query clocks and the two fixed losses.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.finalClock_polynomiallyBounded {clock : ℕ → ℕ} (additive compilerLoss : ℕ) (hclock : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (time : ℕ), clock time ≤ coefficient * (time + 1) ^ exponent) : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (outputLength conditionLength time : ℕ), finalClock clock additive compilerLoss outputLength conditionLength time ≤ coefficient * (outputLength + conditionLength + time + 1) ^ exponent

Polynomial growth of the primitive clock implies polynomial growth of the slack-amplified final clock.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.IsAdmissibleClock.parameters_admissible {clock : ℕ → ℕ} (hclock : IsAdmissibleClock clock) (additive compilerLoss : ℕ) : (parameters clock additive compilerLoss).IsAdmissible

An admissible primitive clock induces admissible slack-amplified conditional-gap parameters.