Finite counting toolkit

Exact cardinality lemmas for the finite sample space Fin T → Bool used by the probabilistic-machine semantics (NTM.acceptCount, NTM.acceptProb). These are the reusable combinatorial facts underlying randomized classes, amplification, and interactive proofs (roadmap track N2).

Main results

• card_finArrowBool — |Fin T → Bool| = 2 ^ T
• blockEquiv — the split of a length-a + b random string into its length-a prefix and length-b suffix, packaged as an Equiv (so the projection and concatenation maps are inverse by construction)
• card_filter_block — block independence: the count of seeds whose prefix and suffix satisfy given predicates is the product of the two counts
• card_filter_exists_le — the finite union bound: the number of sample points satisfying some predicate in a finite family is at most the sum of the per-predicate counts
• boolFunEquivFinset, card_filter_popCount_eq — Boolean vectors as true supports and their exact binomial weight counts
• finCountP_eq_popCount — the bridge from the dependency-light Fin.countP used by circuit encoders to finite-set support counting
• blocksEquiv, card_blockEventCount_eq — a long machine seed as independent blocks and the exact weighted binomial count for any block event
• repeatRandomSeed, card_repeatRandomSeed_fiber — extract the actual simulation slots from a fixed-time repetition seed and count its ignored administrative bits
• card_filter_of_constant_fibers — transfer an event count through a projection whose fibers all have the same power-of-two cardinality
• card_blockMajority_eq_false — the exact weighted lower-tail count for failure across an odd number of blocks
• blockEventCount_add_compl, blockMajority_compl_of_odd — event-complement symmetry for block counts and odd strict majorities
• card_majority_eq_true, card_majority_eq_false — exact binomial-tail counts for strict-majority success and failure
• majority_not_of_odd — strict majority is antisymmetric under pointwise negation at odd length

Cardinality of the random-bit sample space

theorem Complexity.card_finArrowBool (T : ℕ) : Fintype.card (Fin T → Bool) = 2 ^ T

The finite sample space of T random bits has 2 ^ T points. This is the denominator in NTM.acceptProb.

theorem Complexity.card_finArrowBool_add (a b : ℕ) : Fintype.card (Fin (a + b) → Bool) = 2 ^ a * 2 ^ b

Splitting T = a + b random bits multiplies the point counts.

theorem Complexity.card_boolFunc (n : ℕ) : Fintype.card ((Fin n → Bool) → Bool) = 2 ^ 2 ^ n

There are exactly 2 ^ (2 ^ n) Boolean functions on n bits — the number of distinct 2 ^ n-entry truth tables. The base fact for property density in natural-proofs arguments.

theorem Complexity.card_adjMatrix (n : ℕ) : Fintype.card (Fin n → Fin n → Bool) = 2 ^ (n * n)

There are exactly 2 ^ (n * n) directed graphs (adjacency matrices) on n vertices — the number of n × n Boolean matrices. The size datum behind adjacency-matrix encodings of graph languages such as CLIQUE.

def Complexity.adjMatrixEquivBitVec (n : ℕ) : (Fin n → Fin n → Bool) ≃ (Fin (n * n) → Bool)

An n-vertex adjacency matrix biject with n²-bit strings by row-major serialization. Packaging this as an Equiv gives a canonical encode (adjMatrixEquivBitVec) and decode (.symm) that are inverse by construction — the codec behind graph-language encodings.

Equations

• Complexity.adjMatrixEquivBitVec n = (Equiv.curry (Fin n) (Fin n) Bool).symm.trans (finProdFinEquiv.arrowCongr (Equiv.refl Bool))

Block projection and concatenation

def Complexity.blockEquiv (a b : ℕ) : (Fin (a + b) → Bool) ≃ (Fin a → Bool) × (Fin b → Bool)

A length-a + b random string is equivalently its length-a prefix paired with its length-b suffix. The forward map is the pair of projections; the inverse is concatenation. Packaging this as an Equiv proves the projection and concatenation maps are mutually inverse.

