Explicit slack amplification -- proof internals #
theorem
Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.finalClock_source_le_internal
(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)