Cyclic circuits and least-fixed-point semantics

A cyclic circuit reuses native Line and Wire, allowing each equation to refer to any gate. Unlike a topologically ordered Program, the equations may contain feedback. Designated outputs can read inputs or gates; zero gates, zero outputs, sharing and unused components are allowed. Every equation is charged once by its operation weight.

For a monotone interpretation on a complete lattice, Mathlib's OrderHom.lfp gives a canonical least solution, without a separate construction certificate. This is mathematical semantics, not an execution algorithm or a finite-iteration bound. In particular, monotonicity alone does not imply that iteration through the natural numbers reaches or approaches the least solution. Native acyclic circuits embed with exactly the same gate values, outputs and weighted costs.

Main definitions

• Cslib.Circuits.CyclicCircuit: finite equations with designated output wires.
• Cslib.Circuits.CyclicCircuit.evalGates, Cslib.Circuits.CyclicCircuit.eval: least-solution gate values and outputs.
• Cslib.Circuits.CyclicCircuit.ecomplexityFrom: minimum cost from supplied source functions.

Main results

• Cslib.Circuits.Circuit.eval_toCyclic, Cslib.Circuits.Circuit.cost_toCyclic: the native acyclic embedding preserves semantics and costs.
• Cslib.Circuits.CyclicCircuit.evalGates_le: leastness among pre-fixed states.
• Cslib.Circuits.CyclicCircuit.ecomplexityFrom_le_acyclic: allowing feedback cannot increase source complexity.

References

• Adapted from LowerBound/Fusion/Cyclic.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib. The least-solution semantics uses Mathlib's Knaster–Tarski fixed-point API.

structure Cslib.Circuits.CyclicCircuit (σ : Signature) (inputCount outputCount : ℕ) : Type u

A finite system of gate equations with designated input or gate outputs.

• size : ℕ

  Number of equations; inputs and designated outputs cost nothing.

• lines : Fin self.size → Line σ inputCount self.size

  Every gate may read any input or gate, including itself.

• outputs : Fin outputCount → Wire inputCount self.size

  Each output reads an input or a solved gate. Sharing is allowed.

def Cslib.Circuits.CyclicCircuit.cost {σ : Signature} {n m : ℕ} (c : CyclicCircuit σ n m) (weight : σ.Op → ℕ) : ℕ

Sum all operation weights, including unused and repeated equations.

def Cslib.Circuits.Circuit.toCyclic {σ : Signature} {n m : ℕ} (c : Circuit σ n m) : CyclicCircuit σ n m

Regard the native acyclic program as a system of simultaneous equations.

@[simp]

theorem Cslib.Circuits.Circuit.cost_toCyclic {σ : Signature} {n m : ℕ} (c : Circuit σ n m) (weight : σ.Op → ℕ) : c.toCyclic.cost weight = c.program.cost weight

The embedding retains exactly the weighted cost of every gate.

def Cslib.Circuits.CyclicCircuit.step {σ : Signature} {U : Type v} {n m : ℕ} [Preorder U] (c : CyclicCircuit σ n m) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) : (Fin c.size → U) →o Fin c.size → U

Update every gate simultaneously using the supplied input and proposed gate values.

def Cslib.Circuits.CyclicCircuit.evalGates {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] (c : CyclicCircuit σ n m) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) : Fin c.size → U

The least solution of the gate equations in a complete lattice.

def Cslib.Circuits.CyclicCircuit.eval {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] (c : CyclicCircuit σ n m) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) : Fin m → U

Read all designated outputs at the least solution.

theorem Cslib.Circuits.CyclicCircuit.evalGates_fixed {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] (c : CyclicCircuit σ n m) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) (i : Fin c.size) : (c.lines i).eval I input (c.evalGates I hI input) = c.evalGates I hI input i

The least solution satisfies every gate equation. This is not a recursive simp rule.

theorem Cslib.Circuits.CyclicCircuit.evalGates_le {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] (c : CyclicCircuit σ n m) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) {state : Fin c.size → U} (h : ∀ (i : Fin c.size), (c.lines i).eval I input state ≤ state i) : c.evalGates I hI input ≤ state

The solution lies below every state whose equation results lie below its gate values.

@[simp]

theorem Cslib.Circuits.Circuit.evalGates_toCyclic {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] (c : Circuit σ n m) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) : c.toCyclic.evalGates I hI input = c.program.eval I input

The unique solution of an acyclic program is its ordinary gate evaluation.

@[simp]

theorem Cslib.Circuits.Circuit.eval_toCyclic {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] (c : Circuit σ n m) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (input : Fin n → U) : c.toCyclic.eval I hI input = c.eval I input

Embedding a native circuit preserves all outputs, including direct inputs and sharing.

def Cslib.Circuits.CyclicCircuit.ComputesFrom {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] {X : Type u_1} (c : CyclicCircuit σ n m) (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (target : X → Fin m → U) (sources : X → Fin n → U) : Prop

Compute the target from exactly the supplied sources using least-fixed-point semantics.

noncomputable def Cslib.Circuits.CyclicCircuit.ecomplexityFrom {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] {X : Type u_1} (I : Interpretation σ U) (hI : ∀ (op : σ.Op), Monotone (I op)) (weight : σ.Op → ℕ) (target : X → Fin m → U) (sources : X → Fin n → U) : ℕ∞

Minimum weighted cyclic cost, or infinity if no implementing circuit exists.

theorem Cslib.Circuits.CyclicCircuit.ecomplexityFrom_le_of_computesFrom {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] {X : Type u_1} {I : Interpretation σ U} {hI : ∀ (op : σ.Op), Monotone (I op)} {weight : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} (c : CyclicCircuit σ n m) (hc : c.ComputesFrom I hI target sources) : ecomplexityFrom I hI weight target sources ≤ ↑(c.cost weight)

Every implementing cyclic circuit bounds the minimum cost.

theorem Cslib.Circuits.CyclicCircuit.ecomplexityFrom_ne_top_iff {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] {X : Type u_1} {I : Interpretation σ U} {hI : ∀ (op : σ.Op), Monotone (I op)} {weight : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} : ecomplexityFrom I hI weight target sources ≠ ⊤ ↔ ∃ (c : CyclicCircuit σ n m), c.ComputesFrom I hI target sources

Finite cyclic complexity is equivalent to the existence of an implementation.

theorem Cslib.Circuits.CyclicCircuit.le_ecomplexityFrom_iff {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] {X : Type u_1} {I : Interpretation σ U} {hI : ∀ (op : σ.Op), Monotone (I op)} {weight : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} {k : ℕ∞} : k ≤ ecomplexityFrom I hI weight target sources ↔ ∀ (c : CyclicCircuit σ n m), c.ComputesFrom I hI target sources → k ≤ ↑(c.cost weight)

A lower bound on cyclic complexity holds exactly when it bounds every implementation.

theorem Cslib.Circuits.CyclicCircuit.ecomplexityFrom_le_acyclic {σ : Signature} {U : Type v} {n m : ℕ} [CompleteLattice U] {X : Type u_1} {I : Interpretation σ U} {hI : ∀ (op : σ.Op), Monotone (I op)} {weight : σ.Op → ℕ} {target : X → Fin m → U} {sources : X → Fin n → U} : ecomplexityFrom I hI weight target sources ≤ Circuits.ecomplexityFrom I weight target sources

Allowing feedback cannot increase minimum cost: native circuits embed without any cost.