Growth bounds for the iterated-clock schedule -- proof internals

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

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsAdmissibleClock.ordinaryParameters_admissible_internal {clock : ℕ → ℕ} (hclock : IsAdmissibleClock clock) : (ordinaryParameters clock).IsAdmissible

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsAdmissibleClock.conditionalParameters_admissible_internal {clock : ℕ → ℕ} (hclock : IsAdmissibleClock clock) : (conditionalParameters clock).IsAdmissible