The iterated-clock schedule in the conditional MinKT reduction

This module constructs the exact p, p^2, p^3, and p^4 query schedule from Proposition 6.2. A regular primitive clock, explicit finite loss budget, and the already-formalized paired upper-chain theorem produce the complete Compatible contract for reducing conditional gap MinKT to two ordinary gap MinKT estimator queries.

@[simp]

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

@[simp]

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

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

Every fixed iterate of a monotone primitive clock is monotone.

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

Repeated application of a widening primitive clock only increases time.

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan_correction (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 {clock : ℕ → ℕ} (hclock : IsRegularClock clock) : (ordinaryParameters clock).IsWidening

A regular clock makes the one-step ordinary gap transform widening.

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

A regular clock makes the final four-step conditional transform widening.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.not_satisfiesBounds_ordinaryParameters {tapes : ℕ} (machine : TM tapes) (clock : ℕ → ℕ) (estimate : GapMINKT.Logarithmic.Estimator) : ¬estimate.SatisfiesBounds machine (ordinaryParameters clock)

The full-domain estimator sandwich is unsatisfiable for the iterated plan's ordinary parameters: their transformed clock ignores output length, so at source time 0 no machine prints a string longer than clock 0. The consequences therefore require the sandwich only on the plan's own estimator queries (SatisfiesBoundsOn).

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

The exact iterated clocks and finite loss inequalities discharge every non-machine field of the unconditional-estimator compatibility contract.

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

Combining the operational condition-first compiler with the exact iterated-clock/loss schedule yields the complete compatibility contract.