Building the conditional difference estimator from one ordinary estimator #
One unconditional Fact 3.4 estimator is queried on a paired string and on its
condition. Under the explicit clock/loss compatibility contract, those two
queries instantiate every surrounding input of the SoI accounting theorem.
Consequently their adjusted difference satisfies the conditional estimator
sandwich and solves GapMINCKT.
The remaining construction obligations are concentrated in Compatible: a
concrete upper-chain evaluator, the paper's iterated clock identities and
dominations, and the finite logarithmic budget calculations.
The paired ordinary query contains the canonical pair.
The paired ordinary query uses the planned source clock.
The condition query contains exactly the condition string.
The condition query uses the planned source clock.
Every paired query belongs to the plan's exact estimator-query domain.
Every condition-only query belongs to the plan's exact estimator-query domain.
The induced minuend is one application of the ordinary estimator to the paired query.
The induced subtrahend is one application of the same estimator to the condition query.
The induced difference retains the plan's explicit correction.
An operational condition-first compiler with attained minima proves the
paired upper-chain field required by Compatible.
A valid unconditional estimator plus clock/loss compatibility instantiates all inputs surrounding the single SoI invocation.
Estimator correctness is needed only on the two ordinary queries issued by the plan, not on every possible MINKT instance.
Fully composed ordinary-estimator-plus-SoI construction of the conditional estimator sandwich.
Query-local ordinary estimator correctness suffices for the fully composed conditional estimator sandwich.
Thresholding the adjusted difference of two ordinary estimator queries solves the exact conditional gap promise.
If the induced threshold language is in P, the ordinary-estimator-plus-
SoI construction places the exact conditional gap promise in PromiseP.
Query-local ordinary estimator bounds and a polynomial-time induced
completion place the exact conditional gap promise in PromiseP.