State padding preserves tensor-network values

3 fully proved

Tensor Network

TheoremState padding preserves the weighted pair sum#✓fully proved

Padding the finite state sets preserves the full sum of vertex weights and arbitrary pair kernels. No factorization, finiteness of the state carriers, or global injectivity is required.

TensorNetwork.sum_statePadding · 15 lines

theorem sum_statePadding [Fintype J] [LinearOrder J]
    (S₀ : J → Finset σ₀) (S₁ : J → Finset σ₁)
    (W₀ : J → σ₀ → ℤ) (W₁ : J → σ₁ → ℤ)
    (K₀ : J → J → σ₀ → σ₀ → ℤ) (K₁ : J → J → σ₁ → σ₁ → ℤ)
    (pad : J → σ₀ → σ₁)
    (maps : ∀ a, ∀ z ∈ S₀ a, pad a z ∈ S₁ a)
    (inj : ∀ a, ∀ z ∈ S₀ a, ∀ z' ∈ S₀ a, pad a z = pad a z' → z = z')
    (off : ∀ a, ∀ y ∈ S₁ a, (∀ z ∈ S₀ a, pad a z ≠ y) → W₁ a y = 0)
    (weights : ∀ a, ∀ z ∈ S₀ a, W₁ a (pad a z) = W₀ a z)
    (kernels : ∀ a b, a ≠ b → ∀ z ∈ S₀ a, ∀ z' ∈ S₀ b,
      K₁ a b (pad a z) (pad b z') = K₀ a b z z') :
    (∑ y ∈ Fintype.piFinset S₁, (∏ a, W₁ a (y a)) *
      ∏ p ∈ orderedPairs J, K₁ p.1 p.2 (y p.1) (y p.2)) =
    ∑ z ∈ Fintype.piFinset S₀, (∏ a, W₀ a (z a)) *
      ∏ p ∈ orderedPairs J, K₀ p.1 p.2 (z p.1) (z p.2)

Uses 2 · Used by 1

Statement usesOrdered pairs representing unordered pairs

Proof usesMembership in the ordered pairs

Used byState padding preserves value and total capacity

Factored

StructureState padding of a factored tensor network#✓fully proved

The source's local padding protocol for factored networks. The factor clause is retained on source states and source labels, even though value preservation uses the interaction clause. Only capacities between distinct vertices must agree.

TensorNetwork.Factored.StatePadding · 18 lines

structure StatePadding [LinearOrder J]
    (N₀ : Factored J σ₀ τ) (N₁ : Factored J σ₁ τ) (pad : J → σ₀ → σ₁) : Prop where
  /-- Allowed source states map to allowed target states. -/
  maps : ∀ a, ∀ z ∈ N₀.S a, pad a z ∈ N₁.S a
  /-- Padding is injective on the allowed states of each vertex. -/
  inj : ∀ a, ∀ z ∈ N₀.S a, ∀ z' ∈ N₀.S a, pad a z = pad a z' → z = z'
  /-- Target states outside the padding image have zero vertex weight. -/
  off : ∀ a, ∀ y ∈ N₁.S a, (∀ z ∈ N₀.S a, pad a z ≠ y) → N₁.W a y = 0
  /-- Vertex weights agree on padded source states. -/
  W : ∀ a, ∀ z ∈ N₀.S a, N₁.W a (pad a z) = N₀.W a z
  /-- Pair interactions agree on padded source states at distinct vertices. -/
  interaction : ∀ a b, a ≠ b → ∀ z ∈ N₀.S a, ∀ z' ∈ N₀.S b,
    N₁.interaction a b (pad a z) (pad b z') = N₀.interaction a b z z'
  /-- Directed capacities agree off the diagonal. -/
  c : ∀ a b, a ≠ b → N₁.c a b = N₀.c a b
  /-- Directed factors agree on source states and source labels. -/
  f : ∀ a b, a ≠ b → ∀ z ∈ N₀.S a, ∀ θ ∈ N₀.labelSet a b,
    N₁.f a b (pad a z) θ = N₀.f a b z θ

Uses 3 · Used by 1

Statement usesInteger-valued factored tensor network · Interaction of two states in a factored network · Label set of an unordered vertex pair

Used byState padding preserves value and total capacity

TheoremState padding preserves value and total capacity#✓fully proved

A local state-padding certificate preserves both network value and directed total capacity.

theorem StatePadding.value_totalCapacity [Fintype J] [LinearOrder J]
    {N₀ : Factored J σ₀ τ} {N₁ : Factored J σ₁ τ} {pad : J → σ₀ → σ₁}
    (h : StatePadding N₀ N₁ pad) :
    N₁.value = N₀.value ∧ N₁.totalCapacity = N₀.totalCapacity

Uses 6

Statement usesInteger-valued factored tensor network · State padding of a factored tensor network · Directed total capacity of a factored network · Value of a factored tensor network

Proof usesInteraction of two states in a factored network · State padding preserves the weighted pair sum

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.