Closed-form Shannon counting lower bounds

This file turns the exact factorial-improved census into the familiar coefficient-one Shannon lower bound. For a fixed finite basis of maximum arity r ≥ 2 over a q-element universe, almost every m-output function requires more than ⌊m qⁿ / ((r - 1) n)⌋ internal gates.

The proof keeps the exact budget. For any fixed shift t, the denominator n eventually puts that budget below q ^ (n - t); choosing t large absorbs all basis-dependent constants while retaining leading coefficient one.

Stirling reduction

noncomputable def Cslib.Circuits.Signature.stirlingExponent (σ : Signature) [Fintype σ.Op] (n m G : ℕ) : ℝ

Logarithmic exponent obtained from the factorial-improved final term after retaining the leading part of Stirling's lower bound.

Equations

• σ.stirlingExponent n m G = Real.log (↑G + 1) + ↑G * Real.log ↑(σ.lineCount (n + G)) + ↑m * Real.log (↑n + ↑G) - (↑G * Real.log ↑G - ↑G)

noncomputable def Algebraic.Shannon.logTargetCount (q n m : ℕ) : ℝ

Logarithm of the number q ^ (m * q ^ n) of m-output functions on n inputs over a q-element universe, when q is positive.

Equations

• Algebraic.Shannon.logTargetCount q n m = ↑(m * q ^ n) * Real.log ↑q

theorem Algebraic.Nat.cast_mul_log_sub_le_log_factorial {G : ℕ} (positive : 0 < G) : ↑G * Real.log ↑G - ↑G ≤ Real.log ↑G.factorial

The part of Stirling's lower bound responsible for the sharp leading constant.

theorem Cslib.Circuits.Signature.finalTerm_le_exp_stirling (σ : Signature) [Fintype σ.Op] {n m G : ℕ} (positive : 0 < G) (linesPositive : 0 < σ.lineCount (n + G)) : σ.finalTerm n m G ≤ Real.exp (σ.stirlingExponent n m G)

Exponential envelope obtained by inserting the leading part of Stirling's lower bound into the factorial-improved final term.

theorem Cslib.Circuits.Circuit.exists_hard_of_stirlingLog {U : Type u_1} {σ : Signature} {G n m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (universeNontrivial : 1 < Fintype.card U) (gatePositive : 0 < G) (enoughLines : G ≤ σ.lineCount (n + G)) (linesPositive : 0 < σ.lineCount (n + G)) (large : σ.stirlingExponent n m G < Algebraic.Shannon.logTargetCount (Fintype.card U) n m) : ∃ (target : Algebraic.Target U n m), GateHard interpretation G target

Logarithmic finite form of the sharp Shannon criterion. Its left side has leading contribution (r - 1) * G * n * log q for an r-ary signature over a q-element universe.

Gate-budget estimates

def Algebraic.Shannon.gateBudget (q r m n : ℕ) : ℕ

Internal-gate budget at the sharp Shannon scale. Natural-number division implements the floor; its value at n = 0 is irrelevant to eventual results.

Equations

• Algebraic.Shannon.gateBudget q r m n = m * q ^ n / ((r - 1) * n)

@[simp]

theorem Algebraic.Shannon.gateBudget_two_two_one (n : ℕ) : gateBudget 2 2 1 n = 2 ^ n / n

Elementary exponential growth estimates

Gate-budget arithmetic

Bounding the Stirling exponent

Negligibility of the final term

Closed-form density theorems

theorem Cslib.Circuits.Circuit.asymptoticallyAlmostAllHard_shannon {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) {r m : ℕ} (maximum : σ.HasMaximumArity r) (universeNontrivial : 2 ≤ Fintype.card U) (arityAtLeastTwo : 2 ≤ r) (outputsPositive : 0 < m) : AsymptoticallyAlmostAllHard interpretation m (fullFamily U m) (Algebraic.Shannon.gateBudget (Fintype.card U) r m)

Closed-form Shannon theorem for an arbitrary fixed finite basis. At the exact budget ⌊m |U|ⁿ / ((r - 1) n)⌋, the easy functions form an asymptotically negligible fraction of the full function space.

theorem Cslib.Circuits.Circuit.tendsto_easyDensity_zero_shannon {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) {r m : ℕ} (maximum : σ.HasMaximumArity r) (universeNontrivial : 2 ≤ Fintype.card U) (arityAtLeastTwo : 2 ≤ r) (outputsPositive : 0 < m) : Filter.Tendsto (fun (n : ℕ) => easyDensity interpretation (fullFamily U m n) (Algebraic.Shannon.gateBudget (Fintype.card U) r m n)) Filter.atTop (nhds 0)

Conventional density form of the closed Shannon theorem.

theorem Cslib.Circuits.Circuit.tendsto_boolean_easyDensity_zero_shannon {σ : Signature} [Fintype σ.Op] (interpretation : Interpretation σ Bool) {r m : ℕ} (maximum : σ.HasMaximumArity r) (arityAtLeastTwo : 2 ≤ r) (outputsPositive : 0 < m) : Filter.Tendsto (fun (n : ℕ) => easyDensity interpretation (fullFamily Bool m n) (Algebraic.Shannon.gateBudget 2 r m n)) Filter.atTop (nhds 0)

Boolean specialization of the closed Shannon theorem. For a binary basis and one output, Shannon.gateBudget_two_two_one identifies the budget with 2 ^ n / n.

theorem Cslib.Circuits.Circuit.tendsto_finiteField_easyDensity_zero_shannon {σ : Signature} {K : Type u} [Field K] [Fintype K] [Fintype σ.Op] (interpretation : Interpretation σ K) {r m : ℕ} (maximum : σ.HasMaximumArity r) (arityAtLeastTwo : 2 ≤ r) (outputsPositive : 0 < m) : Filter.Tendsto (fun (n : ℕ) => easyDensity interpretation (fullFamily K m n) (Algebraic.Shannon.gateBudget (Fintype.card K) r m n)) Filter.atTop (nhds 0)

Finite-field specialization of the closed Shannon theorem.