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 : ℕ)
:
@[simp]
theorem
Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.clockIterate_succ
(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.
@[simp]
theorem
Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.ordinaryParameters_transformedTime
(clock : ℕ → ℕ)
(inst : MINKT.Instance)
:
@[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)
:
@[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)
:
@[simp]
theorem
Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan_pairUpperLoss
(clock : ℕ → ℕ)
(pairUpperLoss correction : MINCKT.Instance → ℕ)
(inst : MINCKT.Instance)
:
@[simp]
theorem
Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan_correction
(clock : ℕ → ℕ)
(pairUpperLoss correction : MINCKT.Instance → ℕ)
(inst : MINCKT.Instance)
:
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.IsRegularClock.estimatorQuery_finite
{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)
:
Every ordinary-estimator query in the iterated plan has finite time-bounded complexity. Paired queries use the operational composition upper bound; condition queries use the attained source minimum and clock widening.
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.