Polynomial growth of the slack-amplified final clock -- proof internals

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

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.pow_slackExponent_le_product_internal (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

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.finalClock_polynomiallyBounded_internal {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

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