Explicit slack amplification -- proof internals

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.paddedTime_le_totalTime_internal (inst : MINCKT.Instance) : paddedTime inst ≤ totalTime inst.output.length inst.condition.length inst.time

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

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

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

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.losses_le_slackExponent_internal {clock : ℕ → ℕ} (hclock : Monotone clock) (additive compilerLoss : ℕ) (inst : MINCKT.Instance) : Nat.log 2 (clockIterate clock 2 (paddedTime inst)) + logarithmicSoILoss clock additive (clockIterate clock 2 (paddedTime inst)) + correction clock compilerLoss inst ≤ slackExponent clock additive compilerLoss inst.output.length inst.condition.length inst.time

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

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

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

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

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.length_le_of_timeBoundedKolmogorovComplexity_ne_top_internal {tapes : ℕ} {machine : TM tapes} {output : List Bool} {time : ℕ} (hfinite : machine.timeBoundedKolmogorovComplexity output time ≠ ⊤) : output.length ≤ time

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.pairInput_replicate_internal (clock : ℕ → ℕ) (compilerLoss length : ℕ) : (plan clock compilerLoss).pairInput { output := List.replicate length true, condition := [], time := 0 } = { output := pair (List.replicate length true) [], time := clock length }

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.pairInput_replicate_isEstimatorQuery_internal (clock : ℕ → ℕ) (compilerLoss length : ℕ) : (plan clock compilerLoss).IsEstimatorQuery { output := pair (List.replicate length true) [], time := clock length }

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.two_mul_add_two_le_clock_clock_of_satisfiesBoundsOn_internal {tapes : ℕ} {machine : TM tapes} {clock : ℕ → ℕ} {compilerLoss : ℕ} {estimate : GapMINKT.Logarithmic.Estimator} (hestimate : estimate.SatisfiesBoundsOn machine (ordinaryParameters clock) (plan clock compilerLoss).IsEstimatorQuery) (length : ℕ) : 2 * length + 2 ≤ clock (clock length)

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.two_mul_add_two_le_clock_of_forall_ne_top_internal {tapes : ℕ} {machine : TM tapes} {clock : ℕ → ℕ} {compilerLoss : ℕ} (hfinite : ∀ (query : MINKT.Instance), (plan clock compilerLoss).IsEstimatorQuery query → machine.timeBoundedKolmogorovComplexity query.output query.time ≠ ⊤) (length : ℕ) : 2 * length + 2 ≤ clock length

theorem Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.not_satisfiesBoundsOn_plan_id_internal {tapes : ℕ} (machine : TM tapes) (compilerLoss : ℕ) (estimate : GapMINKT.Logarithmic.Estimator) : ¬estimate.SatisfiesBoundsOn machine (ordinaryParameters id) (plan id compilerLoss).IsEstimatorQuery