Equations

• Complexity.blockEquiv a b = (finSumFinEquiv.arrowCongr (Equiv.refl Bool)).symm.trans (Equiv.sumArrowEquivProdArrow (Fin a) (Fin b) Bool)

def Complexity.blockFst (a b : ℕ) (w : Fin (a + b) → Bool) : Fin a → Bool

The prefix projection of a length-a + b random string.

Equations

• Complexity.blockFst a b w = ((Complexity.blockEquiv a b) w).1

def Complexity.blockSnd (a b : ℕ) (w : Fin (a + b) → Bool) : Fin b → Bool

The suffix projection of a length-a + b random string.

Equations

• Complexity.blockSnd a b w = ((Complexity.blockEquiv a b) w).2

@[simp]

theorem Complexity.blockSnd_apply (a b : ℕ) (w : Fin (a + b) → Bool) (i : Fin b) : blockSnd a b w i = w (Fin.natAdd a i)

Suffix projection is restriction along the canonical shifted inclusion.

def Complexity.blockAppend (a b : ℕ) (u : Fin a → Bool) (v : Fin b → Bool) : Fin (a + b) → Bool

Concatenate a length-a prefix and length-b suffix into one random string.

Equations

• Complexity.blockAppend a b u v = (Complexity.blockEquiv a b).symm (u, v)

@[simp]

theorem Complexity.blockFst_append (a b : ℕ) (u : Fin a → Bool) (v : Fin b → Bool) : blockFst a b (blockAppend a b u v) = u

@[simp]

theorem Complexity.blockSnd_append (a b : ℕ) (u : Fin a → Bool) (v : Fin b → Bool) : blockSnd a b (blockAppend a b u v) = v

@[simp]

theorem Complexity.blockAppend_fst_snd (a b : ℕ) (w : Fin (a + b) → Bool) : blockAppend a b (blockFst a b w) (blockSnd a b w) = w

theorem Complexity.card_filter_block {a b : ℕ} (P : (Fin a → Bool) → Prop) (Q : (Fin b → Bool) → Prop) [DecidablePred P] [DecidablePred Q] : {w : Fin (a + b) → Bool | P (blockFst a b w) ∧ Q (blockSnd a b w)}.card = (Finset.filter P Finset.univ).card * (Finset.filter Q Finset.univ).card

Block independence (exact counting form). The number of length-a + b seeds whose prefix satisfies P and suffix satisfies Q is the product of the two individual counts. Because blockEquiv is a bijection onto the product sample space, the joint event factors — the exact-count statement of independence across blocks, and the combinatorial heart of relating a repeated machine's acceptance to its single-run acceptance (amplification, roadmap N2/M2).

Finite union bound

theorem Complexity.card_filter_exists_le {ι : Type u_1} {α : Type u_2} [Fintype α] [DecidableEq α] (s : Finset ι) (p : ι → α → Prop) [(i : ι) → DecidablePred (p i)] : {x : α | ∃ i ∈ s, p i x}.card ≤ ∑ i ∈ s, (Finset.filter (p i) Finset.univ).card

The finite union bound: the number of sample points satisfying some predicate p i for i in a finite index set s is at most the sum over s of the per-predicate counts. The workhorse behind failure-probability bounds over many bad events.

theorem Complexity.exists_good_seed {S : Type u_1} {ι : Type u_2} [Fintype S] [DecidableEq S] (inputs : Finset ι) (bad : ι → Finset S) (h : ∑ i ∈ inputs, (bad i).card < Fintype.card S) : ∃ (s : S), ∀ i ∈ inputs, s ∉ bad i

The probabilistic method: a perfect seed exists. If the total number of "bad" seeds summed over all inputs is strictly less than the number of seeds, then some single seed is good for every input simultaneously. This is the machine-independent counting core of BPP ⊆ P/poly (hardwiring one random string that works for all 2ⁿ inputs of a given length).

Majority

def Complexity.popCount {k : ℕ} (f : Fin k → Bool) : ℕ

