Exact real-valued aggregate capacity

The logarithm of the joint key cardinality charges the real logarithm of each register size. It incurs no per-register rounding or guessed-output-bit cost.

instance Algebraic.Aggregate.Capacity.instNonemptySummaryRegisterOfCommMonoid {J : Type} {State : J → Type} [(j : J) → CommMonoid (State j)] (op : Op State) : Nonempty (SummaryRegister op)

noncomputable def Algebraic.Aggregate.Capacity.realCapacity {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : ℝ

Exact bit capacity, without rounding the logarithms of register sizes.

Equations

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

theorem Algebraic.Aggregate.Capacity.card_summaryRegister_eq {J : Type} {State : J → Type} [(j : J) → Fintype (State j)] (op : Op State) : Fintype.card (SummaryRegister op) = if op.isSpecial = true then Fintype.card op.Register else 2

Binary summary registers have two states; special ones retain their original register.

theorem Algebraic.Aggregate.Capacity.card_key_eq {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Fintype.card (Key p) = 2 ^ ordinaryCount p * Fintype.card (Registers p)

The joint summary cardinality is the exact product of all charged register sizes.

theorem Algebraic.Aggregate.Capacity.logb_card_key_eq_realCapacity {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : Real.logb 2 ↑(Fintype.card (Key p)) = realCapacity p

The unrounded capacity is exactly the base-two logarithm of the key space.

theorem Algebraic.Aggregate.Capacity.realCapacity_le_of_register_card {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → CommMonoid (State j)] [(j : J) → Fintype (State j)] (p : Program (signature State) n g) (states : ℕ) (hs : 2 ≤ states) (h : ∀ (gate : SpecialGate p), Fintype.card (Register p gate) ≤ states) : realCapacity p ≤ ↑g * Real.logb 2 ↑states

Bounding all special registers by states bounds exact capacity per gate.

theorem Algebraic.Aggregate.Capacity.realCapacity_le_capacity {J : Type} {State : J → Type} {n g : ℕ} [(j : J) → Fintype (State j)] (p : Program (signature State) n g) : realCapacity p ≤ ↑(capacity p)

Rounding each register logarithm can only increase the exact joint capacity.