Documentation

Complexitylib.Metacomplexity.MINCKT.Gap.Multiplicative.Defs

Multiplicative-gap conditional MinKT -- definitions #

This is the exact machine-relative promise from Definition 6.5 of Hirahara's Symmetry of Information from Meta-Complexity. It retains the same depth-adjusted yes side as GapMINCKT, but replaces the no threshold by

sigma(|x|) * s + log_2(tau(|x|,|y|,t)).

The canonical (x,y,1^t,1^s) codec and trivariate clock parameters are reused verbatim. The factor is an explicit function of the output length.

source
def Complexity.GapMINCKT.Multiplicative.IsNo {conditionalTapes : ℕ} (inst : Instance) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) :
Prop

Definition 6.5's multiplicative no condition.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Complexity.GapMINCKT.Multiplicative.IsRelaxedWitness {conditionalTapes : ℕ} (inst : Instance) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) (program : List Bool) :
    Prop

    A concrete transformed-clock program forbidden by the multiplicative no condition.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Complexity.GapMINCKT.Multiplicative.yesLanguage {ordinaryTapes conditionalTapes : ℕ} (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) :
      Language

      Definition 6.5 has exactly the additive promise's depth-adjusted yes side.

      Equations
      Instances For
        source
        def Complexity.GapMINCKT.Multiplicative.noLanguage {conditionalTapes : ℕ} (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) (factor : ℕ → ℕ) :
        Language

        Canonically encoded multiplicative no language.

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