Factorial-improved Shannon counting

After semantic normalization, all internal gate functions are distinct. Each computed function can therefore be encoded under all g! gate relabelings, and those encodings are distinct. This removes the artificial topological ordering from the leading Shannon count.

Loose presentations and relabeling

structure Algebraic.LooseCircuit (σ : Signature) (n g m : ℕ) : Type u_1

A circuit presentation whose internal gates need not be topologically ordered.

• internal : Fin g → Line σ n g

  One defining line for every labeled internal gate.

• outputs : Fin m → Wire n g

  One designated wire for every output.

def Algebraic.looseCircuitEquiv (σ : Signature) (n g m : ℕ) : LooseCircuit σ n g m ≃ (Fin g → Line σ n g) × (Fin m → Wire n g)

A loose circuit is equivalently a pair of indexed line collections.

Equations

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

@[instance_reducible]

noncomputable instance Algebraic.instFintypeLooseCircuit {σ : Signature} {n g m : ℕ} [Fintype σ.Op] : Fintype (LooseCircuit σ n g m)

Equations

• Algebraic.instFintypeLooseCircuit = Fintype.ofEquiv ((Fin g → Cslib.Circuits.Line σ n g) × (Fin m → Cslib.Circuits.Wire n g)) (Algebraic.looseCircuitEquiv σ n g m).symm

theorem Algebraic.card_looseCircuit {σ : Signature} {n g m : ℕ} [Fintype σ.Op] : Fintype.card (LooseCircuit σ n g m) = σ.lineCount (n + g) ^ g * (n + g) ^ m

Exact count of loose labeled circuit presentations.

def Algebraic.LooseCircuit.Satisfies {σ : Signature} {n g m : ℕ} {U : Type u_2} (circuit : LooseCircuit σ n g m) (interpretation : Interpretation σ U) (input : Fin n → U) (values : Fin g → U) : Prop

A loose circuit valuation solves all of its internal gate equations.

Equations

• circuit.Satisfies interpretation input values = ∀ (gate : Fin g), values gate = (circuit.internal gate).eval interpretation input values

def Algebraic.LooseCircuit.evalOutputs {σ : Signature} {n g m : ℕ} {U : Type u_2} (circuit : LooseCircuit σ n g m) (_interpretation : Interpretation σ U) (input : Fin n → U) (values : Fin g → U) : Fin m → U

Read designated output wires under a chosen internal-gate valuation.

Equations

• circuit.evalOutputs _interpretation input values output = Cslib.Circuits.Wire.elim input values (circuit.outputs output)

def Cslib.Circuits.Wire.Renaming.ofEquiv {g h n : ℕ} (labels : Fin g ≃ Fin h) : Renaming n g h

Rename gate wires along a bijection of gate labels, fixing every input.

Equations

• Cslib.Circuits.Wire.Renaming.ofEquiv labels = { gates := fun (gate : Fin g) => Cslib.Circuits.Wire.gate (labels gate) }

theorem Cslib.Circuits.Wire.value_ofEquiv {g h n : ℕ} {U : Sort u_1} (labels : Fin g ≃ Fin h) (inputs : Fin n → U) (values : Fin g → U) (wire : Wire n g) : elim inputs (values ∘ ⇑labels.symm) ((Renaming.ofEquiv labels).apply wire) = elim inputs values wire

theorem Cslib.Circuits.Wire.value_permutation {g n : ℕ} {U : Sort u_1} (permutation : Equiv.Perm (Fin g)) (inputs : Fin n → U) (values : Fin g → U) (wire : Wire n g) : elim inputs (values ∘ ⇑(Equiv.symm permutation)) ((Renaming.ofPermutation permutation).apply wire) = elim inputs values wire

def Cslib.Circuits.Circuit.relabel {σ : Signature} {n m g : ℕ} (circuit : Circuit σ n m) (labels : Fin circuit.size ≃ Fin g) : Algebraic.LooseCircuit σ n g m

Forget topological order, then rename every internal gate along a bijection onto the labels Fin g.

Equations

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

