Permutations with one prime cycle per hash class

This module formalizes the combinatorial and circuit-complexity structure of permutations on BitString (m + K) that act as a disjoint union of prime-length cycles indexed by m-bit hash classes. States of BitString (m + K) are pairs (r, b) of an m-bit class word r and a K-bit position word b. Given a cycle length ℓ r < 2 ^ K for each class r, the step map advances b by 1 modulo ℓ r when b < ℓ r and fixes every other state.

• PrimeCycles.iterate_step and PrimeCycles.power_apply_mod: the T-th power adds T modulo ℓ r, so it depends on T only through the remainder table r ↦ T % ℓ r.
• PrimeCycles.iterate_eq_iterate_iff: when the nontrivial lengths (1 < ℓ r) are pairwise coprime, two powers agree if and only if their exponents are congruent modulo order ℓ, the product of the nontrivial lengths. Hence order ℓ is both the permutation order (PrimeCycles.iterate_eq_id_iff) and the exact number of distinct powers (PrimeCycles.card_range_iterate).
• PrimeCycles.classPrime: the hash-class construction with candidates 2 ^ (m + g) + (r xor f z) * 2 ^ g + z for z < 2 ^ g and K = m + g + 1. Different classes have disjoint candidate sets (PrimeCycles.candidate_injective), so the chosen prime lengths are distinct and pairwise coprime (PrimeCycles.classPrime_coprime).
• PrimeCycles.near_landau_lower_bound: for any mixing function f with values below 2 ^ m, the resulting permutation is bijective, has order at least 2 ^ ((m + g) * c) where c is the number of active classes, and has a power below its order requiring more than q gates whenever the ordered-syntax exponent for q gates is below (m + g) * c.
• The bundled PrimeCycleData interface (PrimeCycleData.step_circuit, PrimeCycleData.power_circuit, PrimeCycleData.exists_hard_power).

Main definitions

• Cslib.Circuits.Boolean.Iteration.PrimeCycles.classWord, Cslib.Circuits.Boolean.Iteration.PrimeCycles.posWord, Cslib.Circuits.Boolean.Iteration.PrimeCycles.pack: split and pack m-bit class and K-bit position words.
• Cslib.Circuits.Boolean.Iteration.PrimeCycles.power: T-step map advancing each class r modulo ℓ r.
• Cslib.Circuits.Boolean.Iteration.PrimeCycles.step: single-step permutation power ℓ 1.
• Cslib.Circuits.Boolean.Iteration.PrimeCycles.active, Cslib.Circuits.Boolean.Iteration.PrimeCycles.order, Cslib.Circuits.Boolean.Iteration.PrimeCycles.LengthsCoprime: active classes, common-period product of the nontrivial cycle lengths (which equals the exact permutation order under LengthsCoprime), and pairwise coprimality predicate.
• Cslib.Circuits.Boolean.Iteration.PrimeCycles.candidate, Cslib.Circuits.Boolean.Iteration.PrimeCycles.classPrime: prime candidates and least-index prime candidate in each hash class, or 1 if none exists.
• Cslib.Circuits.Boolean.Iteration.PrimeCycleData, Cslib.Circuits.Boolean.Iteration.PrimeCycleData.activeLength, Cslib.Circuits.Boolean.Iteration.PrimeCycleData.stepNat, Cslib.Circuits.Boolean.Iteration.PrimeCycleData.step, Cslib.Circuits.Boolean.Iteration.PrimeCycleData.perm, Cslib.Circuits.Boolean.Iteration.PrimeCycleData.period, Cslib.Circuits.Boolean.Iteration.PrimeCycleData.lengthBits, Cslib.Circuits.Boolean.Iteration.PrimeCycleData.remainderBits, Cslib.Circuits.Boolean.Iteration.PrimeCycleData.ofHash: bundled cycle-length data with pairwise coprime nontrivial lengths and associated step, period, bit-encoding, and hash constructors.

Main results

• Cslib.Circuits.Boolean.Iteration.PrimeCycles.iterate_eq_iterate_iff: two powers agree iff the exponents are congruent modulo order ℓ.
• Cslib.Circuits.Boolean.Iteration.PrimeCycles.card_range_iterate: the number of distinct powers equals order ℓ.
• Cslib.Circuits.Boolean.Iteration.PrimeCycles.near_landau_lower_bound: explicit lower bound for the hash-class prime-cycle permutation.
• Cslib.Circuits.Boolean.Iteration.PrimeCycleData.step_circuit and Cslib.Circuits.Boolean.Iteration.PrimeCycleData.power_circuit: circuit synthesis for the step and T-th power from class-length and remainder tables.

References

• Adapted from lean/Proofs/PrimeCycles.lean in S. Schlesinger, Square-root circuit bounds for iterated functions.

