Difference estimators for conditional gap MinKT -- proof internals

theorem Complexity.GapMINCKT.DifferenceEstimator.estimate_apply_internal (components : DifferenceEstimator) (inst : MINCKT.Instance) : components.estimate inst = components.minuend inst - components.subtrahend inst - components.correction inst

theorem Complexity.GapMINCKT.DifferenceEstimator.SatisfiesAccounting.satisfiesBounds_internal {ordinaryTapes conditionalTapes : ℕ} {components : DifferenceEstimator} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} (haccounting : components.SatisfiesAccounting ordinaryMachine conditionalMachine parameters) : components.estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters