Time-bounded description composition -- proof internals #
theorem
Complexity.TimeBoundedProgramCompositionAt.restrict_bounds_internal
{jointTapes firstTapes secondTapes : ℕ}
{jointMachine : TM jointTapes}
{firstMachine : TM firstTapes}
{secondMachine : OracleTM secondTapes}
{compile : List Bool → List Bool → List Bool}
{firstOutput secondOutput : List Bool}
{firstTime secondTime jointTime firstBound secondBound : ℕ}
(hcompose :
TimeBoundedProgramCompositionAt jointMachine firstMachine secondMachine compile firstOutput secondOutput firstTime
secondTime jointTime firstBound secondBound)
{smallerFirstBound smallerSecondBound : ℕ}
(hfirst : smallerFirstBound ≤ firstBound)
(hsecond : smallerSecondBound ≤ secondBound)
:
TimeBoundedProgramCompositionAt jointMachine firstMachine secondMachine compile firstOutput secondOutput firstTime
secondTime jointTime smallerFirstBound smallerSecondBound
theorem
Complexity.TimeBoundedProgramCompositionAt.mono_jointTime_internal
{jointTapes firstTapes secondTapes : ℕ}
{jointMachine : TM jointTapes}
{firstMachine : TM firstTapes}
{secondMachine : OracleTM secondTapes}
{compile : List Bool → List Bool → List Bool}
{firstOutput secondOutput : List Bool}
{firstTime secondTime firstJointTime secondJointTime firstBound secondBound : ℕ}
(hcompose :
TimeBoundedProgramCompositionAt jointMachine firstMachine secondMachine compile firstOutput secondOutput firstTime
secondTime firstJointTime firstBound secondBound)
(hjoint : firstJointTime ≤ secondJointTime)
:
TimeBoundedProgramCompositionAt jointMachine firstMachine secondMachine compile firstOutput secondOutput firstTime
secondTime secondJointTime firstBound secondBound
theorem
Complexity.timeBoundedKolmogorovComplexity_pair_le_of_composition_internal
{jointTapes firstTapes secondTapes : ℕ}
{jointMachine : TM jointTapes}
{firstMachine : TM firstTapes}
{secondMachine : OracleTM secondTapes}
{compile : List Bool → List Bool → List Bool}
{firstOutput secondOutput : List Bool}
{firstTime secondTime jointTime firstBound secondBound combinedBound : ℕ}
(hcompose :
TimeBoundedProgramCompositionAt jointMachine firstMachine secondMachine compile firstOutput secondOutput firstTime
secondTime jointTime firstBound secondBound)
(hlength :
∀ (firstProgram secondProgram : List Bool),
firstProgram.length ≤ firstBound →
secondProgram.length ≤ secondBound → (compile firstProgram secondProgram).length ≤ combinedBound)
(hfirst : firstMachine.timeBoundedKolmogorovComplexity firstOutput firstTime ≤ ↑firstBound)
(hsecond :
secondMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity secondOutput firstOutput secondTime ≤ ↑secondBound)
:
jointMachine.timeBoundedKolmogorovComplexity (pair firstOutput secondOutput) jointTime ≤ ↑combinedBound
theorem
Complexity.timeBoundedKolmogorovComplexity_pair_le_of_pair_composition_internal
{jointTapes firstTapes secondTapes : ℕ}
{jointMachine : TM jointTapes}
{firstMachine : TM firstTapes}
{secondMachine : OracleTM secondTapes}
{firstOutput secondOutput : List Bool}
{firstTime secondTime jointTime firstBound secondBound : ℕ}
(hcompose :
TimeBoundedProgramCompositionAt jointMachine firstMachine secondMachine pair firstOutput secondOutput firstTime
secondTime jointTime firstBound secondBound)
(hfirst : firstMachine.timeBoundedKolmogorovComplexity firstOutput firstTime ≤ ↑firstBound)
(hsecond :
secondMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity secondOutput firstOutput secondTime ≤ ↑secondBound)
:
theorem
Complexity.timeBoundedKolmogorovComplexity_pair_le_of_reverse_pair_composition_internal
{jointTapes firstTapes secondTapes : ℕ}
{jointMachine : TM jointTapes}
{firstMachine : TM firstTapes}
{secondMachine : OracleTM secondTapes}
{firstOutput secondOutput : List Bool}
{firstTime secondTime jointTime firstBound secondBound : ℕ}
(hcompose :
TimeBoundedProgramCompositionAt jointMachine firstMachine secondMachine
(fun (firstProgram secondProgram : List Bool) => pair secondProgram firstProgram) firstOutput secondOutput firstTime
secondTime jointTime firstBound secondBound)
(hfirst : firstMachine.timeBoundedKolmogorovComplexity firstOutput firstTime ≤ ↑firstBound)
(hsecond :
secondMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity secondOutput firstOutput secondTime ≤ ↑secondBound)
:
theorem
Complexity.TimeBoundedConditionalPairCompositionAt.restrict_bounds_internal
{jointTapes conditionTapes resultTapes : ℕ}
{jointMachine : TM jointTapes}
{conditionMachine : TM conditionTapes}
{resultMachine : OracleTM resultTapes}
{compile : List Bool → List Bool → List Bool}
{result condition : List Bool}
{conditionTime resultTime jointTime conditionBound resultBound : ℕ}
(hcompose :
TimeBoundedConditionalPairCompositionAt jointMachine conditionMachine resultMachine compile result condition
conditionTime resultTime jointTime conditionBound resultBound)
{smallerConditionBound smallerResultBound : ℕ}
(hcondition : smallerConditionBound ≤ conditionBound)
(hresult : smallerResultBound ≤ resultBound)
:
TimeBoundedConditionalPairCompositionAt jointMachine conditionMachine resultMachine compile result condition
conditionTime resultTime jointTime smallerConditionBound smallerResultBound
theorem
Complexity.TimeBoundedConditionalPairCompositionAt.mono_jointTime_internal
{jointTapes conditionTapes resultTapes : ℕ}
{jointMachine : TM jointTapes}
{conditionMachine : TM conditionTapes}
{resultMachine : OracleTM resultTapes}
{compile : List Bool → List Bool → List Bool}
{result condition : List Bool}
{conditionTime resultTime firstJointTime secondJointTime conditionBound resultBound : ℕ}
(hcompose :
TimeBoundedConditionalPairCompositionAt jointMachine conditionMachine resultMachine compile result condition
conditionTime resultTime firstJointTime conditionBound resultBound)
(hjoint : firstJointTime ≤ secondJointTime)
:
TimeBoundedConditionalPairCompositionAt jointMachine conditionMachine resultMachine compile result condition
conditionTime resultTime secondJointTime conditionBound resultBound
theorem
Complexity.timeBoundedKolmogorovComplexity_pair_le_add_of_conditional_composition_internal
{jointTapes conditionTapes resultTapes : ℕ}
{jointMachine : TM jointTapes}
{conditionMachine : TM conditionTapes}
{resultMachine : OracleTM resultTapes}
{compile : List Bool → List Bool → List Bool}
{result condition : List Bool}
{conditionTime resultTime jointTime conditionBound resultBound constant : ℕ}
(hcompose :
TimeBoundedConditionalPairCompositionAt jointMachine conditionMachine resultMachine compile result condition
conditionTime resultTime jointTime conditionBound resultBound)
(hlength :
∀ (conditionProgram resultProgram : List Bool),
conditionProgram.length ≤ conditionBound →
resultProgram.length ≤ resultBound →
(compile conditionProgram resultProgram).length ≤ resultProgram.length + conditionProgram.length + constant)
(hconditionFinite : conditionMachine.timeBoundedKolmogorovComplexity condition conditionTime ≠ ⊤)
(hresultFinite : resultMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity result condition resultTime ≠ ⊤)
(hconditionBound : conditionMachine.timeBoundedKolmogorovComplexity condition conditionTime ≤ ↑conditionBound)
(hresultBound :
resultMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity result condition resultTime ≤ ↑resultBound)
:
jointMachine.timeBoundedKolmogorovComplexity (pair result condition) jointTime ≤ resultMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity result condition resultTime + conditionMachine.timeBoundedKolmogorovComplexity condition conditionTime + ↑constant