SoI accounting for conditional-complexity difference estimators

This module composes a time-bounded symmetry-of-information hypothesis with explicit joint/condition estimator bounds and finite loss budgets. The result is the pre-cancellation accounting contract for the adjusted-difference estimator, hence the full GapMINCKT estimator sandwich, solver, and PromiseP completion criterion.

Every clock equality and loss allocation remains visible in SatisfiesSoIInputs; this theorem does not assume that a concrete universal estimator or its polynomial-time implementation has already been built.

theorem Complexity.GapMINCKT.DifferenceEstimator.SatisfiesSoIInputs.satisfiesAccounting {ordinaryTapes conditionalTapes : ℕ} {components : DifferenceEstimator} {schedule : SoIAccountingSchedule} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {soiClock soiLoss : ℕ → ℕ} (hinputs : components.SatisfiesSoIInputs schedule ordinaryMachine conditionalMachine parameters soiClock soiLoss) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine soiClock soiLoss) (hwidening : parameters.IsWidening) : components.SatisfiesAccounting ordinaryMachine conditionalMachine parameters

SoI and the surrounding estimator inequalities imply both pre-cancellation accounting bounds.

theorem Complexity.GapMINCKT.DifferenceEstimator.SatisfiesSoIInputs.satisfiesBounds {ordinaryTapes conditionalTapes : ℕ} {components : DifferenceEstimator} {schedule : SoIAccountingSchedule} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {soiClock soiLoss : ℕ → ℕ} (hinputs : components.SatisfiesSoIInputs schedule ordinaryMachine conditionalMachine parameters soiClock soiLoss) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine soiClock soiLoss) (hwidening : parameters.IsWidening) : components.estimate.SatisfiesBounds ordinaryMachine conditionalMachine parameters

Fully composed SoI-to-estimator theorem.

theorem Complexity.GapMINCKT.DifferenceEstimator.SatisfiesSoIInputs.solvedBy {ordinaryTapes conditionalTapes : ℕ} {components : DifferenceEstimator} {schedule : SoIAccountingSchedule} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {soiClock soiLoss : ℕ → ℕ} (hinputs : components.SatisfiesSoIInputs schedule ordinaryMachine conditionalMachine parameters soiClock soiLoss) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine soiClock soiLoss) (hwidening : parameters.IsWidening) : (GapMINCKT ordinaryMachine conditionalMachine parameters hwidening).SolvedBy (decisionOfEstimator components.estimate)

Thresholding the SoI-certified adjusted difference solves the exact conditional gap promise.

theorem Complexity.GapMINCKT.DifferenceEstimator.SatisfiesSoIInputs.mem_PromiseP {ordinaryTapes conditionalTapes : ℕ} {components : DifferenceEstimator} {schedule : SoIAccountingSchedule} {ordinaryMachine : TM ordinaryTapes} {conditionalMachine : OracleTM conditionalTapes} {parameters : Parameters} {soiClock soiLoss : ℕ → ℕ} (hinputs : components.SatisfiesSoIInputs schedule ordinaryMachine conditionalMachine parameters soiClock soiLoss) (hsoi : TimeBoundedSymmetryOfInformation ordinaryMachine conditionalMachine soiClock soiLoss) (hwidening : parameters.IsWidening) (hpolynomial : estimatorLanguage components.estimate ∈ P) : GapMINCKT ordinaryMachine conditionalMachine parameters hwidening ∈ PromiseP

A polynomial-time threshold language for the SoI-certified difference is a PromiseP completion of GapMINCKT.