Finite random restrictions

RandomRestriction.Seed N q is an exact finite product distribution. Each coordinate has one free symbol and q copies of each fixed Boolean value, so:

• the sample space has (2 * q + 1) ^ N equiprobable seeds;
• exactly one coordinate symbol decodes to none; and
• exactly q symbols decode to each fixed value.

Thus the free-coordinate probability is exactly 1 / (2 * q + 1). The API is stated in cardinality form so later switching arguments do not depend on rounding or division conventions.

theorem Complexity.RandomRestriction.card_seed (N q : ℕ) : Fintype.card (Seed N q) = (2 * q + 1) ^ N

The exact cardinality of the sparse-restriction sample space.

theorem Complexity.RandomRestriction.card_decodeSymbol_none (q : ℕ) : {symbol : Symbol q | decodeSymbol symbol = none}.card = 1

There is exactly one free symbol at each coordinate.

theorem Complexity.RandomRestriction.eventCount_coordinate_free {N : ℕ} (q : ℕ) (index : Fin N) : (eventCount q fun (restriction : Restriction.On N) => restriction index = none) = (2 * q + 1) ^ (N - 1)

Exactly (2q + 1)^(N - 1) seeds leave one prescribed input coordinate free.

theorem Complexity.RandomRestriction.card_decodeSymbol_some (q : ℕ) (value : Bool) : {symbol : Symbol q | decodeSymbol symbol = some value}.card = q

Each fixed Boolean value has exactly q equiprobable symbols.

theorem Complexity.RandomRestriction.decodeSymbol_eq_none_iff {q : ℕ} (symbol : Symbol q) : decodeSymbol symbol = none ↔ symbol = Sum.inl ()

A coordinate is free exactly when its seed symbol is the distinguished left-summand value.

theorem Complexity.RandomRestriction.eventCount_le {N q : ℕ} (event : Restriction.On N → Prop) [DecidablePred event] : eventCount q event ≤ (2 * q + 1) ^ N

Every event count is bounded by the total number of seeds.

theorem Complexity.RandomRestriction.eventCount_true (N q : ℕ) : (eventCount q fun (x : Restriction.On N) => True) = (2 * q + 1) ^ N

The certain event has the full sample-space cardinality.

theorem Complexity.RandomRestriction.eventCount_congr {N q : ℕ} (left right : Restriction.On N → Prop) [DecidablePred left] [DecidablePred right] (hiff : ∀ (restriction : Restriction.On N), left restriction ↔ right restriction) : eventCount q left = eventCount q right

Extensionally equal restriction events have equal counts.

theorem Complexity.RandomRestriction.eventCount_mono {N q : ℕ} (left right : Restriction.On N → Prop) [DecidablePred left] [DecidablePred right] (himp : ∀ (restriction : Restriction.On N), left restriction → right restriction) : eventCount q left ≤ eventCount q right

Inclusion of finite restriction events implies monotonicity of their counts.

theorem Complexity.RandomRestriction.eventCount_or_le_add {N q : ℕ} (left right : Restriction.On N → Prop) [DecidablePred left] [DecidablePred right] : (eventCount q fun (restriction : Restriction.On N) => left restriction ∨ right restriction) ≤ eventCount q left + eventCount q right

The count of a union of two restriction events is at most the sum of their counts.

theorem Complexity.RandomRestriction.eventCount_exists_le_sum {N q : ℕ} {ι : Type} [Fintype ι] (event : ι → Restriction.On N → Prop) [(index : ι) → DecidablePred (event index)] : (eventCount q fun (restriction : Restriction.On N) => ∃ (index : ι), event index restriction) ≤ ∑ index : ι, eventCount q (event index)

Finite union bound for restriction events, stated directly in exact cardinality form.

theorem Complexity.RandomRestriction.card_eventSeed {N q : ℕ} (event : Restriction.On N → Prop) [DecidablePred event] : Fintype.card (EventSeed N q event) = eventCount q event

The event-seed subtype has exactly the event count as its cardinality.

