Explicit slack amplification for the conditional MinKT reduction

The literal fourfold clock identifies the final gap slack with log_2(p^4(t + |x| + |y|)), while the reduction must pay three logarithmic losses, the SoI additive constant, and the pair compiler. This module defines a larger final clock whose logarithm pays those terms by construction.

The enlargement remains a finite product of fixed polynomial clocks. Its polynomial-growth proof is kept separate from the finite loss accounting.

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.totalTime (outputLength conditionLength time : ℕ) : ℕ

The total source parameter t + |x| + |y|.

Equations

• Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.totalTime outputLength conditionLength time = time + outputLength + conditionLength

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.slackExponent (clock : ℕ → ℕ) (additive compilerLoss outputLength conditionLength time : ℕ) : ℕ

Exponent containing every logarithmic loss that the conditional estimator must pay. The + 1 terms make the clock total even at time zero.

Equations

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

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.finalClock (clock : ℕ → ℕ) (additive compilerLoss outputLength conditionLength time : ℕ) : ℕ

Slack-amplified final clock.

The power of two makes its logarithm at least slackExponent. The remaining factors ensure that it dominates both the fourfold query clock and the source time, including degenerate zero inputs.

Equations

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

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.parameters (clock : ℕ → ℕ) (additive compilerLoss : ℕ) : Parameters

Conditional gap parameters using the slack-amplified final clock.

Equations

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

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.correction (clock : ℕ → ℕ) (compilerLoss : ℕ) (inst : MINCKT.Instance) : ℕ

The centering correction pays the condition-estimator loss and the fixed pair compiler loss exactly.

Equations

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

def Complexity.GapMINCKT.DifferenceEstimator.Unconditional.Iterated.Slack.plan (clock : ℕ → ℕ) (compilerLoss : ℕ) : Plan

Exact two-query plan with constant pair compiler loss and constructive centering correction.

Equations

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