Disjoint prime-cycle permutations indexed by hash classes

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.classWord {m K : ℕ} (x : BitString (m + K)) : BitVec m

The m-bit class word in the first m coordinates.

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.posWord {m K : ℕ} (x : BitString (m + K)) : BitVec K

The K-bit position word in the last K coordinates.

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.pack {m K : ℕ} (r : BitVec m) (b : BitVec K) : BitString (m + K)

Pack an m-bit class word and a K-bit position word into BitString (m + K).

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.classWord_pack {m K : ℕ} (r : BitVec m) (b : BitVec K) : classWord (pack r b) = r

Extracting the class word from pack r b recovers r.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.posWord_pack {m K : ℕ} (r : BitVec m) (b : BitVec K) : posWord (pack r b) = b

Extracting the position word from pack r b recovers b.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.pack_words {m K : ℕ} (x : BitString (m + K)) : pack (classWord x) (posWord x) = x

Repacking the class and position words of x recovers x.

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.power {m K : ℕ} (ℓ : BitVec m → ℕ) (T : ℕ) (x : BitString (m + K)) : BitString (m + K)

The T-th power: advance the position by T modulo ℓ r on the cycle b < ℓ r, and fix every other state (in particular every state with ℓ r ≤ 1).

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.step {m K : ℕ} (ℓ : BitVec m → ℕ) : BitString (m + K) → BitString (m + K)

The single-step permutation power ℓ 1.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.power_zero {m K : ℕ} (ℓ : BitVec m → ℕ) : power ℓ 0 = id

The 0-th power power ℓ 0 is the identity map.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.iterate_step {m K : ℕ} (ℓ : BitVec m → ℕ) (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) (T : ℕ) : (step ℓ)^[T] = power ℓ T

The T-th iterate of step ℓ is power ℓ T.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.power_apply_mod {m K : ℕ} (ℓ : BitVec m → ℕ) (T : ℕ) (r : BitVec m) (b : BitVec K) : power ℓ T (pack r b) = pack r (BitVec.ofNat K (if 0 < ℓ r ∧ b.toNat < ℓ r then (b.toNat + T % ℓ r) % ℓ r else b.toNat))

(step ℓ)^[T] (pack r b) depends on T only through T % ℓ r.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.step_bijective {m K : ℕ} (ℓ : BitVec m → ℕ) (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) : Function.Bijective (step ℓ)

When every cycle length is below 2 ^ K, step ℓ is a bijection on BitString (m + K).

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.power_eq_power_iff {m K : ℕ} (ℓ : BitVec m → ℕ) (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) (S T : ℕ) : power ℓ S = power ℓ T ↔ ∀ (r : BitVec m), 1 < ℓ r → S ≡ T [MOD ℓ r]

Two powers agree iff the exponents agree modulo every nontrivial cycle length.

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.active {m : ℕ} (ℓ : BitVec m → ℕ) : Finset (BitVec m)

The nontrivial classes (1 < ℓ r).

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.order {m : ℕ} (ℓ : BitVec m → ℕ) : ℕ

The common-period product of the nontrivial cycle lengths (which equals the exact permutation order under LengthsCoprime).

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.order_pos {m : ℕ} (ℓ : BitVec m → ℕ) : 0 < order ℓ

The common-period product order ℓ of the nontrivial cycle lengths is positive.

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.LengthsCoprime {m : ℕ} (ℓ : BitVec m → ℕ) : Prop

Pairwise coprimality of the nontrivial cycle lengths.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.modEq_order_iff {m : ℕ} {ℓ : BitVec m → ℕ} (hc : LengthsCoprime ℓ) (S T : ℕ) : S ≡ T [MOD order ℓ] ↔ ∀ (r : BitVec m), 1 < ℓ r → S ≡ T [MOD ℓ r]

Under LengthsCoprime ℓ, two exponents are congruent modulo order ℓ iff they are congruent modulo every nontrivial cycle length ℓ r.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.iterate_eq_iterate_iff {m K : ℕ} {ℓ : BitVec m → ℕ} (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) (hc : LengthsCoprime ℓ) (S T : ℕ) : (step ℓ)^[S] = (step ℓ)^[T] ↔ S ≡ T [MOD order ℓ]

With pairwise coprime nontrivial lengths, (step ℓ)^[S] = (step ℓ)^[T] iff S ≡ T [MOD order ℓ].

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.iterate_eq_id_iff {m K : ℕ} {ℓ : BitVec m → ℕ} (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) (hc : LengthsCoprime ℓ) (T : ℕ) : (step ℓ)^[T] = id ↔ order ℓ ∣ T

(step ℓ)^[T] = id iff order ℓ ∣ T.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.iterate_injective {m K : ℕ} {ℓ : BitVec m → ℕ} (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) (hc : LengthsCoprime ℓ) : Function.Injective fun (T : Fin (order ℓ)) => (step ℓ)^[↑T]