theorem Cslib.Circuits.Circuit.relabel_satisfies {σ : Signature} {n m g : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (labels : Fin circuit.size ≃ Fin g) (interpretation : Interpretation σ U) (input : Fin n → U) : (circuit.relabel labels).Satisfies interpretation input (circuit.program.eval interpretation input ∘ ⇑labels.symm)

theorem Cslib.Circuits.Circuit.relabel_evalOutputs {σ : Signature} {n m g : ℕ} {U : Type u_2} (circuit : Circuit σ n m) (labels : Fin circuit.size ≃ Fin g) (interpretation : Interpretation σ U) (input : Fin n → U) : (circuit.relabel labels).evalOutputs interpretation input (circuit.program.eval interpretation input ∘ ⇑labels.symm) = circuit.eval interpretation input

Acyclicity and unique valuations

def Cslib.Circuits.Wire.Below {g n : ℕ} (rank : Fin g → ℕ) (bound : ℕ) (wire : Wire n g) : Prop

Inputs are always available; a gate wire is below a numeric rank bound.

Equations

• Cslib.Circuits.Wire.Below rank bound wire = Cslib.Circuits.Wire.elim (fun (x : Fin n) => True) (fun (gate : Fin g) => rank gate < bound) wire

theorem Cslib.Circuits.Wire.below_castSucc {n g : ℕ} (wire : Wire n g) (gate : Fin g) : Below (fun (gate : Fin (g + 1)) => ↑gate) (↑gate.castSucc) wire.castSucc ↔ Below (fun (gate : Fin g) => ↑gate) (↑gate) wire

theorem Cslib.Circuits.Wire.below_last {n g : ℕ} (wire : Wire n g) : Below (fun (gate : Fin (g + 1)) => ↑gate) (↑(Fin.last g)) wire.castSucc

theorem Cslib.Circuits.Program.lines_below {σ : Signature} {n g : ℕ} (program : Program σ n g) (gate : Fin g) (argument : Fin (σ.Arity (program.lines gate).op)) : Wire.Below (fun (gate : Fin g) => ↑gate) (↑gate) ((program.lines gate).wires argument)

def Algebraic.LooseCircuit.AcyclicUnder {σ : Signature} {n g m : ℕ} (circuit : LooseCircuit σ n g m) (rank : Fin g → ℕ) : Prop

A rank strictly decreases along every internal gate dependency.

Equations

• circuit.AcyclicUnder rank = ∀ (gate : Fin g) (argument : Fin (σ.Arity (circuit.internal gate).op)), Cslib.Circuits.Wire.Below rank (rank gate) ((circuit.internal gate).wires argument)

theorem Cslib.Circuits.Wire.below_permutation {g n : ℕ} (permutation : Equiv.Perm (Fin g)) (gate : Fin g) (wire : Wire n g) : Below (fun (renamed : Fin g) => ↑((Equiv.symm permutation) renamed)) (↑((Equiv.symm permutation) gate)) ((Renaming.ofPermutation permutation).apply wire) ↔ Below (fun (original : Fin g) => ↑original) (↑((Equiv.symm permutation) gate)) wire

theorem Cslib.Circuits.Wire.below_ofEquiv {g h n : ℕ} (labels : Fin g ≃ Fin h) (gate : Fin h) (wire : Wire n g) : Below (fun (renamed : Fin h) => ↑(labels.symm renamed)) (↑(labels.symm gate)) ((Renaming.ofEquiv labels).apply wire) ↔ Below (fun (original : Fin g) => ↑original) (↑(labels.symm gate)) wire

theorem Cslib.Circuits.Circuit.relabel_acyclic {σ : Signature} {n m g : ℕ} (circuit : Circuit σ n m) (labels : Fin circuit.size ≃ Fin g) : (circuit.relabel labels).AcyclicUnder fun (gate : Fin g) => ↑(labels.symm gate)

theorem Cslib.Circuits.Wire.values_eq_of_below {g n : ℕ} {U : Sort u_1} (rank : Fin g → ℕ) (bound : ℕ) (wire : Wire n g) (below : Below rank bound wire) (inputs : Fin n → U) (left right : Fin g → U) (agree : ∀ (gate : Fin g), rank gate < bound → left gate = right gate) : elim inputs left wire = elim inputs right wire

theorem Algebraic.LooseCircuit.satisfies_unique {σ : Signature} {n g m : ℕ} {U : Type u_2} (circuit : LooseCircuit σ n g m) (interpretation : Interpretation σ U) (input : Fin n → U) (rank : Fin g → ℕ) (acyclic : circuit.AcyclicUnder rank) {left right : Fin g → U} (leftSatisfies : circuit.Satisfies interpretation input left) (rightSatisfies : circuit.Satisfies interpretation input right) : left = right

An acyclic loose presentation has at most one solution to its gate equations.

The factorial encoding

@[reducible, inline]

abbrev Cslib.Circuits.Circuit.IrredundantTarget {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n g m : ℕ) : Type u_1

A target together with evidence that an irredundant g-gate circuit computes it.

Equations

• Cslib.Circuits.Circuit.IrredundantTarget interpretation n g m = ↥(Cslib.Circuits.Circuit.irredundantFunctions interpretation n g m)

noncomputable def Cslib.Circuits.Circuit.irredundantRepresentative {U : Type u_1} {σ : Signature} {n g m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (target : IrredundantTarget interpretation n g m) : Circuit σ n m

Choose one irredundant representative circuit for a target.

Equations

• Cslib.Circuits.Circuit.irredundantRepresentative interpretation target = Classical.choose ⋯

theorem Cslib.Circuits.Circuit.irredundantRepresentative_size {U : Type u_1} {σ : Signature} {n g m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (target : IrredundantTarget interpretation n g m) : (irredundantRepresentative interpretation target).size = g

theorem Cslib.Circuits.Circuit.irredundantRepresentative_irredundant {U : Type u_1} {σ : Signature} {n g m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (target : IrredundantTarget interpretation n g m) : (irredundantRepresentative interpretation target).Irredundant interpretation

theorem Cslib.Circuits.Circuit.irredundantRepresentative_eval {U : Type u_1} {σ : Signature} {n g m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (target : IrredundantTarget interpretation n g m) : (irredundantRepresentative interpretation target).eval interpretation = ↑target

noncomputable def Cslib.Circuits.Circuit.representativeLabels {U : Type u_1} {σ : Signature} {n g m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (target : IrredundantTarget interpretation n g m) (permutation : Equiv.Perm (Fin g)) : Fin (irredundantRepresentative interpretation target).size ≃ Fin g

Gate labels of the chosen representative, renamed by a permutation of Fin g.

Equations

• Cslib.Circuits.Circuit.representativeLabels interpretation target permutation = (finCongr ⋯).trans permutation

noncomputable def Cslib.Circuits.Circuit.sharpEncoding {U : Type u_1} {σ : Signature} {n g m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) : IrredundantTarget interpretation n g m × Equiv.Perm (Fin g) → Algebraic.LooseCircuit σ n g m

Encode one chosen irredundant circuit for a function under a gate renaming.

Equations

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

theorem Cslib.Circuits.Circuit.sharpEncoding_injective {U : Type u_1} {σ : Signature} {n g m : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) : Function.Injective (sharpEncoding interpretation)

The target fixes the unique acyclic valuation of an encoded presentation; irredundancy then makes its gate permutation recoverable.

Counting consequences

theorem Cslib.Circuits.Circuit.card_irredundantFunctions_mul_factorial_le {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n g m : ℕ) : (irredundantFunctions interpretation n g m).card * g.factorial ≤ σ.lineCount (n + g) ^ g * (n + g) ^ m

Sharp fixed-size Shannon count, including the full g! relabeling gain.

def Cslib.Circuits.Signature.sharpCount (σ : Signature) [Fintype σ.Op] (n g m : ℕ) : ℕ

Sharp number of possible functions at exactly g internal gates.

Equations

• σ.sharpCount n g m = σ.lineCount (n + g) ^ g * (n + g) ^ m / g.factorial

theorem Cslib.Circuits.Circuit.card_irredundantFunctions_le_sharpCount {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n g m : ℕ) : (irredundantFunctions interpretation n g m).card ≤ σ.sharpCount n g m

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

Sharp Shannon budget for all circuits with at most G internal gates.

Equations

• σ.sharpBudget n m G = ∑ g ∈ Finset.range (G + 1), σ.sharpCount n g m

theorem Cslib.Circuits.Circuit.card_functionsAtMost_le_sharpBudget {U : Type u_1} {σ : Signature} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (n m G : ℕ) : (functionsAtMost interpretation n m G).card ≤ σ.sharpBudget n m G

theorem Cslib.Circuits.Circuit.exists_hard_in_family_sharp {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (family : Finset (Algebraic.Target U n m)) (large : σ.sharpBudget n m G < family.card) : ∃ target ∈ family, GateHard interpretation G target

A family larger than the sharp budget contains a size-hard function.

theorem Cslib.Circuits.Circuit.exists_hard_sharp {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (large : σ.sharpBudget n m G < Algebraic.Target.count U n m) : ∃ (target : Algebraic.Target U n m), GateHard interpretation G target

Full-universe sharp Shannon lower bound.

theorem Cslib.Circuits.Circuit.exists_hard_sharp_of_complete {U : Type u_1} {σ : Signature} {n m G : ℕ} [Fintype σ.Op] [Fintype U] (interpretation : Interpretation σ U) (complete : interpretation.FunctionallyComplete) (large : σ.sharpBudget n m G < Algebraic.Target.count U n m) : ∃ (target : Algebraic.Target U n m), GateHard interpretation G target ∧ ∃ (circuit : Circuit σ n m), circuit.ComputesWith interpretation target

Under functional completeness, a target outside the sharp budget is both hard below G and computable at some finite size.

theorem Cslib.Circuits.Circuit.exists_boolean_hard_sharp {σ : Signature} {n m G : ℕ} [Fintype σ.Op] (interpretation : Interpretation σ Bool) (large : σ.sharpBudget n m G < Algebraic.Target.count Bool n m) : ∃ (target : Algebraic.Target Bool n m), GateHard interpretation G target

Boolean specialization of the sharp Shannon theorem.