Time-bounded symmetry of information -- proof internals #
theorem
Complexity.TimeBoundedSymmetryOfInformation.conditional_ne_top_internal
{ordinaryTapes conditionalTapes : ℕ}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{clock loss : ℕ → ℕ}
(hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock loss)
{first condition : List Bool}
{time : ℕ}
(hsize : first.length + condition.length ≤ time)
(hpair : ordinaryMachine.timeBoundedKolmogorovComplexity (pair first condition) time ≠ ⊤)
:
conditionalMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition (clock time) ≠ ⊤
theorem
Complexity.TimeBoundedSymmetryOfInformation.condition_ne_top_internal
{ordinaryTapes conditionalTapes : ℕ}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{clock loss : ℕ → ℕ}
(hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock loss)
{first condition : List Bool}
{time : ℕ}
(hsize : first.length + condition.length ≤ time)
(hpair : ordinaryMachine.timeBoundedKolmogorovComplexity (pair first condition) time ≠ ⊤)
:
theorem
Complexity.TimeBoundedSymmetryOfInformation.weaken_loss_internal
{ordinaryTapes conditionalTapes : ℕ}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{clock firstLoss secondLoss : ℕ → ℕ}
(hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock firstLoss)
(hloss : ∀ (time : ℕ), firstLoss time ≤ secondLoss time)
:
TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock secondLoss
theorem
Complexity.TimeBoundedSymmetryOfInformation.weaken_clock_internal
{ordinaryTapes conditionalTapes : ℕ}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{firstClock secondClock loss : ℕ → ℕ}
(hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine firstClock loss)
(hclock : ∀ (time : ℕ), firstClock time ≤ secondClock time)
:
TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine secondClock loss
theorem
Complexity.TimeBoundedSymmetryOfInformation.conditional_le_of_pair_upper_internal
{ordinaryTapes conditionalTapes alternativeTapes : ℕ}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{alternativeMachine : OracleTM alternativeTapes}
{clock loss : ℕ → ℕ}
(hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock loss)
{first condition : List Bool}
{time conditionTime alternativeTime upperLoss : ℕ}
(hsize : first.length + condition.length ≤ time)
(hclock : conditionTime ≤ clock time)
(hpairUpper :
ordinaryMachine.timeBoundedKolmogorovComplexity (pair first condition) time ≤ alternativeMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition alternativeTime + ordinaryMachine.timeBoundedKolmogorovComplexity condition conditionTime + ↑upperLoss)
:
conditionalMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition (clock time) ≤ alternativeMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition alternativeTime + ordinaryMachine.computationalDepthBetween condition conditionTime (clock time) + ↑upperLoss + ↑(loss time)
theorem
Complexity.TimeBoundedSymmetryOfInformation.conditional_le_of_composition_internal
{ordinaryTapes conditionalTapes alternativeTapes : ℕ}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
{alternativeMachine : OracleTM alternativeTapes}
{compile : List Bool → List Bool → List Bool}
{clock loss : ℕ → ℕ}
(hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock loss)
{first condition : List Bool}
{time conditionTime alternativeTime conditionBound alternativeBound constant : ℕ}
(hsize : first.length + condition.length ≤ time)
(hclock : conditionTime ≤ clock time)
(hcompose :
TimeBoundedConditionalPairCompositionAt ordinaryMachine ordinaryMachine alternativeMachine compile first condition
conditionTime alternativeTime time conditionBound alternativeBound)
(hlength :
∀ (conditionProgram alternativeProgram : List Bool),
conditionProgram.length ≤ conditionBound →
alternativeProgram.length ≤ alternativeBound →
(compile conditionProgram alternativeProgram).length ≤ alternativeProgram.length + conditionProgram.length + constant)
(hconditionFinite : ordinaryMachine.timeBoundedKolmogorovComplexity condition conditionTime ≠ ⊤)
(halternativeFinite :
alternativeMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition alternativeTime ≠ ⊤)
(hconditionBound : ordinaryMachine.timeBoundedKolmogorovComplexity condition conditionTime ≤ ↑conditionBound)
(halternativeBound :
alternativeMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition alternativeTime ≤ ↑alternativeBound)
:
conditionalMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition (clock time) ≤ alternativeMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition alternativeTime + ordinaryMachine.computationalDepthBetween condition conditionTime (clock time) + ↑constant + ↑(loss time)
theorem
Complexity.PolynomialTimeBoundedSymmetryOfInformation.enlarge_clock_internal
{ordinaryTapes conditionalTapes : ℕ}
{ordinaryMachine : TM ordinaryTapes}
{conditionalMachine : OracleTM conditionalTapes}
(hsoi : PolynomialTimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine)
{largerClock : ℕ → ℕ}
(hlargerAdmissible : IsAdmissibleKolmogorovClock largerClock)
(hlarger :
∀ (clock : ℕ → ℕ) (additive : ℕ),
IsAdmissibleKolmogorovClock clock →
(TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine clock fun (time : ℕ) =>
Nat.log 2 (clock time) + additive) →
∀ (time : ℕ), clock time ≤ largerClock time)
:
IsAdmissibleKolmogorovClock largerClock ∧ ∃ (additive : ℕ),
TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine largerClock fun (time : ℕ) =>
Nat.log 2 (largerClock time) + additive