Frontiers measured by distinct circuit signals

The compiler labels every edge by the wire it carries. Exactness makes all edges with the same label equal on every accepting run. ncard_accepted_le_signals therefore charges only the distinct signals on the union of adjacent frontiers, together with the input read at the step. This is a capacity theorem, not a new universal layout bound.

theorem Complexity.Frontier.Compiler.signal_junction_path {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} {U : Type u_2} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) (w : Signal p out) (k : ℕ) (hk : k < fanout p out w) : Relation.ReflTransGen ((network p out I Acc).labelGraph Edge.signal w).Adj (Vertex.junction ⟨w, ⟨k, hk⟩⟩) (Vertex.signal w)

All occurrences of a signal are joined by edges carrying that same signal.

theorem Complexity.Frontier.Compiler.signal_occurrence_path {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} {U : Type u_2} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) (w : Signal p out) (v : Vertex p out) (hv : v ∈ (network p out I Acc).signalHypergraph Edge.signal w) : Relation.ReflTransGen ((network p out I Acc).labelGraph Edge.signal w).Adj v (Vertex.signal w)

theorem Complexity.Frontier.Compiler.signalCut_eq_hypergraph_cut {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} {U : Type u_2} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) (X : Set (Vertex p out)) : Edge.signal '' (network p out I Acc).cut X = ((network p out I Acc).signalHypergraph Edge.signal).cut X

The junction compiler realizes exactly the native signal-hypergraph separator.

theorem Complexity.Frontier.Compiler.signalCut_submodular {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} {U : Type u_2} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) (X Y : Set (Vertex p out)) : (Edge.signal '' (network p out I Acc).cut (X ∩ Y)).ncard + (Edge.signal '' (network p out I Acc).cut (X ∪ Y)).ncard ≤ (Edge.signal '' (network p out I Acc).cut X).ncard + (Edge.signal '' (network p out I Acc).cut Y).ncard

Distinct-signal capacity is a symmetric submodular separator function.

noncomputable def Complexity.Frontier.Compiler.signalFrontier {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} {U : Type u_2} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) (π : Layout (Vertex p out)) (t : ℕ) : Set (Signal p out)

The signal labels on a frontier. Repeated edges of the same wire are charged once.

Equations

• Complexity.Frontier.Compiler.signalFrontier I Acc π t = Complexity.Frontier.Compiler.Edge.signal '' (Complexity.Frontier.Compiler.network p out I Acc).frontier π t

theorem Complexity.Frontier.Compiler.ncard_signalFrontier_le {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} {U : Type u_2} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) (π : Layout (Vertex p out)) (t : ℕ) : (signalFrontier I Acc π t).ncard ≤ ((network p out I Acc).frontier π t).ncard

Signal capacity never exceeds edge capacity.

theorem Complexity.Frontier.Compiler.ncard_accepted_le_signals {σ : Cslib.Circuits.Signature} {n s : ℕ} {O : Type u_1} {U : Type u_2} [Finite O] [Finite U] [Nonempty U] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (Acc : O → Set U) (π : Layout (Vertex p out)) {K b : ℕ} (hfree : RectangleFree (network p out I Acc).accepted K) (hK : K ≤ (network p out I Acc).accepted.ncard) (hb : ∀ (t : ℕ) (ht : t < Nat.card (Vertex p out)), (signalFrontier I Acc π t ∪ signalFrontier I Acc π (t + 1)).ncard + ((network p out I Acc).readAt ((Equiv.symm π) ⟨t, ht⟩)).ncard ≤ b) : (network p out I Acc).accepted.ncard ≤ (K - 1) ^ 2 * (Nat.card (Vertex p out) * Nat.card U ^ b + Nat.card U ^ (network p out I Acc).readᶜ.ncard)

Counting with signal capacity. The step budget charges distinct signals across both frontiers and the inputs read at the vertex. It can be strictly smaller than the edge budget.