The number of true positions of a Boolean vector.

Equations

• Complexity.popCount f = {i : Fin k | f i = true}.card

theorem Complexity.finCountP_eq_popCount {k : ℕ} (f : Fin k → Bool) : Fin.countP f = popCount f

Batteries' fold-based Boolean count agrees with the finite-set support count used by the randomized-counting layer.

def Complexity.boolFunEquivFinset (α : Type u_1) [Fintype α] [DecidableEq α] : (α → Bool) ≃ Finset α

Boolean-valued functions are equivalent to their true supports.

Equations

• Complexity.boolFunEquivFinset α = { toFun := fun (f : α → Bool) => {i : α | f i = true}, invFun := fun (s : Finset α) (i : α) => decide (i ∈ s), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Complexity.mem_boolFunEquivFinset {α : Type u_1} [Fintype α] [DecidableEq α] (f : α → Bool) (i : α) : i ∈ (boolFunEquivFinset α) f ↔ f i = true

@[simp]

theorem Complexity.boolFunEquivFinset_card {k : ℕ} (f : Fin k → Bool) : ((boolFunEquivFinset (Fin k)) f).card = popCount f

theorem Complexity.card_filter_popCount_eq (k r : ℕ) : {f : Fin k → Bool | popCount f = r}.card = k.choose r

Exactly k.choose r Boolean vectors of length k have r true entries.

theorem Complexity.card_filter_popCount_mem (k : ℕ) (s : Finset ℕ) : {f : Fin k → Bool | popCount f ∈ s}.card = ∑ r ∈ s, k.choose r

The number of vectors whose popCount lies in a finite set is the corresponding sum of binomial coefficients.

Weighted event counts across blocks

def Complexity.blocksEquiv (k T : ℕ) : (Fin (k * T) → Bool) ≃ (Fin k → Fin T → Bool)

A length-k * T seed is equivalently a sequence of k blocks of length T. The product equivalence fixes the row-major schedule consumed by repeated randomized computations.

Equations

• Complexity.blocksEquiv k T = (finProdFinEquiv.arrowCongr (Equiv.refl Bool)).symm.trans (Equiv.curry (Fin k) (Fin T) Bool)

@[simp]

theorem Complexity.blocksEquiv_apply (k T : ℕ) (w : Fin (k * T) → Bool) (i : Fin k) (t : Fin T) : (blocksEquiv k T) w i t = w (finProdFinEquiv (i, t))

@[simp]

theorem Complexity.blocksEquiv_symm_apply (k T : ℕ) (f : Fin k → Fin T → Bool) (p : Fin (k * T)) : (blocksEquiv k T).symm f p = f (finProdFinEquiv.symm p).1 (finProdFinEquiv.symm p).2

Fixed-time repetition schedules

def Complexity.repeatStrideIndexEquiv (k T : ℕ) : Fin (k * T) ⊕ Fin (k * (T + 2)) ≃ Fin (k * (2 * T + 2))

Split stride positions into simulation slots and administrative slots.

Equations

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

def Complexity.repeatStrideSeedEquiv (k T : ℕ) : (Fin (k * (2 * T + 2)) → Bool) ≃ (Fin (k * T) → Bool) × (Fin (k * (T + 2)) → Bool)

Split a full stride seed into simulation and administrative choices.

Equations

• Complexity.repeatStrideSeedEquiv k T = ((Complexity.repeatStrideIndexEquiv k T).arrowCongr (Equiv.refl Bool)).symm.trans (Equiv.sumArrowEquivProdArrow (Fin (k * T)) (Fin (k * (T + 2))) Bool)

def Complexity.repeatStrideRandomSeed (k T : ℕ) (w : Fin (k * (2 * T + 2)) → Bool) : Fin (k * T) → Bool

Project a repetition stride onto its k * T genuine simulation choices.

Equations

• Complexity.repeatStrideRandomSeed k T w = ((Complexity.repeatStrideSeedEquiv k T) w).1

def Complexity.repeatRandomSeed (k T : ℕ) (w : Fin (2 + k * (2 * T + 2)) → Bool) : Fin (k * T) → Bool

Extract the k * T genuinely random simulation choices from a repetition trace of length 2 + k * (2 * T + 2). The first two choices and the last T + 2 choices of every repetition stride are administrative and ignored.

Equations

• Complexity.repeatRandomSeed k T w = Complexity.repeatStrideRandomSeed k T (Complexity.blockSnd 2 (k * (2 * T + 2)) w)

theorem Complexity.repeatRandomSeed_apply (k T : ℕ) (w : Fin (2 + k * (2 * T + 2)) → Bool) (i : Fin k) (t : Fin T) : repeatRandomSeed k T w (finProdFinEquiv (i, t)) = w (Fin.natAdd 2 (finProdFinEquiv (i, Fin.castLE ⋯ t)))

The compact seed's (i,t) entry is the choice at simulation offset t in repetition stride i, after the two initial setup choices.

theorem Complexity.card_repeatRandomSeed_fiber (k T : ℕ) (seed : Fin (k * T) → Bool) : {w : Fin (2 + k * (2 * T + 2)) → Bool | repeatRandomSeed k T w = seed}.card = 2 ^ (2 + k * (T + 2))

Every compact repetition seed has exactly one freely chosen assignment to each administrative slot in its full-seed fiber.

theorem Complexity.card_filter_of_constant_fibers {total compact ignored : ℕ} (randomSeed : (Fin total → Bool) → Fin compact → Bool) (Accept : (Fin total → Bool) → Prop) (Good : (Fin compact → Bool) → Prop) [DecidablePred Accept] [DecidablePred Good] (hfactor : ∀ (w : Fin total → Bool), Accept w ↔ Good (randomSeed w)) (hfiber : ∀ (seed : Fin compact → Bool), {w : Fin total → Bool | randomSeed w = seed}.card = 2 ^ ignored) : (Finset.filter Accept Finset.univ).card = (Finset.filter Good Finset.univ).card * 2 ^ ignored

If a finite Boolean-seed projection has constant fibers, then every event that factors through the projection gains exactly that common fiber factor.

theorem Complexity.card_filter_repeatRandomSeed (k T : ℕ) (P : (Fin (k * T) → Bool) → Prop) [DecidablePred P] : {w : Fin (2 + k * (2 * T + 2)) → Bool | P (repeatRandomSeed k T w)}.card = (Finset.filter P Finset.univ).card * 2 ^ (2 + k * (T + 2))

An event depending only on the compact repetition seed has its count multiplied by the number of ignored administrative choice assignments.

def Complexity.blockEventCount {k T : ℕ} (E : Finset (Fin T → Bool)) (w : Fin (k * T) → Bool) : ℕ

The number of blocks of a long seed that lie in the event E.

Equations

• Complexity.blockEventCount E w = {i : Fin k | (Complexity.blocksEquiv k T) w i ∈ E}.card

theorem Complexity.blockEventCount_add_compl {k T : ℕ} (E : Finset (Fin T → Bool)) (w : Fin (k * T) → Bool) : blockEventCount E w + blockEventCount Eᶜ w = k

Every block lies in exactly one of an event and its complement.

theorem Complexity.card_blockEventCount_eq {T : ℕ} (E : Finset (Fin T → Bool)) (k j : ℕ) : {w : Fin (k * T) → Bool | blockEventCount E w = j}.card = k.choose j * E.card ^ j * (2 ^ T - E.card) ^ (k - j)

Weighted binomial count in the machine seed space. Exactly the stated binomial number of long seeds have j blocks in E; the two weights are the counts of successful and unsuccessful T-bit blocks.

def Complexity.blockMajority {k T : ℕ} (E : Finset (Fin T → Bool)) (w : Fin (k * T) → Bool) : Bool

Strict majority of the blocks of a long seed lying in the event E.

Equations

• Complexity.blockMajority E w = decide (2 * Complexity.blockEventCount E w > k)

theorem Complexity.blockMajority_compl_of_odd {k T : ℕ} (hk : Odd k) (E : Finset (Fin T → Bool)) (w : Fin (k * T) → Bool) : blockMajority Eᶜ w = !blockMajority E w

At an odd number of blocks, complementing the event flips the strict majority verdict.

theorem Complexity.blockMajority_eq_false_iff {k T : ℕ} (E : Finset (Fin T → Bool)) (w : Fin (k * T) → Bool) : blockMajority E w = false ↔ blockEventCount E w ≤ k / 2

theorem Complexity.blockMajority_eq_false_iff_mem_range {T r : ℕ} (E : Finset (Fin T → Bool)) (w : Fin ((2 * r + 1) * T) → Bool) : blockMajority E w = false ↔ blockEventCount E w ∈ Finset.range (r + 1)

theorem Complexity.card_blockMajority_eq_false (T r : ℕ) (E : Finset (Fin T → Bool)) : {w : Fin ((2 * r + 1) * T) → Bool | blockMajority E w = false}.card = ∑ j ∈ Finset.range (r + 1), (2 * r + 1).choose j * E.card ^ j * (2 ^ T - E.card) ^ (2 * r + 1 - j)

Exact odd-majority failure count. For 2r + 1 independent T-bit blocks, failure means at most r blocks lie in E; each summand is the corresponding weighted binomial fiber.

def Complexity.majority {k : ℕ} (f : Fin k → Bool) : Bool

The strict majority vote of a Boolean vector: true iff more than half the positions are true.

Equations

• Complexity.majority f = decide (2 * Complexity.popCount f > k)

theorem Complexity.popCount_le {k : ℕ} (f : Fin k → Bool) : popCount f ≤ k

popCount is bounded by the length.

theorem Complexity.majority_eq_true_iff {k : ℕ} (f : Fin k → Bool) : majority f = true ↔ k / 2 < popCount f

theorem Complexity.majority_eq_false_iff {k : ℕ} (f : Fin k → Bool) : majority f = false ↔ popCount f ≤ k / 2

theorem Complexity.majority_eq_true_iff_mem_Icc {k : ℕ} (f : Fin k → Bool) : majority f = true ↔ popCount f ∈ Finset.Icc (k / 2 + 1) k

theorem Complexity.majority_eq_false_iff_mem_range {k : ℕ} (f : Fin k → Bool) : majority f = false ↔ popCount f ∈ Finset.range (k / 2 + 1)

theorem Complexity.card_majority_eq_true (k : ℕ) : {f : Fin k → Bool | majority f = true}.card = ∑ r ∈ Finset.Icc (k / 2 + 1) k, k.choose r

The exact binomial upper-tail count for strict-majority success.

theorem Complexity.card_majority_eq_false (k : ℕ) : {f : Fin k → Bool | majority f = false}.card = ∑ r ∈ Finset.range (k / 2 + 1), k.choose r

The exact binomial lower-tail count for strict-majority failure, including ties when the vector length is even.

theorem Complexity.card_majority_ne_true (k : ℕ) : {f : Fin k → Bool | majority f ≠ true}.card = ∑ r ∈ Finset.range (k / 2 + 1), k.choose r

Failure phrased as not returning true has the same exact lower-tail count.

theorem Complexity.popCount_add_popCount_not {k : ℕ} (f : Fin k → Bool) : (popCount f + popCount fun (i : Fin k) => !f i) = k

A position is either true or true-after-negation, never both: the two popCounts sum to the length.

theorem Complexity.popCount_not {k : ℕ} (f : Fin k → Bool) : (popCount fun (i : Fin k) => !f i) = k - popCount f

popCount of the pointwise negation is the complementary count.

theorem Complexity.majority_not_of_odd {k : ℕ} (hk : Odd k) (f : Fin k → Bool) : (majority fun (i : Fin k) => !f i) = !majority f

Antisymmetry of majority under negation at odd length. When the length k is odd there are no ties, so negating every bit flips the majority vote.