Nonlinear recovery maps

The graph code (x, F x) is MDS when any N of its 2N coordinates determine x. Every layout has a cut containing exactly N input and output terminals. The complementary mixed observations at that cut are both injective, so its signal values determine the input. Over a finite alphabet this gives the same circuit lower bound as total regularity.

def Complexity.Frontier.IsMDS {U : Type u} {N : ℕ} (F : (Fin N → U) → Fin N → U) : Prop

Any balanced mixed observation determines the input. Equivalently, any N coordinates of the systematic graph code (x, F x) determine its codeword.

Equations

• Complexity.Frontier.IsMDS F = ∀ (X Y : Set (Fin N)), X.ncard + Y.ncard = N → ∀ (x y : Fin N → U), Set.EqOn x y X → Set.EqOn (F x) (F y) Y → x = y

theorem Complexity.Frontier.IsMDS.mixedFiber_eq_singleton {U : Type u} {N : ℕ} {F : (Fin N → U) → Fin N → U} (hF : IsMDS F) {X Y : Set (Fin N)} (hXY : X.ncard + Y.ncard = N) (x : Fin N → U) : mixedFiber F X Y x = {x}

theorem Complexity.Frontier.upstream_of_mds {U : Type u} {N : ℕ} {σ : Cslib.Circuits.Signature} {I : Cslib.Circuits.Interpretation σ U} {c : Cslib.Circuits.Circuit σ N N} {F : (Fin N → U) → Fin N → U} [Nontrivial U] (hF : IsMDS F) (hc : c.Computes I F) (o i : Fin N) : c.program.Upstream (c.outputs o) (Cslib.Circuits.Wire.input i)

The MDS property forces every output to depend on every input.

theorem Complexity.Frontier.exists_balanced_terminal_cut {U : Type u} {N : ℕ} {σ : Cslib.Circuits.Signature} (I : Cslib.Circuits.Interpretation σ U) (c : Cslib.Circuits.Circuit σ N N) (π : Layout (Compiler.Vertex c.program c.outputs)) : ∃ (t : ℕ), ((Compiler.network c.program c.outputs I fun (x : Fin N) => Set.univ).readIn (π.initial t)).ncard + {o : Fin N | Compiler.Vertex.output o ∈ π.initial t}.ncard = N

Every layout passes a balanced input-output observation. This statement only needs the output terminals; some unused inputs are allowed.

theorem Complexity.Frontier.exists_injective_cut_mds {U : Type u} {N : ℕ} {σ : Cslib.Circuits.Signature} {I : Cslib.Circuits.Interpretation σ U} {c : Cslib.Circuits.Circuit σ N N} {F : (Fin N → U) → Fin N → U} (hF : IsMDS F) (hc : c.Computes I F) (π : Layout (Compiler.Vertex c.program c.outputs)) : ∃ (t : ℕ), Function.Injective fun (x : Fin N → U) (e : ↑((Compiler.network c.program c.outputs I fun (x : Fin N) => Set.univ).cut (π.initial t))) => c.program.trace I x ↑(↑e).signal

The frontier of a balanced cut determines the input of an MDS map.

theorem Complexity.Frontier.exists_graph_of_mds {U : Type u} {N : ℕ} {σ : Cslib.Circuits.Signature} {I : Cslib.Circuits.Interpretation σ U} {c : Cslib.Circuits.Circuit σ N N} {F : (Fin N → U) → Fin N → U} [Finite U] [Nontrivial U] (hN : 1 ≤ N) {r : ℕ} (hr : 2 ≤ r) (hfan : c.FanInAtMost r) (hF : IsMDS F) (hc : c.Computes I F) : ∃ (V : Type) (E : Type) (_ : Finite V) (_ : Finite E) (G : Multigraph V E), G.Connected ∧ G.Loopless ∧ G.MaxDegreeLE (r + 1) ∧ Nat.card V ≤ 2 * r * c.innerSize + 3 * N ∧ G.cycleRank + N ≤ (r - 1) * c.innerSize + 1 ∧ ∀ (π : Layout V), ∃ (t : ℕ), N ≤ (G.cut (π.initial t)).ncard

An MDS map supplies the same full-entropy graph demand as a totally regular matrix.

theorem Complexity.Frontier.lowerBound_mds {r : ℕ} (hr : 2 ≤ r) {A : ℝ} (hA : 0 < A) (hlayout : LayoutBound (r + 1) A) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (U : Type u) [Finite U] [Nontrivial U] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (F : (Fin N → U) → Fin N → U) (c : Cslib.Circuits.Circuit σ N N), IsMDS F → c.FanInAtMost r → c.Computes I F → (1 + 1 / A - ε) * ↑N < (↑r - 1) * ↑c.innerSize

Circuit lower bounds from mixed recovery. The alphabet and circuit basis are arbitrary; finiteness supplies the capacity bound.

theorem Complexity.Frontier.mds_gaussian {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (U : Type u) [Finite U] [Nontrivial U] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (F : (Fin N → U) → Fin N → U) (c : Cslib.Circuits.Circuit σ N N), IsMDS F → c.FanInAtMost 2 → c.Computes I F → (1 + Real.pi / (3 * Real.arccos ((1 + 2 * √2) / 4)) - ε) * ↑N < ↑c.innerSize

Nonlinear MDS maps inherit the binary Gaussian coefficient.

theorem Complexity.Frontier.mds_degree {r : ℕ} (hr : 2 ≤ r) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (U : Type u) [Finite U] [Nontrivial U] (σ : Cslib.Circuits.Signature) (I : Cslib.Circuits.Interpretation σ U) (F : (Fin N → U) → Fin N → U) (c : Cslib.Circuits.Circuit σ N N), IsMDS F → c.FanInAtMost r → c.Computes I F → (1 + 1 / Gaussian.degreeCoefficient (r + 1) - ε) * ↑N < (↑r - 1) * ↑c.innerSize

Every fixed fan-in for nonlinear MDS maps, with the Gaussian degree coefficient.

theorem Complexity.Frontier.IsMDS.permute {U : Type u} {N : ℕ} {F : (Fin N → U) → Fin N → U} (hF : IsMDS F) (before after : Fin N → Equiv.Perm U) : IsMDS fun (x : Fin N → U) (i : Fin N) => (after i) (F (fun (j : Fin N) => (before j) (x j)) i)

Coordinatewise alphabet permutations preserve the MDS graph-code property.

theorem Complexity.Frontier.TotallyRegular.isMDS {N : ℕ} {K : Type u_1} [Field K] {M : Matrix (Fin N) (Fin N) K} (hM : TotallyRegular M) : IsMDS fun (x : Fin N → K) => M.mulVec x

Total regularity is the linear special case of mixed recovery.