Mixed input-output fibers

For an arbitrary map, specify some input coordinates and some output coordinates. The largest remaining fiber measures ambiguity in this mixed observation. Equal frontier values permit two complementary splices, embedding each frontier class in the product of two mixed fibers. No linearity or algebra on the alphabet is needed.

def Complexity.Frontier.mixedFiber {ι : Type u_1} {O : Type u_2} {U : Type u_3} (F : (ι → U) → O → U) (X : Set ι) (Y : Set O) (x : ι → U) : Set (ι → U)

Inputs indistinguishable from x after observing the inputs in X and outputs in Y.

Equations

• Complexity.Frontier.mixedFiber F X Y x = {z : ι → U | Set.EqOn z x X ∧ Set.EqOn (F z) (F x) Y}

noncomputable def Complexity.Frontier.maxMixedFiber {ι : Type u_1} {O : Type u_2} {U : Type u_3} [Finite ι] [Finite U] (F : (ι → U) → O → U) (X : Set ι) (Y : Set O) : ℕ

Largest nonempty fiber of a mixed input-output observation. Empty fibers do not affect the maximum; indexing by an input therefore includes every relevant observation.

Equations

• Complexity.Frontier.maxMixedFiber F X Y = Finset.univ.sup fun (x : ι → U) => (Complexity.Frontier.mixedFiber F X Y x).ncard

theorem Complexity.Frontier.ncard_mixedFiber_le {ι : Type u_1} {O : Type u_2} {U : Type u_3} [Finite ι] [Finite U] (F : (ι → U) → O → U) (X : Set ι) (Y : Set O) (x : ι → U) : (mixedFiber F X Y x).ncard ≤ maxMixedFiber F X Y

def Complexity.Frontier.OutputSplicing {ι : Type u_1} {O : Type u_2} {U : Type u_3} {M : Type u_4} (F : (ι → U) → O → U) (X : Set ι) (Y : Set O) (message : (ι → U) → M) : Prop

A boundary code permits splicing the inputs on X while preserving the corresponding outputs on Y. This is an observational property, not a causal evaluation order.

Equations

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

theorem Complexity.Frontier.OutputSplicing.ncard_class_le {ι : Type u_1} {O : Type u_2} {U : Type u_3} {M : Type u_4} [Finite ι] [Finite U] {F : (ι → U) → O → U} {X : Set ι} {Y : Set O} {message : (ι → U) → M} (h : OutputSplicing F X Y message) (x : ι → U) : {y : ι → U | message y = message x}.ncard ≤ (mixedFiber F X Y x).ncard * (mixedFiber F Xᶜ Yᶜ x).ncard

A message class embeds in the product of two complementary mixed fibers.

theorem Complexity.Frontier.OutputSplicing.card_le {ι : Type u_1} {O : Type u_2} {U : Type u_3} {M : Type u_4} [Finite ι] [Finite U] {F : (ι → U) → O → U} {X : Set ι} {Y : Set O} {message : (ι → U) → M} (h : OutputSplicing F X Y message) : Nat.card U ^ Nat.card ι ≤ (Set.range message).ncard * (maxMixedFiber F X Y * maxMixedFiber F Xᶜ Yᶜ)

Mixed-fiber demand, in cardinal form. The number of used messages, multiplied by the two largest complementary fibers, must cover all inputs.

theorem Complexity.Frontier.OutputSplicing.injective {ι : Type u_1} {O : Type u_2} {U : Type u_3} {M : Type u_4} {F : (ι → U) → O → U} {X : Set ι} {Y : Set O} {message : (ι → U) → M} (h : OutputSplicing F X Y message) (hX : ∀ (x y : ι → U), Set.EqOn x y X → Set.EqOn (F x) (F y) Y → x = y) (hY : ∀ (x y : ι → U), Set.EqOn x y Xᶜ → Set.EqOn (F x) (F y) Yᶜ → x = y) : Function.Injective message

When both mixed observations are injective, the boundary code determines the input.

def Complexity.Frontier.Compiler.cutSignals {O : Type u_2} {U : Type u_3} {σ : Cslib.Circuits.Signature} {n s : ℕ} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (P : Set (Vertex p out)) : Set (Signal p out)

The signals on a cut, counted once each regardless of copy multiplicity.

Equations

• Complexity.Frontier.Compiler.cutSignals I P = Complexity.Frontier.Compiler.Edge.signal '' (Complexity.Frontier.Compiler.network p out I fun (x : O) => Set.univ).cut P

theorem Complexity.Frontier.Compiler.outputSplicing {O : Type u_2} {U : Type u_3} {σ : Cslib.Circuits.Signature} {n s : ℕ} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) (P : Set (Vertex p out)) : OutputSplicing (fun (x : Fin n → U) (o : O) => p.trace I x (out o)) ((network p out I fun (x : O) => Set.univ).readIn P) {o : O | Vertex.output o ∈ P} fun (x : Fin n → U) (w : ↑(cutSignals I P)) => p.trace I x ↑↑w

Distinct signal values on a compiled cut satisfy the mixed-output splicing interface.

theorem Complexity.Frontier.Compiler.pow_le_cutSignals_mul_fibers {O : Type u_2} {U : Type u_3} {σ : Cslib.Circuits.Signature} {n s : ℕ} [Finite O] {p : Cslib.Circuits.Program σ n s} {out : O → Cslib.Circuits.Wire n s} (I : Cslib.Circuits.Interpretation σ U) [Finite U] (P : Set (Vertex p out)) : Nat.card U ^ n ≤ Nat.card U ^ (cutSignals I P).ncard * (maxMixedFiber (fun (x : Fin n → U) (o : O) => p.trace I x (out o)) ((network p out I fun (x : O) => Set.univ).readIn P) {o : O | Vertex.output o ∈ P} * maxMixedFiber (fun (x : Fin n → U) (o : O) => p.trace I x (out o)) ((network p out I fun (x : O) => Set.univ).readIn P)ᶜ {o : O | Vertex.output o ∈ P}ᶜ)

Pointwise frontier demand for arbitrary maps. This bounds every cut by its mixed input-output ambiguity. Taking logarithms gives the additive demand formulation.