Capacity of boundary codes #
An encoding must determine the entire transition: both adjacent boundary states and the newly read inputs. Bounding each boundary separately would incorrectly omit the cost of joining them. Any finite code with this property can replace the ambient wire alphabet.
theorem
Complexity.Frontier.Sweep.transitionCount_le_codes
{ι : Type u_1}
{U : Type u_2}
{M : Type u_3}
[Finite ι]
[Finite U]
{S : Set (ι → U)}
(P : Sweep S M)
{D : ℕ → Type u_4}
(code : (t : ℕ) → (ι → U) → D t)
(C : (t : ℕ) → Set (D t))
(hC : ∀ t < P.length, (C t).Finite)
(hmem : ∀ t < P.length, ∀ x ∈ S, code t x ∈ C t)
(hdet : ∀ t < P.length, ∀ x ∈ S, ∀ y ∈ S, code t x = code t y → P.transition t x = P.transition t y)
:
Count used transitions by any finite code that determines them on accepted inputs.
theorem
Complexity.Frontier.Sweep.abs_sumOn_le_codes
{ι : Type u_1}
{U : Type u_2}
{M : Type u_3}
[Finite ι]
[Finite U]
{S : Set (ι → U)}
(P : Sweep S M)
(hP : P.Coherent)
(hL : 0 < P.length)
{D : ℕ → Type u_4}
(code : (t : ℕ) → (ι → U) → D t)
(C : (t : ℕ) → Set (D t))
(hC : ∀ t < P.length, (C t).Finite)
(hmem : ∀ t < P.length, ∀ x ∈ S, code t x ∈ C t)
(hdet : ∀ t < P.length, ∀ x ∈ S, ∀ y ∈ S, code t x = code t y → P.transition t x = P.transition t y)
{KL KR : ℕ}
(hKL : 1 < KL)
(hKR : 1 < KR)
{w cost : (ι → U) → ℝ}
{a : ℝ}
(ha : 0 ≤ a)
(hw : ∀ (x : ι → U), |w x| ≤ a)
(hc : ∀ (x : ι → U), 0 ≤ cost x)
(hrect : RectangleBudget w cost KL KR)
:
Weighted peeling with code capacity in place of the number of boundary wires.
theorem
Complexity.Frontier.Sweep.transitionCount_le_linear_codes
{ι : Type u_1}
{F : Type u_2}
{M : Type u_3}
{W : Type u_4}
[Finite ι]
[Field F]
[Finite F]
[AddCommGroup W]
[Module F W]
{S : Set (ι → F)}
(P : Sweep S M)
(L : ℕ → (ι → F) →ₗ[F] W)
(hdet : ∀ t < P.length, ∀ x ∈ S, ∀ y ∈ S, (L t) x = (L t) y → P.transition t x = P.transition t y)
:
Affine dependence can be charged by rank: equality of the linear parts is enough to determine the entire transition, and a fixed translation does not affect this test.