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.
• lcmBelow and elementary upper bounds (lcmBelow_add_dvd, four_pow_ge_two_mul_lcmBelow, lcmBelow_lt_four_pow), together with the bundled PrimeCycleData interface (PrimeCycleData.step_circuit, PrimeCycleData.power_circuit, PrimeCycleData.exists_hard_power).

Main definitions

• 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.order: common-period product of the nontrivial cycle lengths (which equals the exact permutation order under LengthsCoprime).
• Cslib.Circuits.Boolean.Iteration.PrimeCycles.classPrime: least-index prime candidate in each hash class, or 1 if none exists.
• Cslib.Circuits.Boolean.Iteration.lcmBelow: least common multiple of {1, …, n}.
• Cslib.Circuits.Boolean.Iteration.PrimeCycleData: bundled cycle-length data with pairwise coprime nontrivial lengths.

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.lcmBelow_lt_four_pow: lcm(1, …, n) < 4 ^ n for 1 ≤ n.
• 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.

Least common multiples up to n

def Cslib.Circuits.Boolean.Iteration.lcmBelow (n : ℕ) : ℕ

The least common multiple lcm(1, …, n).

theorem Cslib.Circuits.Boolean.Iteration.lcmBelow_pos (n : ℕ) : 0 < lcmBelow n

theorem Cslib.Circuits.Boolean.Iteration.lcmBelow_eq_prod_prime_powers (n : ℕ) : lcmBelow n = ∏ p ∈ n.primesLE, p ^ Nat.log p n

theorem Cslib.Circuits.Boolean.Iteration.lcmBelow_add_dvd {m n : ℕ} (h : n ≤ m) : lcmBelow (m + n) ∣ lcmBelow m * (m + n).choose m

For n ≤ m, lcmBelow (m + n) divides lcmBelow m * (m + n).choose m. Every prime power p ^ L ≤ m + n exceeding m satisfies m < p ^ L ≤ m + n, which forces a base-p carry at digit L when adding m and n.

theorem Cslib.Circuits.Boolean.Iteration.lcmBelow_add_le {m n : ℕ} (h : n ≤ m) : lcmBelow (m + n) ≤ lcmBelow m * (m + n).choose m

theorem Cslib.Circuits.Boolean.Iteration.four_pow_ge_two_mul_lcmBelow (n : ℕ) (hn : 1 ≤ n) : 2 * lcmBelow n ≤ 4 ^ n

Elementary upper bound 2 * lcm(1, …, n) ≤ 4 ^ n for all n ≥ 1.

theorem Cslib.Circuits.Boolean.Iteration.lcmBelow_lt_four_pow (n : ℕ) (hn : 1 ≤ n) : lcmBelow n < 4 ^ n

For every n ≥ 1, lcm(1, …, n) < 4 ^ n.

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

@[simp]

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

@[simp]

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.pack_words {m K : ℕ} (x : BitString (m + K)) : pack (classWord x) (posWord x) = 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

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.power_add {m K : ℕ} (ℓ : BitVec m → ℕ) (hℓ : ∀ (r : BitVec m), ℓ r < 2 ^ K) (S T : ℕ) (x : BitString (m + K)) : power ℓ T (power ℓ S x) = power ℓ (S + T) x

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.advance_mod (a b T : ℕ) : ModulusCounter.advance a b (T % a) = ModulusCounter.advance a b 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.power_prod_eq_id {m K : ℕ} (ℓ : BitVec m → ℕ) : power ℓ (∏ r : BitVec m with 0 < ℓ r, ℓ r) = id

Every positive length divides the product of positive lengths, so that power is the identity.

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

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 ℓ

theorem Cslib.Circuits.Boolean.Iteration.PrimeCycles.dvd_order {m : ℕ} (ℓ : BitVec m → ℕ) {r : BitVec m} (hr : 1 < ℓ r) : ℓ r ∣ order ℓ

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]

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.pow_card_le_order {m : ℕ} {ℓ : BitVec m → ℕ} {L : ℕ} (hL : ∀ (r : BitVec m), 1 < ℓ r → L ≤ ℓ r) : L ^ (active ℓ).card ≤ order ℓ

The order is at least L ^ c when the c nontrivial lengths are each at least L.

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_mod {m g : ℕ} (f : ℕ → ℕ) (r : BitVec m) {z : ℕ} (hz : z < 2 ^ g) : candidate g f r z % 2 ^ g = z

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

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_spec {m g : ℕ} (f : ℕ → ℕ) (r : BitVec m) : classPrime m g f r = 1 ∨ ∃ z < 2 ^ g, classPrime m g f r = candidate g f r z ∧ Nat.Prime (classPrime m g f r)

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))

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

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

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

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

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))

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)

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.