Finite row networks for grid tensors

DefinitionRow network of a grid tensor#✓fully proved

Merge every grid row into one vertex of a factored tensor network. The state and label carriers may be infinite; only the supplied alphabets are enumerated. Capacity metadata charges L per vertical edge and the supplied cut capacity for each active rectangle.

TensorNetwork.gridRowNetwork · 33 lines

def gridRowNetwork [Fintype ρ] [LinearOrder ρ] [Fintype γ] [LinearOrder γ]
    [DecidableEq A]
    (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (cutLabels : ((ρ × ρ) × (γ × γ)) → Finset T)
    (top bottom : ((ρ × ρ) × (γ × γ)) → A → A → T → ℤ)
    (cap : ((ρ × ρ) × (γ × γ)) → ℕ) (L : ℕ) :
    Factored ρ (γ → ρ × γ → A)
      ((γ → A) × ({k : γ × γ // k ∈ orderedPairs γ} → T)) := by
  classical
  exact
    { S := fun a => Fintype.piFinset fun i =>
        Fintype.piFinset fun w => if w = (a, i) then diagonalLabels else labels
      W := fun a z =>
        (∏ i, R (a, i) (z i)) *
          ∏ q ∈ orderedPairs γ,
            if z q.1 (a, q.2) = z q.2 (a, q.1) then 1 else 0
      Θ := fun a b => if a < b then
        (Fintype.piFinset fun _ : γ => labels) ×ˢ
          Fintype.piFinset fun k : {k : γ × γ // k ∈ orderedPairs γ} =>
            cutLabels ((a, b), k)
        else ∅
      f := fun a b z θ => if a < b then
        (∏ i, if z i (b, i) = θ.1 i then 1 else 0) *
          ∏ k : {k : γ × γ // k ∈ orderedPairs γ},
            top ((a, b), k) (z k.1.1 (b, k.1.2))
              (z k.1.2 (b, k.1.1)) (θ.2 k)
        else
          (∏ i, if z i (b, i) = θ.1 i then 1 else 0) *
            ∏ k : {k : γ × γ // k ∈ orderedPairs γ},
              bottom ((b, a), k) (z k.1.1 (b, k.1.2))
                (z k.1.2 (b, k.1.1)) (θ.2 k)
      c := fun a b => Fintype.card γ * L +
        ∑ k : γ × γ with k ∈ orderedPairs γ, cap ((min a b, max a b), k) }

Uses 3 · Used by 7

Statement usesInteger-valued factored tensor network · Integer-valued complete-graph tensor instance · Ordered pairs representing unordered pairs

Used byCapacity bound between grid rows · Shape bound for the grid row network · Size bound for the grid row network · Total capacity of the grid row network · Interaction between rows of the grid row network · Row interaction for enumerated left states · Grid row network computes the grid value

TheoremInteraction between rows of the grid row network#✓fully proved

The interaction between increasing rows is the rectangle-kernel product times vertical equality indicators. For finite alphabets, an equal vertical value contributes only when it is in labels.

TensorNetwork.gridRowNetwork_interaction · 17 lines

theorem gridRowNetwork_interaction [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] [DecidableEq A]
    (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (cutLabels : ((ρ × ρ) × (γ × γ)) → Finset T)
    (top bottom : ((ρ × ρ) × (γ × γ)) → A → A → T → ℤ)
    (cap : ((ρ × ρ) × (γ × γ)) → ℕ) (L : ℕ)
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ)
    (hG : ∀ ω x y u v,
      G ω x y u v = ∑ θ ∈ cutLabels ω, top ω x y θ * bottom ω u v θ)
    {a b : ρ} (hab : a < b) (z z' : γ → ρ × γ → A) :
    (gridRowNetwork labels diagonalLabels R cutLabels top bottom cap L).interaction
        a b z z' =
      (∏ i, if z i (b, i) = z' i (a, i) ∧ z i (b, i) ∈ labels then 1 else 0) *
        ∏ k : {k : γ × γ // k ∈ orderedPairs γ},
          G ((a, b), k)
            (z k.1.1 (b, k.1.2)) (z k.1.2 (b, k.1.1))
            (z' k.1.1 (a, k.1.2)) (z' k.1.2 (a, k.1.1))

Uses 6 · Used by 2

Statement usesInteraction of two states in a factored network · Integer-valued complete-graph tensor instance · Row network of a grid tensor · Ordered pairs representing unordered pairs

Proof usesInteger-valued factored tensor network · Label set of an unordered vertex pair

Used bySize bound for the grid row network · Row interaction for enumerated left states

TheoremRow interaction for enumerated left states#✓fully proved

When the left state is enumerated by the row network, the alphabet-membership condition is automatic, so the interaction recovers the source vertical-equality formula. The right state may be arbitrary because equality with an allowed left value already forces its vertical value.

TensorNetwork.gridRowNetwork_interaction_of_mem · 18 lines

theorem gridRowNetwork_interaction_of_mem [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] [DecidableEq A]
    (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (cutLabels : ((ρ × ρ) × (γ × γ)) → Finset T)
    (top bottom : ((ρ × ρ) × (γ × γ)) → A → A → T → ℤ)
    (cap : ((ρ × ρ) × (γ × γ)) → ℕ) (L : ℕ)
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ)
    (hG : ∀ ω x y u v,
      G ω x y u v = ∑ θ ∈ cutLabels ω, top ω x y θ * bottom ω u v θ)
    {a b : ρ} (hab : a < b) (z z' : γ → ρ × γ → A)
    (hz : z ∈ (gridRowNetwork labels diagonalLabels R cutLabels top bottom cap L).S a) :
    (gridRowNetwork labels diagonalLabels R cutLabels top bottom cap L).interaction
        a b z z' =
      (∏ i, if z i (b, i) = z' i (a, i) then 1 else 0) *
        ∏ k : {k : γ × γ // k ∈ orderedPairs γ},
          G ((a, b), k)
            (z k.1.1 (b, k.1.2)) (z k.1.2 (b, k.1.1))
            (z' k.1.1 (a, k.1.2)) (z' k.1.2 (a, k.1.1))

Uses 6 · Used by 1

Statement usesInteger-valued factored tensor network · Interaction of two states in a factored network · Integer-valued complete-graph tensor instance · Row network of a grid tensor · Ordered pairs representing unordered pairs

Proof usesInteraction between rows of the grid row network

Used byGrid row network computes the grid value

TheoremGrid row network computes the grid value#✓fully proved

If each rectangle kernel is the finite sum of its top and bottom factors, contracting the constructed row network gives the canonical finite grid value.

theorem gridRowNetwork_value [Fintype ρ] [LinearOrder ρ]
    [Fintype γ] [LinearOrder γ] [DecidableEq A]
    (labels diagonalLabels : Finset A) (R : Instance (ρ × γ) A)
    (G : ((ρ × ρ) × (γ × γ)) → A → A → A → A → ℤ)
    (cutLabels : ((ρ × ρ) × (γ × γ)) → Finset T)
    (top bottom : ((ρ × ρ) × (γ × γ)) → A → A → T → ℤ)
    (cap : ((ρ × ρ) × (γ × γ)) → ℕ) (L : ℕ)
    (hG : ∀ ω x y u v,
      G ω x y u v = ∑ θ ∈ cutLabels ω, top ω x y θ * bottom ω u v θ) :
    (gridRowNetwork labels diagonalLabels R cutLabels top bottom cap L).value =
      gridValue labels diagonalLabels R G

Uses 13

Statement usesValue of a factored tensor network · Integer-valued complete-graph tensor instance · Row network of a grid tensor · Finite grid tensor evaluation · Ordered pairs representing unordered pairs

Proof usesInteger-valued factored tensor network · Interaction of two states in a factored network · Directed labelings of a finite grid · Ordered rectangles of a finite grid · Row interaction for enumerated left states · Characterization of directed grid labelings · Membership in the ordered pairs · Applying a rectangle kernel to its diagonal ends

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.