Explicit slack amplification for the conditional MinKT reduction

The final clock is enlarged constructively so that its base-two logarithm pays the paired-estimator loss, the condition-estimator loss, the SoI loss, and the fixed pair compiler overhead. This removes the two abstract LossBudget inequalities from the exact two-query reduction.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.finalClock_source_le (clock : ℕ → ℕ) (additive compilerLoss outputLength conditionLength time : ℕ) : time ≤ finalClock clock additive compilerLoss outputLength conditionLength time

The slack-amplified clock dominates the source time.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.finalClock_iterateFour_le (clock : ℕ → ℕ) (additive compilerLoss outputLength conditionLength time : ℕ) : clockIterate clock 4 (totalTime outputLength conditionLength time) ≤ finalClock clock additive compilerLoss outputLength conditionLength time

The slack-amplified clock dominates the fourfold query clock.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.slackExponent_le_log_finalClock (clock : ℕ → ℕ) (additive compilerLoss outputLength conditionLength time : ℕ) : slackExponent clock additive compilerLoss outputLength conditionLength time ≤ Nat.log 2 (finalClock clock additive compilerLoss outputLength conditionLength time)

The final logarithmic slack contains its complete explicit loss exponent.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.lowerLoss_budget {clock : ℕ → ℕ} (hclock : Monotone clock) (additive compilerLoss : ℕ) (inst : MINCKT.Instance) : (ordinaryParameters clock).logarithmicSlack ((plan clock compilerLoss).pairInput inst) + logarithmicSoILoss clock additive ((plan clock compilerLoss).soiTime inst) + (plan clock compilerLoss).correction inst ≤ (parameters clock additive compilerLoss).logarithmicSlack inst

Monotonicity moves all three query losses from t' to the total source parameter, after which the amplified final slack pays them.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.upperLoss_budget (clock : ℕ → ℕ) (compilerLoss : ℕ) (inst : MINCKT.Instance) : (ordinaryParameters clock).logarithmicSlack ((plan clock compilerLoss).conditionInput inst) + (plan clock compilerLoss).pairUpperLoss inst ≤ (plan clock compilerLoss).correction inst

The constructive correction exactly pays the condition-query and compiler losses.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.IsRegularClock.compatible {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} {additive compilerLoss : ℕ} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} (hclock : IsRegularClock clock) (hpair : ∀ (inst : MINCKT.Instance), ordinaryMachine.timeBoundedKolmogorovComplexity (pair inst.output inst.condition) ((plan clock compilerLoss).pairInputTime inst) ≤ inst.complexity conditionalMachine + ordinaryMachine.timeBoundedKolmogorovComplexity inst.condition inst.time + ↑((plan clock compilerLoss).pairUpperLoss inst)) : Compatible (plan clock compilerLoss) ordinaryMachine conditionalMachine (ordinaryParameters clock) (parameters clock additive compilerLoss) clock (logarithmicSoILoss clock additive)

Slack amplification and the paired upper-chain theorem produce the full compatibility contract with no remaining clock or loss hypotheses.

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.IsRegularClock.compatible_of_pairComposition {ordinaryTapes conditionalTapes : ℕ} {clock : ℕ → ℕ} {additive compilerLoss : ℕ} {composition : PairCompositionPlan} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} (hclock : IsRegularClock clock) (hsupports : SupportsPairUpper (plan clock compilerLoss) composition ordinaryMachine conditionalMachine) : Compatible (plan clock compilerLoss) ordinaryMachine conditionalMachine (ordinaryParameters clock) (parameters clock additive compilerLoss) clock (logarithmicSoILoss clock additive)

The operational condition-first compiler closes the last machine-specific premise of the slack-amplified schedule.