Approximate-selection round traces -- definitions

An extension estimator assigns an estimated survivor count to every possible next input at every sample prefix. This layer records bounded and global accuracy, together with the trace obtained by repeatedly choosing a minimum estimate.

def Complexity.AntiChecker.ApproximatesRoundsUpTo {arity : ℕ} (rounds precision : ℕ) (target : BitString arity → Bool) (threshold : ℕ) (estimator : List (BitString arity) → BitString arity → ℕ) : Prop

An extension estimator satisfies the relative survivor-count contract at every sample prefix shorter than the prescribed number of rounds.

Equations

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

def Complexity.AntiChecker.ApproximatesEveryRound {arity : ℕ} (precision : ℕ) (target : BitString arity → Bool) (threshold : ℕ) (estimator : List (BitString arity) → BitString arity → ℕ) : Prop

An extension estimator satisfies the relative survivor-count contract at every possible sample prefix.

Equations

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

def Complexity.AntiChecker.IsEstimateSelectionTrace {arity : ℕ} (estimator : List (BitString arity) → BitString arity → ℕ) : List (BitString arity) → Prop

Every input in the list, read from tail to head, minimizes the estimator relative to the prefix constructed before it.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.AntiChecker.IsEstimateSelectionTrace estimator [] = True