Counting the actual guesses and register states

Operation symbols and their fan-in do not enter these counts. Each special occurrence contributes one guessed bit and one finite register.

def Algebraic.Aggregate.ordinaryCount {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : ℕ

The ordinary gate count of the mixed program.

Equations

• Algebraic.Aggregate.ordinaryCount p = g - Algebraic.Aggregate.specialCount p

theorem Algebraic.Aggregate.specialCount_le {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : specialCount p ≤ g

theorem Algebraic.Aggregate.ordinaryCount_add_specialCount {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : ordinaryCount p + specialCount p = g

theorem Algebraic.Aggregate.card_filter_ordinary {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : {gate : Fin g | Op.isSpecial (p.lines gate).op = false}.card = ordinaryCount p

The ordinary gate count also counts the binary-operation filter.

theorem Algebraic.Aggregate.card_guess {J : Type} {State : J → Type} {n g : ℕ} (p : Program (signature State) n g) : Fintype.card (Guess p) = 2 ^ specialCount p

theorem Algebraic.Aggregate.card_registers {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Fintype.card (Registers p) = ∏ gate : SpecialGate p, Fintype.card (Register p gate)

theorem Algebraic.Aggregate.card_registers_le {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Fintype.card (Registers p) ≤ 2 ^ ∑ gate : SpecialGate p, Nat.clog 2 (Fintype.card (Register p gate))

theorem Algebraic.Aggregate.card_componentKey_le {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Fintype.card (Guess p × Registers p) ≤ 2 ^ budget p

The component-cover key space has at most 2 ^ budget p elements.

theorem Algebraic.Aggregate.budget_le_of_register_bits {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) (bits : ℕ) (h : ∀ (gate : SpecialGate p), Nat.clog 2 (Fintype.card (Register p gate)) ≤ bits) : budget p ≤ (bits + 1) * specialCount p

Uniform register bit bounds turn the actual-occurrence budget into a gate-count bound.

theorem Algebraic.Aggregate.budget_le_of_register_card {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) (bits : ℕ) (h : ∀ (gate : SpecialGate p), Fintype.card (Register p gate) ≤ 2 ^ bits) : budget p ≤ (bits + 1) * specialCount p

A uniform state-count bound supplies the corresponding register bit bound.