Time-bounded symmetry of information -- definitions

Hirahara's time-bounded symmetry-of-information hypothesis has the lower-chain form

C_cond^{p(t)}(x | y) + C^{p(t)}(y) <= C^t(pair x y) + log p(t).

This layer makes the ordinary machine, random-access conditional machine, canonical pair codec, transformed clock, and loss function explicit. Because the machines are arbitrary rather than implicitly universal, the fixed-clock hypothesis also requires the joint bounded complexity to be finite. This prevents an incapable joint machine from satisfying the inequality vacuously through top.

structure Complexity.IsAdmissibleKolmogorovClock (clock : ℕ → ℕ) : Prop

A clock suitable for the polynomial time-bounded SoI package dominates the original clock and has a uniform polynomial upper bound.

• dominates (time : ℕ) : time ≤ clock time

  The transformed clock never gives less time than the source clock.

• polynomiallyBounded : ∃ (coefficient : ℕ) (exponent : ℕ), ∀ (time : ℕ), clock time ≤ coefficient * (time + 1) ^ exponent

  One power bound controls the transformed clock at every input.

structure Complexity.TimeBoundedSymmetryOfInformation {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (clock loss : ℕ → ℕ) : Prop

Machine-relative time-bounded symmetry of information for a fixed clock transform and loss. The first conjunct is a non-vacuity condition needed when the ordinary machine is not yet known to be universal.

• pairFinite (first condition : List Bool) (time : ℕ) : first.length + condition.length ≤ time → ordinaryMachine.timeBoundedKolmogorovComplexity (pair first condition) time ≠ ⊤

  Every admissible paired instance has a bounded description.

• chain_le (first condition : List Bool) (time : ℕ) : first.length + condition.length ≤ time → conditionalMachine.randomAccessConditionalTimeBoundedKolmogorovComplexity first condition (clock time) + ordinaryMachine.timeBoundedKolmogorovComplexity condition (clock time) ≤ ordinaryMachine.timeBoundedKolmogorovComplexity (pair first condition) time + ↑(loss time)

  The lower-chain inequality at the transformed clock.

def Complexity.PolynomialTimeBoundedSymmetryOfInformation {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) : Prop

The polynomial/logarithmic SoI package. An additive loss constant remains explicit because the machines and codecs are explicit; it cannot be hidden by silently changing the universal evaluator.

Equations

• One or more equations did not get rendered due to their size.