Counting one-way summary states

Binary occurrences cost one bit; special occurrences cost the logarithm of their actual register cardinality. The count has no guessed-output-bit factor.

def Algebraic.Aggregate.Capacity.registerBits {J : Type} {State : J → Type} [(j : J) → Fintype (State j)] (op : Op State) : ℕ

The register capacity of a single operation.

Equations

• Algebraic.Aggregate.Capacity.registerBits op = if op.isSpecial = true then Nat.clog 2 (Fintype.card op.Register) else 1

theorem Algebraic.Aggregate.Capacity.card_summaryRegister_le {J : Type} {State : J → Type} [(j : J) → Fintype (State j)] (op : Op State) : Fintype.card (SummaryRegister op) ≤ 2 ^ registerBits op

The finite summary register fits in its charged number of bits.

theorem Algebraic.Aggregate.Capacity.sum_registerBits_eq_capacity {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : ∑ gate : Fin g, registerBits (p.lines gate).op = capacity p

The gatewise bit sum is the ordinary count plus the actual special-register costs.

theorem Algebraic.Aggregate.Capacity.card_key_le {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Fintype.card (Key p) ≤ 2 ^ capacity p

The one-way key space has at most 2 ^ capacity p elements.

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

A uniform bound on every register charges at most bits per gate.

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

Uniform state cardinalities give a uniform gatewise capacity bound.