Distinct residues modulo order ℓ yield distinct powers.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.card_range_iterate {m K : ℕ} {ℓ : BitVec m → ℕ} (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) (hc : LengthsCoprime ℓ) : Nat.card ↑(Set.range fun (T : ℕ) => (step ℓ)^[T]) = order ℓ

The number of distinct powers of step ℓ is order ℓ.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.exists_hard_power_of_budget_lt {m K : ℕ} {ℓ : BitVec m → ℕ} (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) (hc : LengthsCoprime ℓ) (q : ℕ) (large : signature.orderedBudget (m + K) (m + K) q < order ℓ) : ∃ T < order ℓ, ∀ (out : Circuit signature (m + K) (m + K)), out.Computes interpretation (step ℓ)^[T] → q < out.size

If the ordered-syntax budget for q gates is below order ℓ, some power below order ℓ requires more than q gates.

Hash-class prime candidates

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.candidate {m : ℕ} (g : ℕ) (f : ℕ → ℕ) (r : BitVec m) (z : ℕ) : ℕ

The z-th candidate of class r: 2 ^ (m + g) + (r xor f z) * 2 ^ g + z.

def Cslib.Circuits.Boolean.Iteration.PrimeCycles.classPrime (m g : ℕ) (f : ℕ → ℕ) (r : BitVec m) : ℕ

The class length: the prime candidate with least z < 2 ^ g, or 1 if there is none.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.candidate_injective {m g : ℕ} (f : ℕ → ℕ) {r s : BitVec m} {y z : ℕ} (hy : y < 2 ^ g) (hz : z < 2 ^ g) (h : candidate g f r y = candidate g f s z) : r = s

Different classes have disjoint candidate sets.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.classPrime_bounds {m g : ℕ} {f : ℕ → ℕ} (hf : ∀ (z : ℕ), f z < 2 ^ m) (r : BitVec m) : classPrime m g f r < 2 ^ (m + g + 1) ∧ (1 < classPrime m g f r → 2 ^ (m + g) ≤ classPrime m g f r ∧ Nat.Prime (classPrime m g f r))

Every classPrime m g f r is below 2 ^ (m + g + 1), and any nontrivial classPrime m g f r is a prime at least 2 ^ (m + g).

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.classPrime_coprime {m : ℕ} (g : ℕ) (f : ℕ → ℕ) : LengthsCoprime (classPrime m g f)

Nontrivial class lengths are distinct primes, hence pairwise coprime.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.near_landau_lower_bound (m g : ℕ) (f : ℕ → ℕ) (hf : ∀ (z : ℕ), f z < 2 ^ m) (q h : ℕ) (hw : m + (m + g + 1) + q + 1 ≤ 2 ^ h) (large : 3 * q + h * (2 * q + (m + (m + g + 1)) + 1) < (m + g) * (active (classPrime m g f)).card) : Function.Bijective (step (classPrime m g f)) ∧ 2 ^ ((m + g) * (active (classPrime m g f)).card) ≤ order (classPrime m g f) ∧ ∃ T < order (classPrime m g f), ∀ (out : Circuit signature (m + (m + g + 1)) (m + (m + g + 1))), out.Computes interpretation (step (classPrime m g f))^[T] → q < out.size

Lower bound for the hash-class permutation: for any mixing function f with values below 2 ^ m, put K = m + g + 1 and let ℓ r be the least-index prime candidate of class r. The step is a bijection of BitString (m + K), its order is at least 2 ^ ((m + g) * c) where c is the number of active classes, and if the ordered-syntax exponent for q gates is below (m + g) * c, some power F^[T] with T < order requires more than q gates.

Bundled prime-cycle permutation data and circuit synthesis

structure Cslib.Circuits.Boolean.Iteration.PrimeCycleData (m K : ℕ) : Type

Bundled cycle-length specification for m-bit hash classes and K-bit cycle positions, with pairwise coprime nontrivial cycle lengths.

• length : BitVec m → ℕ

  Cycle length assigned to each m-bit class.

• length_lt (r : BitVec m) : self.length r < 2 ^ K

  Every cycle length fits in K bits.

• lengths_coprime : PrimeCycles.LengthsCoprime self.length

  Nontrivial cycle lengths (1 < length r) are pairwise coprime.

def Cslib.Circuits.Boolean.Iteration.PrimeCycleData.activeLength {m K : ℕ} (D : PrimeCycleData m K) (r : BitVec m) : ℕ

The effective cycle length of class r, equal to D.length r when 1 < D.length r and 1 otherwise.

def Cslib.Circuits.Boolean.Iteration.PrimeCycleData.stepNat {m K : ℕ} (D : PrimeCycleData m K) (r : BitVec m) (b : ℕ) : ℕ

