Documentation

Complexitylib.Metacomplexity.MINCKT.Gap.Difference.Defs

Difference estimators for conditional gap MinKT -- definitions #

Hirahara's Proposition 6.2 estimates conditional complexity by subtracting an estimate for the condition from an estimate for the joint string, together with a logarithmic centering correction. This module isolates the numerical shape

B = minuend - subtrahend - correction

from the later construction of those components.

SatisfiesAccounting states the two inequalities before cancellation. Its proof layer shows that natural truncated subtraction is sound under precisely those inequalities and produces the GapMINCKT.Estimator.SatisfiesBounds sandwich required by the promise solver.

source
structure Complexity.GapMINCKT.DifferenceEstimator :
Type

Three numerical components of a threshold-free conditional estimator.

  • minuend : MINCKT.Instance → ℕ

    Joint-string estimate, the minuend of the difference.

  • subtrahend : MINCKT.Instance → ℕ

    Condition-only estimate subtracted from the joint estimate.

  • correction : MINCKT.Instance → ℕ

    Explicit centering/rounding correction subtracted last.

Instances For
    source
    def Complexity.GapMINCKT.DifferenceEstimator.estimate (components : DifferenceEstimator) :
    Estimator

    The natural-valued adjusted difference used as a conditional estimate.

    Equations
    Instances For
      source
      structure Complexity.GapMINCKT.DifferenceEstimator.SatisfiesAccounting {ordinaryTapes conditionalTapes : ℕ} (components : DifferenceEstimator) (ordinaryMachine : TM ordinaryTapes) (conditionalMachine : OracleTM conditionalTapes) (parameters : Parameters) :
      Prop

      The two pre-cancellation inequalities needed to validate the adjusted difference.

      The upper inequality leaves the subtrahend and correction on the right of the desired source-complexity bound. The lower inequality leaves the same terms on the left of the transformed-complexity bound. Cancellation then yields exactly the conditional estimator sandwich.

      Instances For