theorem Complexity.RandomRestriction.eventCount_freeVariables_empty (N q : ℕ) : (eventCount q fun (restriction : Restriction.On N) => restriction.freeVariables = ∅) = (2 * q) ^ N

Exactly (2 * q) ^ N seeds fix every input coordinate.

theorem Complexity.RandomRestriction.eventCount_freeVariables_nonempty (N q : ℕ) : (eventCount q fun (restriction : Restriction.On N) => restriction.freeVariables.Nonempty) = (2 * q + 1) ^ N - (2 * q) ^ N

The number of seeds leaving at least one coordinate free is the total sample-space size minus the number of all-fixed seeds.

theorem Complexity.RandomRestriction.eventCount_one_le_freeVariables (N q : ℕ) : (eventCount q fun (restriction : Restriction.On N) => 1 ≤ restriction.freeVariables.card) = (2 * q + 1) ^ N - (2 * q) ^ N

Cardinality form of the exact probability that at least one coordinate survives the sparse restriction.

theorem Complexity.RandomRestriction.eventCount_mul_pow_le_of_encoding {N q : ℕ} (event : Restriction.On N → Prop) [DecidablePred event] (queryCount : ℕ) (Code : Type) [Fintype Code] (encode : EventSeed N q event × (Fin queryCount → Fin q) → Seed N q × Code) (injective : Function.Injective encode) : eventCount q event * q ^ queryCount ≤ (2 * q + 1) ^ N * Fintype.card Code

Generic finite encoding bound used by switching arguments.

An injection that assigns every bad seed and every queryCount-tuple of q copy labels to an arbitrary seed plus a finite auxiliary code proves the displayed amplified counting inequality. No probability division or positivity side condition is hidden in the statement.

theorem Complexity.RandomRestriction.positionOf_apply {s N : ℕ} (queries : Fin s ↪ Fin N) (position : Fin s) : positionOf queries (queries position) = some position

Looking up an embedded coordinate recovers its unique position.

theorem Complexity.RandomRestriction.assignmentAlong_disjoint {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (values : Fin s → Bool) (free : ∀ (position : Fin s), decode seed (queries position) = none) (index : Fin N) : assignmentAlong queries values index = none ∨ decode seed index = none

The assignment supported on queries is disjoint from any restriction under which every queried coordinate is free.

@[simp]

theorem Complexity.RandomRestriction.assignmentAlong_apply {s N : ℕ} (queries : Fin s ↪ Fin N) (values : Fin s → Bool) (position : Fin s) : assignmentAlong queries values (queries position) = some (values position)

The partial assignment supported on queries has the prescribed value at every selected coordinate.

theorem Complexity.RandomRestriction.decode_fixAlong {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (copies : Fin s → Fin q) (values : Fin s → Bool) : decode (fixAlong seed queries copies values) = (assignmentAlong queries values).comp (decode seed)

Fixing selected seed coordinates composes the decoded restriction with the corresponding finite partial assignment.

@[simp]

theorem Complexity.RandomRestriction.fixAlong_apply {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (copies : Fin s → Fin q) (values : Fin s → Bool) (position : Fin s) : fixAlong seed queries copies values (queries position) = Sum.inr (copies position, values position)

@[simp]

theorem Complexity.RandomRestriction.freeAlong_apply {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (position : Fin s) : freeAlong seed queries (queries position) = Sum.inl ()

theorem Complexity.RandomRestriction.freeAlong_fixAlong {N q s : ℕ} (seed : Seed N q) (queries : Fin s ↪ Fin N) (copies : Fin s → Fin q) (values : Fin s → Bool) (free : ∀ (position : Fin s), seed (queries position) = Sum.inl ()) : freeAlong (fixAlong seed queries copies values) queries = seed

Fixing formerly-free embedded coordinates and then freeing them recovers the original seed.

@[simp]

theorem Complexity.RandomRestriction.mem_freeVariables {N q : ℕ} (seed : Seed N q) (index : Fin N) : index ∈ freeVariables seed ↔ decode seed index = none