The iterated-clock schedule -- proof internals

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.clockIterate_zero_internal (clock : ℕ → ℕ) (time : ℕ) : clockIterate clock 0 time = time

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.clockIterate_succ_internal (clock : ℕ → ℕ) (iterations time : ℕ) : clockIterate clock (iterations + 1) time = clock (clockIterate clock iterations time)

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.clockIterate_monotone_internal {clock : ℕ → ℕ} (hclock : Monotone clock) (iterations : ℕ) : Monotone (clockIterate clock iterations)

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.clockIterate_dominates_internal {clock : ℕ → ℕ} (hclock : ∀ (time : ℕ), time ≤ clock time) (iterations time : ℕ) : time ≤ clockIterate clock iterations time

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.paddedTime_size_le_internal (inst : MINCKT.Instance) : inst.output.length + inst.condition.length ≤ paddedTime inst

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.paddedTime_time_le_internal (inst : MINCKT.Instance) : inst.time ≤ paddedTime inst

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.paddedTime_le_total_internal (inst : MINCKT.Instance) : paddedTime inst ≤ inst.time + inst.output.length + inst.condition.length

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.ordinaryParameters_transformedTime_internal (clock : ℕ → ℕ) (inst : MINKT.Instance) : (ordinaryParameters clock).transformedTime inst = clock inst.time

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.conditionalParameters_transformedTime_internal (clock : ℕ → ℕ) (inst : MINCKT.Instance) : (conditionalParameters clock).transformedTime inst = clockIterate clock 4 (inst.time + inst.output.length + inst.condition.length)

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan_pairInputTime_internal (clock : ℕ → ℕ) (pairUpperLoss correction : MINCKT.Instance → ℕ) (inst : MINCKT.Instance) : (plan clock pairUpperLoss correction).pairInputTime inst = clockIterate clock 1 (paddedTime inst)

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan_conditionInputTime_internal (clock : ℕ → ℕ) (pairUpperLoss correction : MINCKT.Instance → ℕ) (inst : MINCKT.Instance) : (plan clock pairUpperLoss correction).conditionInputTime inst = clockIterate clock 3 (paddedTime inst)

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan_soiTime_internal (clock : ℕ → ℕ) (pairUpperLoss correction : MINCKT.Instance → ℕ) (inst : MINCKT.Instance) : (plan clock pairUpperLoss correction).soiTime inst = clockIterate clock 2 (paddedTime inst)

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan_pairUpperLoss_internal (clock : ℕ → ℕ) (pairUpperLoss correction : MINCKT.Instance → ℕ) (inst : MINCKT.Instance) : (plan clock pairUpperLoss correction).pairUpperLoss inst = pairUpperLoss inst

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan_correction_internal (clock : ℕ → ℕ) (pairUpperLoss correction : MINCKT.Instance → ℕ) (inst : MINCKT.Instance) : (plan clock pairUpperLoss correction).correction inst = correction inst

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsRegularClock.ordinaryParameters_widening_internal {clock : ℕ → ℕ} (hclock : IsRegularClock clock) : (ordinaryParameters clock).IsWidening

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsRegularClock.conditionalParameters_widening_internal {clock : ℕ → ℕ} (hclock : IsRegularClock clock) : (conditionalParameters clock).IsWidening

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsRegularClock.estimatorQuery_finite_internal {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} {pairUpperLoss correction : MINCKT.Instance → ℕ} {composition : PairCompositionPlan} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} (hclock : IsRegularClock clock) (hsupports : SupportsPairUpper (plan clock pairUpperLoss correction) composition ordinaryMachine conditionalMachine) {query : MINKT.Instance} (hquery : (plan clock pairUpperLoss correction).IsEstimatorQuery query) : ordinaryMachine.timeBoundedKolmogorovComplexity query.output query.time ≠ ⊤

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsRegularClock.compatible_internal {ordinaryTapes conditionalTapes : ℕ} {clock soiLoss : ℕ → ℕ} {pairUpperLoss correction : MINCKT.Instance → ℕ} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} (hclock : IsRegularClock clock) (hloss : LossBudget clock pairUpperLoss correction soiLoss) (hpair : ∀ (inst : MINCKT.Instance), ordinaryMachine.timeBoundedKolmogorovComplexity (pair inst.output inst.condition) ((plan clock pairUpperLoss correction).pairInputTime inst) ≤ inst.complexity conditionalMachine + ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition inst.time + ↑((plan clock pairUpperLoss correction).pairUpperLoss inst)) : Compatible (plan clock pairUpperLoss correction) ordinaryMachine conditionalMachine (ordinaryParameters clock) (conditionalParameters clock) clock soiLoss

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsRegularClock.compatible_of_pairComposition_internal {ordinaryTapes conditionalTapes : ℕ} {clock soiLoss : ℕ → ℕ} {pairUpperLoss correction : MINCKT.Instance → ℕ} {composition : PairCompositionPlan} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} (hclock : IsRegularClock clock) (hloss : LossBudget clock pairUpperLoss correction soiLoss) (hsupports : SupportsPairUpper (plan clock pairUpperLoss correction) composition ordinaryMachine conditionalMachine) : Compatible (plan clock pairUpperLoss correction) ordinaryMachine conditionalMachine (ordinaryParameters clock) (conditionalParameters clock) clock soiLoss