Growth bounds for the iterated-clock schedule

Finite iteration preserves the library's explicit polynomial-growth contract. In particular, an admissible primitive clock makes both the one-step ordinary gap transform and the four-step conditional gap transform admissible.

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

Every fixed finite iterate of a polynomially bounded clock is again polynomially bounded.

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

An admissible primitive clock induces admissible ordinary logarithmic-gap parameters.

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

An admissible primitive clock induces admissible fourfold conditional-gap parameters.