Positive rational exponent scales -- definitions

Quantitative metacomplexity theorems use expressions such as 2^(beta*n) and N^(1+epsilon), although circuit sizes and clocks are natural numbers. This module represents a positive rational scale by an explicit numerator and denominator, with separate floor and ceiling multiplication. It thereby keeps rounding choices visible and avoids real-valued resource bounds.

structure Complexity.PositiveRationalScale : Type

An explicit positive rational scale numerator / denominator.

No coprimality condition is imposed: unreduced presentations are useful when a proof needs to retain the constants appearing in a source theorem.

• numerator : ℕ

  Positive numerator of the scale.

• denominator : ℕ

  Positive denominator of the scale.

• numerator_pos : 0 < self.numerator

  The numerator is nonzero.

• denominator_pos : 0 < self.denominator

  The denominator is nonzero.

def Complexity.PositiveRationalScale.value (scale : PositiveRationalScale) : ℚ

The rational value represented by a positive scale.

Different unreduced numerator/denominator pairs may have the same value. The induced order is therefore intentionally a preorder rather than a partial order.

Equations

• scale.value = ↑scale.numerator / ↑scale.denominator

@[instance_reducible]

instance Complexity.PositiveRationalScale.instPreorder : Preorder PositiveRationalScale

Compare positive scales by their represented rational values.

Equations

• Complexity.PositiveRationalScale.instPreorder = Preorder.lift Complexity.PositiveRationalScale.value

def Complexity.PositiveRationalScale.atZeroFromPositive : Filter PositiveRationalScale

The filter of positive rational scales approaching zero from above.

Because zero itself is excluded structurally, atBot for the value preorder is exactly the small-positive-parameter convention used in magnification statements.

Equations

• Complexity.PositiveRationalScale.atZeroFromPositive = Filter.atBot

def Complexity.PositiveRationalScale.floorMul (scale : PositiveRationalScale) (n : ℕ) : ℕ

Floor of scale * n, computed entirely in natural numbers.

Equations

• scale.floorMul n = scale.numerator * n / scale.denominator

def Complexity.PositiveRationalScale.ceilMul (scale : PositiveRationalScale) (n : ℕ) : ℕ

Ceiling of scale * n, computed entirely in natural numbers.

Equations

• scale.ceilMul n = scale.numerator * n ⌈/⌉ scale.denominator

def Complexity.PositiveRationalScale.powFloor (scale : PositiveRationalScale) (n : ℕ) : ℕ

The rounded-down binary exponential 2^floor(scale*n).

Equations

• scale.powFloor n = 2 ^ scale.floorMul n

def Complexity.PositiveRationalScale.powCeil (scale : PositiveRationalScale) (n : ℕ) : ℕ

The rounded-up binary exponential 2^ceil(scale*n).

Equations

• scale.powCeil n = 2 ^ scale.ceilMul n

def Complexity.PositiveRationalScale.onePlusCeilExponent (scale : PositiveRationalScale) (n : ℕ) : ℕ

Natural exponent representing (2^n)^(1+scale) with the fractional term rounded upward.

Equations

• scale.onePlusCeilExponent n = n + scale.ceilMul n

def Complexity.PositiveRationalScale.onePlusCeilPow (scale : PositiveRationalScale) (n : ℕ) : ℕ

Slightly-superlinear bound at raw truth-table arity n.

Equations

• scale.onePlusCeilPow n = 2 ^ scale.onePlusCeilExponent n

def Complexity.PositiveRationalScale.onePlusCeilPowAtLength (scale : PositiveRationalScale) (inputLength : ℕ) : ℕ

Slightly-superlinear bound as a function of raw input length.

The intended domain is power-of-two lengths. Other lengths receive a total value through base-two logarithm but will lie outside the raw MCSP promise.

Equations

• scale.onePlusCeilPowAtLength inputLength = scale.onePlusCeilPow (Nat.log 2 inputLength)