Building the conditional difference estimator from one ordinary estimator

This layer maps every conditional instance (x,y,1^t) to two ordinary MINKT instances:

• the joint input (pair x y, 1^a);
• the condition input (y, 1^b).

One numerical estimator satisfying the unconditional Fact 3.4 sandwich is evaluated on both. Their adjusted difference is the candidate conditional estimator. Compatible exposes the remaining clock identities, upper-chain bound, and loss budgets needed to instantiate SatisfiesSoIInputs.

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Plan : Type

Per-instance choices needed to form the two ordinary estimator queries.

• pairInputTime : MINCKT.Instance → ℕ

  Source clock encoded in the paired-string estimator query.

• conditionInputTime : MINCKT.Instance → ℕ

  Source clock encoded in the condition-only estimator query.

• soiTime : MINCKT.Instance → ℕ

  Base time at which the SoI hypothesis is invoked.

• pairUpperLoss : MINCKT.Instance → ℕ

  Additive loss of the paired upper-chain evaluator.

• correction : MINCKT.Instance → ℕ

  Centering and rounding correction in the final difference.

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.PairCompositionPlan : Type

Compiler and attained-minimum budgets for the paired upper-chain query.

• compile : List Bool → List Bool → List Bool

  Compile a condition program and conditional result program into one ordinary program.

• conditionBound : MINCKT.Instance → ℕ

  Program-length budget for the condition minimum.

• resultBound : MINCKT.Instance → ℕ

  Program-length budget for the conditional result minimum.

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Plan.pairInput (plan : Plan) (inst : MINCKT.Instance) : MINKT.Instance

Ordinary MINKT query for the paired output.

Equations

• plan.pairInput inst = { output := Complexity.pair inst.output inst.condition, time := plan.pairInputTime inst }

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Plan.conditionInput (plan : Plan) (inst : MINCKT.Instance) : MINKT.Instance

Ordinary MINKT query for the condition alone.

Equations

• plan.conditionInput inst = { output := inst.condition, time := plan.conditionInputTime inst }

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Plan.IsEstimatorQuery (plan : Plan) (query : MINKT.Instance) : Prop

Exactly the paired and condition-only MINKT queries issued by this plan.

Equations

• plan.IsEstimatorQuery query = ∃ (inst : Complexity.MINCKT.Instance), query = plan.pairInput inst ∨ query = plan.conditionInput inst

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Plan.components (plan : Plan) (estimate : GapMINKT.Logarithmic.Estimator) : DifferenceEstimator

Difference components obtained by applying one unconditional estimator to the paired and condition-only queries.

Equations

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

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Plan.accountingSchedule (plan : Plan) (ordinaryParameters : GapMINKT.Logarithmic.Parameters) : SoIAccountingSchedule

The SoI accounting schedule induced by the two ordinary estimator queries. The lower-estimate losses are exactly the logarithmic slacks supplied by the unconditional Fact 3.4 sandwich.

Equations

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

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.SupportsPairUpper {ordinaryTapes conditionalTapes : ℕ} (plan : Plan) (composition : PairCompositionPlan) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) : Prop

Operational evidence that the plan's pairUpperLoss really gives the unconditional upper-chain bound used by the SoI argument.

• composes (inst : MINCKT.Instance) : TimeBoundedConditionalPairCompositionAt ordinaryMachine ordinaryMachine conditionalMachine composition.compile inst.output inst.condition inst.time inst.time (plan.pairInputTime inst) (composition.conditionBound inst) (composition.resultBound inst)

  The compiler produces pair x y from a program for y followed by a conditional program for x.

• length_le (inst : MINCKT.Instance) (conditionProgram resultProgram : List Bool) : conditionProgram.length ≤ composition.conditionBound inst → resultProgram.length ≤ composition.resultBound inst → (composition.compile conditionProgram resultProgram).length ≤ resultProgram.length + conditionProgram.length + plan.pairUpperLoss inst

  Compiler length is additive up to the plan's explicit upper loss.

• condition_finite (inst : MINCKT.Instance) : ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition inst.time ≠ ⊤

  The source-clock condition minimum is attained.

• result_finite (inst : MINCKT.Instance) : inst.complexity conditionalMachine ≠ ⊤

  The source-clock conditional minimum is attained.

• condition_le_bound (inst : MINCKT.Instance) : ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition inst.time ≤ ↑(composition.conditionBound inst)

  The chosen condition budget contains the attained minimum.

• result_le_bound (inst : MINCKT.Instance) : inst.complexity conditionalMachine ≤ ↑(composition.resultBound inst)

  The chosen conditional-result budget contains the attained minimum.

structure Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Compatible {ordinaryTapes conditionalTapes : ℕ} (plan : Plan) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (ordinaryParameters : GapMINKT.Logarithmic.Parameters) (conditionalParameters : Parameters) (soiClock soiLoss : ℕ → ℕ) : Prop

Clock, upper-chain, and loss compatibility for reusing one unconditional Fact 3.4 estimator in the SoI difference construction.

• soiClock_le_conditionalTime (inst : MINCKT.Instance) : soiClock (plan.soiTime inst) ≤ conditionalParameters.transformedTime inst

  The gap clock is at least the SoI clock.

• soiSize (inst : MINCKT.Instance) : inst.output.length + inst.condition.length ≤ plan.soiTime inst

  The chosen SoI base time contains the whole pair.

• conditionInputTime_eq (inst : MINCKT.Instance) : plan.conditionInputTime inst = soiClock (plan.soiTime inst)

  The condition query's source clock is the condition clock in SoI.

• conditionTransformedTime_le (inst : MINCKT.Instance) : ordinaryParameters.transformedTime (plan.conditionInput inst) ≤ conditionalParameters.transformedTime inst

  The final conditional gap clock dominates the transformed condition-query clock. In Proposition 6.2 these are p^4(t + |x| + |y|) and p^4(t'), respectively, for t' = max {t, |x| + |y|}.

• pairTransformedTime_eq (inst : MINCKT.Instance) : ordinaryParameters.transformedTime (plan.pairInput inst) = plan.soiTime inst

  Transforming the paired query clock reaches the ordinary paired clock on the right of SoI.

• pair_upper (inst : MINCKT.Instance) : ordinaryMachine.timeBoundedKolmogorovComplexity (pair inst.output inst.condition) (plan.pairInputTime inst) ≤ inst.complexity conditionalMachine + ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition inst.time + ↑(plan.pairUpperLoss inst)

  Unconditional upper chain at the paired query's source clock.

• upperLoss_budget (inst : MINCKT.Instance) : ordinaryParameters.logarithmicSlack (plan.conditionInput inst) + plan.pairUpperLoss inst ≤ plan.correction inst

  The correction pays the condition estimator's logarithmic loss and the paired upper-chain loss.

• lowerLoss_budget (inst : MINCKT.Instance) : ordinaryParameters.logarithmicSlack (plan.pairInput inst) + soiLoss (plan.soiTime inst) + plan.correction inst ≤ conditionalParameters.logarithmicSlack inst

  The conditional logarithmic slack pays the paired estimator loss, SoI loss, and centering correction.