Natural-number position update for class r in one step.

def Cslib.Circuits.Boolean.Iteration.PrimeCycleData.step {m K : ℕ} (D : PrimeCycleData m K) : BitString (m + K) → BitString (m + K)

Single-step map on BitString (m + K).

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.step_bijective {m K : ℕ} (D : PrimeCycleData m K) : Function.Bijective D.step

The single-step map D.step is a bijection on BitString (m + K).

noncomputable def Cslib.Circuits.Boolean.Iteration.PrimeCycleData.perm {m K : ℕ} (D : PrimeCycleData m K) : Equiv.Perm (BitString (m + K))

The permutation of BitString (m + K) induced by D.step.

def Cslib.Circuits.Boolean.Iteration.PrimeCycleData.period {m K : ℕ} (D : PrimeCycleData m K) : ℕ

The order of D.step, equal to the product of the nontrivial cycle lengths.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.period_dvd_of_fixed {m K : ℕ} (D : PrimeCycleData m K) (T : ℕ) : D.step^[T] = id ↔ D.period ∣ T

D.step^[T] is the identity iff D.period divides T.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.powers_injective {m K : ℕ} (D : PrimeCycleData m K) : Function.Injective fun (T : Fin D.period) => D.step^[↑T]

Powers D.step^[T] for T < D.period are pairwise distinct.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.exists_hard_power {m K : ℕ} (D : PrimeCycleData m K) (q : ℕ) (large : signature.orderedBudget (m + K) (m + K) q < D.period) : ∃ T < D.period, ∀ (out : Circuit signature (m + K) (m + K)), out.Computes interpretation D.step^[T] → q < out.size

If the ordered-syntax budget for q gates is strictly below D.period, some power D.step^[T] with T < D.period requires more than q gates.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.step_diff_card_le {m K : ℕ} (D : PrimeCycleData m K) : {x : BitString (m + K) | D.step x ≠ x}.card ≤ 2 ^ (m + K)

The number of states moved by D.step is at most 2 ^ (m + K).

def Cslib.Circuits.Boolean.Iteration.PrimeCycleData.lengthBits {m K : ℕ} (D : PrimeCycleData m K) (r : BitString m) : BitString K

The K-bit cycle-length map on BitString m associated with D.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.word_lengthBits {m K : ℕ} (D : PrimeCycleData m K) (r : BitString m) : word (D.lengthBits r) = BitVec.ofNat K (D.length (word r))

Packing D.lengthBits r into a BitVec K gives BitVec.ofNat K (D.length (word r)).

def Cslib.Circuits.Boolean.Iteration.PrimeCycleData.remainderBits {m K : ℕ} (D : PrimeCycleData m K) (T : ℕ) (r : BitString m) : BitString K

The K-bit remainder map r ↦ T % D.length r (or 0 when D.length r = 0) on BitString m.

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.word_remainderBits {m K : ℕ} (D : PrimeCycleData m K) (T : ℕ) (r : BitString m) : word (D.remainderBits T r) = BitVec.ofNat K (if 0 < D.length (word r) then T % D.length (word r) else 0)

Packing D.remainderBits T r into a BitVec K gives T % D.length (word r) (or 0 when D.length (word r) = 0).

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.step_circuit {m K : ℕ} (D : PrimeCycleData m K) (cLen : Circuit signature m K) (hLen : cLen.Computes interpretation D.lengthBits) : ∃ (out : Circuit signature (m + K) (m + K)), out.Computes interpretation D.step ∧ out.size ≤ cLen.size + 50 * K + 20

Given a circuit cLen computing the K-bit class length D.lengthBits, the single-step permutation D.step has a circuit of size at most cLen.size + 50 * K + 20.

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycleData.power_circuit {m K : ℕ} (D : PrimeCycleData m K) (T : ℕ) (cLen cRem : Circuit signature m K) (hLen : cLen.Computes interpretation D.lengthBits) (hRem : cRem.Computes interpretation (D.remainderBits T)) : ∃ (out : Circuit signature (m + K) (m + K)), out.Computes interpretation D.step^[T] ∧ out.size ≤ cLen.size + cRem.size + 100 * (K + 1)

Given circuits cLen for D.lengthBits and cRem for D.remainderBits T, the T-th power D.step^[T] has a circuit of size at most cLen.size + cRem.size + 100 * (K + 1).

def Cslib.Circuits.Boolean.Iteration.PrimeCycleData.ofHash (m g : ℕ) (f : ℕ → ℕ) (hf : ∀ (z : ℕ), f z < 2 ^ m) : PrimeCycleData m (m + g + 1)

Construct PrimeCycleData from the hash-class prime construction PrimeCycles.classPrime.