The iterated-clock schedule in the conditional MinKT reduction

This definitions layer records the exact clock schedule in Proposition 6.2 of Hirahara's Symmetry of Information from Meta-Complexity. For t' = max {t, |x| + |y|}, the two ordinary estimator queries use source clocks p(t') and p^3(t'), symmetry of information is invoked at p^2(t'), and the final conditional gap clock is p^4(t + |x| + |y|).

The logarithmic losses are not hidden in asymptotic notation. LossBudget states exactly what the correction must absorb and what must fit inside the final logarithmic slack.

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.clockIterate (clock : ℕ → ℕ) : ℕ → ℕ → ℕ

Repeated application of a primitive clock. clockIterate clock k time is the paper's p^(k)(t).

Equations

• One or more equations did not get rendered due to their size.
• Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.clockIterate clock 0 x✝ = x✝

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.paddedTime (inst : MINCKT.Instance) : ℕ

The SoI base input t' = max {t, |x| + |y|}.

Equations

• Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.paddedTime inst = max (inst.output.length + inst.condition.length) inst.time

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.ordinaryParameters (clock : ℕ → ℕ) : GapMINKT.Logarithmic.Parameters

The ordinary gap estimator advances its source clock by one application of clock; the output length is deliberately irrelevant.

Equations

• Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.ordinaryParameters clock = { clock := fun (_outputLength time : ℕ) => clock time }

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.conditionalParameters (clock : ℕ → ℕ) : Parameters

The final conditional clock p^4(t + |x| + |y|).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.logarithmicSoILoss (clock : ℕ → ℕ) (additive time : ℕ) : ℕ

The logarithmic SoI loss log_2(p(t)) + additive.

Equations

• Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.logarithmicSoILoss clock additive time = Nat.log 2 (clock time) + additive

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.plan (clock : ℕ → ℕ) (pairUpperLoss correction : MINCKT.Instance → ℕ) : Plan

The exact two-query plan, with an explicit composition loss and centering correction.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.halfSlackCorrection (clock : ℕ → ℕ) (inst : MINCKT.Instance) : ℕ

The paper's half-slack centering correction. Its adequacy is deliberately kept as a separate finite inequality in LossBudget.

Equations

• One or more equations did not get rendered due to their size.

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.LossBudget (clock : ℕ → ℕ) (pairUpperLoss correction : MINCKT.Instance → ℕ) (soiLoss : ℕ → ℕ) : Prop

Exact finite loss inequalities for the iterated-clock construction.

The first field pays for the lower guarantee on the condition estimator and the ordinary pair compiler. The second field fits the paired-estimator loss, the SoI loss, and the centering correction inside the final gap slack.

• upper (inst : MINCKT.Instance) : Nat.log 2 (clockIterate clock 4 (paddedTime inst)) + pairUpperLoss inst ≤ correction inst

  Losses that must be removed to obtain the source-clock upper estimate.

• lower (inst : MINCKT.Instance) : Nat.log 2 (clockIterate clock 2 (paddedTime inst)) + soiLoss (clockIterate clock 2 (paddedTime inst)) + correction inst ≤ (conditionalParameters clock).logarithmicSlack inst

  Losses that must fit inside the final transformed-clock error.

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsRegularClock (clock : ℕ → ℕ) : Prop

Monotonicity and widening are the exact order properties used to align the four iterated clocks. Polynomial growth is established separately.

• monotone : Monotone clock

  More source time cannot reduce the clock allowance.

• dominates (time : ℕ) : time ≤ clock time

  One clock application never gives less time.

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsAdmissibleClock (clock : ℕ → ℕ) extends Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.IsRegularClock clock : Prop

A regular primitive clock with a uniform polynomial upper bound.

• monotone : Monotone clock
• dominates (time : ℕ) : time ≤ clock time
• polynomiallyBounded : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (time : ℕ), clock time ≤ coefficient * (time + 1) ^ exponent

  One polynomial controls the primitive clock at every input.