Exact statements of Boolean mass production

This module fixes the circuit model and quantifiers used by the Boolean mass-production manuscript. Rates are represented by natural fractions and the copy budget is 2 ^ floor (numerator * inputs / denominator). Keeping the finite statement discrete avoids hiding real-number rounding in the circuit theorem.

MassProductionBound is the bound at one input width and one constant. MassProducesAt quantifies it eventually over the input width, while MassProducesAtAllLengths requires it at every positive input width.

noncomputable def Algebraic.MassProduction.booleanMassComplexity {inputs : ℕ} (function : ScalarFunction Bool inputs) (copies : ℕ) : ℕ∞

Minimum standard De Morgan cost of independently evaluating one Boolean function on copies row-major input blocks.

Equations

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

def Algebraic.MassProduction.rationalCopyBudget (numerator denominator inputs : ℕ) : ℕ

The discrete copy budget at rational exponent numerator / denominator. Natural division is deliberate: it implements the floor in the exponent.

Equations

• Algebraic.MassProduction.rationalCopyBudget numerator denominator inputs = 2 ^ (numerator * inputs / denominator)

theorem Algebraic.MassProduction.rationalCopyBudget_mono_numerator {small large denominator inputs : ℕ} (numeratorBound : small ≤ large) : rationalCopyBudget small denominator inputs ≤ rationalCopyBudget large denominator inputs

Increasing the exponent numerator can only increase the copy budget.

theorem Algebraic.MassProduction.rationalCopyBudget_mono_inputs {numerator denominator small large : ℕ} (inputsBound : small ≤ large) : rationalCopyBudget numerator denominator small ≤ rationalCopyBudget numerator denominator large

Increasing the input width can only increase the copy budget.

def Algebraic.MassProduction.MassProductionBound (numerator denominator constant inputs : ℕ) : Prop

The uniform mass-production estimate at one input width.

Equations

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

theorem Algebraic.MassProduction.MassProductionBound.mono_numerator {small large denominator constant inputs : ℕ} (bound : MassProductionBound large denominator constant inputs) (numeratorBound : small ≤ large) : MassProductionBound small denominator constant inputs

Decreasing the allowed exponent numerator preserves a per-width mass production bound.

def Algebraic.MassProduction.MassProducesAt (numerator denominator : ℕ) : Prop

Eventual worst-case mass production at one rational exponent.

The constant and cutoff may depend on the fixed exponent, but not on the input length, function, or requested number of copies. Positivity is carried as an ordinary hypothesis rather than a typeclass instance.

Equations

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

def Algebraic.MassProduction.MassProducesAtAllLengths (numerator denominator : ℕ) : Prop

Every-positive-length version of mass production at one rational exponent. This is the direct discrete analogue of the manuscript's main theorem after the exponent is fixed.

Equations

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

def Algebraic.MassProduction.ExponentialMassProduction : Prop

The manuscript's exponential-range conclusion, in its exact rational and discrete form: every nonnegative rational exponent strictly below one has a uniform all-length mass-production bound.

Equations

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

theorem Algebraic.MassProduction.MassProducesAtAllLengths.eventually {numerator denominator : ℕ} (production : MassProducesAtAllLengths numerator denominator) : MassProducesAt numerator denominator

The all-length statement immediately implies its eventual counterpart.

theorem Algebraic.MassProduction.MassProducesAt.mono_numerator {small large denominator : ℕ} (production : MassProducesAt large denominator) (numeratorBound : small ≤ large) : MassProducesAt small denominator

Enlarging the allowed numerator weakens the eventual production statement.

theorem Algebraic.MassProduction.MassProducesAtAllLengths.mono_numerator {small large denominator : ℕ} (production : MassProducesAtAllLengths large denominator) (numeratorBound : small ≤ large) : MassProducesAtAllLengths small denominator

Enlarging the allowed numerator also weakens the all-length statement.