Linear boundary states

For a split linear system L x + R y = 0, the extendable syndromes are precisely range L ∩ range R. Two extendable left assignments have the same right completions exactly when their syndromes agree. Thus this is an exact boundary code, not just an upper bound obtained by counting its coordinates. Its dimension is the familiar matroid connectivity expression; see Kashyap, Matroid Pathwidth and Code Trellis Complexity.

def Complexity.Frontier.LinearBoundary.completions {F : Type u_1} {V : Type u_2} {Z : Type u_3} {W : Type u_4} [Field F] [AddCommGroup V] [Module F V] [AddCommGroup Z] [Module F Z] [AddCommGroup W] [Module F W] (L : V →ₗ[F] W) (R : Z →ₗ[F] W) (x : V) : Set Z

Right completions of a left assignment in a split homogeneous linear system.

Equations

• Complexity.Frontier.LinearBoundary.completions L R x = {y : Z | L x + R y = 0}

theorem Complexity.Frontier.LinearBoundary.completions_nonempty_iff {F : Type u_1} {V : Type u_2} {Z : Type u_3} {W : Type u_4} [Field F] [AddCommGroup V] [Module F V] [AddCommGroup Z] [Module F Z] [AddCommGroup W] [Module F W] (L : V →ₗ[F] W) (R : Z →ₗ[F] W) (x : V) : (completions L R x).Nonempty ↔ L x ∈ R.range

theorem Complexity.Frontier.LinearBoundary.completions_eq_iff {F : Type u_1} {V : Type u_2} {Z : Type u_3} {W : Type u_4} [Field F] [AddCommGroup V] [Module F V] [AddCommGroup Z] [Module F Z] [AddCommGroup W] [Module F W] (L : V →ₗ[F] W) (R : Z →ₗ[F] W) {x x' : V} (hx : (completions L R x).Nonempty) : completions L R x = completions L R x' ↔ L x = L x'

Distinct feasible syndromes have distinct completion sets.

theorem Complexity.Frontier.LinearBoundary.syndromes_eq {F : Type u_1} {V : Type u_2} {Z : Type u_3} {W : Type u_4} [Field F] [AddCommGroup V] [Module F V] [AddCommGroup Z] [Module F Z] [AddCommGroup W] [Module F W] (L : V →ₗ[F] W) (R : Z →ₗ[F] W) : ⇑L '' {x : V | (completions L R x).Nonempty} = ↑(L.range ⊓ R.range)

The feasible boundary code is the intersection of the two syndrome spaces.

theorem Complexity.Frontier.LinearBoundary.finrank_states {F : Type u_1} {V : Type u_2} {Z : Type u_3} {W : Type u_4} [Field F] [AddCommGroup V] [Module F V] [AddCommGroup Z] [Module F Z] [AddCommGroup W] [Module F W] (L : V →ₗ[F] W) (R : Z →ₗ[F] W) [FiniteDimensional F W] : Module.finrank F ↥(L.range ⊓ R.range) = Module.finrank F ↥L.range + Module.finrank F ↥R.range - Module.finrank F ↥(L.range ⊔ R.range)

The dimension of the boundary code is the connectivity of the two column spaces.

theorem Complexity.Frontier.LinearBoundary.ncard_syndromes {F : Type u_1} {V : Type u_2} {Z : Type u_3} {W : Type u_4} [Field F] [AddCommGroup V] [Module F V] [AddCommGroup Z] [Module F Z] [AddCommGroup W] [Module F W] (L : V →ₗ[F] W) (R : Z →ₗ[F] W) [FiniteDimensional F W] : (⇑L '' {x : V | (completions L R x).Nonempty}).ncard = Nat.card F ^ (Module.finrank F ↥L.range + Module.finrank F ↥R.range - Module.finrank F ↥(L.range ⊔ R.range))

Over a finite field the exact number of feasible syndromes is q^λ. The Nat.card identity also makes sense over infinite fields; only the finite case is a counting bound.

theorem Complexity.Frontier.LinearBoundary.ncard_syndromes_le_states {F : Type u_1} {V : Type u_2} {Z : Type u_3} {W : Type u_4} [Field F] [AddCommGroup V] [Module F V] [AddCommGroup Z] [Module F Z] [AddCommGroup W] [Module F W] (L : V →ₗ[F] W) (R : Z →ₗ[F] W) [Finite V] {D : Type u_5} (code : V → D) (hcode : ∀ (x : V), (completions L R x).Nonempty → ∀ (x' : V), (completions L R x').Nonempty → code x = code x' → completions L R x = completions L R x') : (⇑L '' {x : V | (completions L R x).Nonempty}).ncard ≤ (code '' {x : V | (completions L R x).Nonempty}).ncard

This many states are necessary as well as sufficient: any exact classifier of right completion sets must separate all feasible syndromes.