The merge coordinate product rule

Coordinates of a merged even pair multiply over the halves, vanishing when the halves have odd parity.

First and second halves of a colouring

def RS.MixedColouring.firstHalf {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + b)) : MixedColouring k ℓ a

The first half of a colouring of a sum.

Equations

• c.firstHalf i = c (Fin.castAdd b i)

def RS.MixedColouring.secondHalf {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + b)) : MixedColouring k ℓ b

The second half of a colouring of a sum.

Equations

• c.secondHalf j = c (Fin.natAdd a j)

theorem RS.MixedColouring.oddSet_card_split {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + b)) : c.oddSet.card = c.firstHalf.oddSet.card + c.secondHalf.oddSet.card

The odd count splits over the halves.

Helper lemmas

theorem RS.MixedColouring.firstHalf_zero {k ℓ a : ℕ} (c : MixedColouring k ℓ (a + 0)) : c.firstHalf = c

The first half at b = 0 is the colouring itself.

theorem RS.MixedColouring.firstHalf_tail {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + (b + 1))) : c.tail.firstHalf = c.firstHalf

The first half of a tail equals the first half.

theorem RS.MixedColouring.secondHalf_tail {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + (b + 1))) : c.tail.secondHalf = c.secondHalf.tail

The second half of a tail equals the tail of the second half.

theorem RS.MixedColouring.isEven_half_iff {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + b)) (hc : c.IsEven) : c.firstHalf.IsEven ↔ c.secondHalf.IsEven

Parity of the halves is linked when the whole is even.

theorem RS.MixedColouring.secondHalf_isEven {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + b)) (hc : c.IsEven) (h : c.firstHalf.IsEven) : c.secondHalf.IsEven

When the whole is even and the first half is even, the second half is even.

theorem RS.MixedColouring.secondHalf_not_isEven {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + b)) (hc : ¬c.IsEven) (h : c.firstHalf.IsEven) : ¬c.secondHalf.IsEven

When the whole is odd and the first half is even, the second half is odd.

theorem RS.MixedColouring.secondHalf_last {k ℓ a b : ℕ} (c : MixedColouring k ℓ (a + (b + 1))) : c.secondHalf (Fin.last b) = c (Fin.last (a + b))

The last colour of c equals the last colour of the second half.

Forward computation of evenSplitEquiv

theorem RS.evenSplitEquiv_inl {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (hc : c.IsEven) (a' : Fin k) (ha : c (Fin.last d) = Sum.inl a') : (evenSplitEquiv k ℓ d) ⟨c, hc⟩ = Sum.inl (⟨c.tail, ⋯⟩, a')

Compute evenSplitEquiv forward via its inverse, last colour even.

theorem RS.evenSplitEquiv_inr {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (hc : c.IsEven) (b' : Fin (2 * ℓ)) (hb : c (Fin.last d) = Sum.inr b') : (evenSplitEquiv k ℓ d) ⟨c, hc⟩ = Sum.inr (⟨c.tail, ⋯⟩, b')

Compute evenSplitEquiv forward via its inverse, last colour odd.

Forward computation of oddSplitEquiv

theorem RS.oddSplitEquiv_inl {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (hc : ¬c.IsEven) (a' : Fin k) (ha : c (Fin.last d) = Sum.inl a') : (oddSplitEquiv k ℓ d) ⟨c, hc⟩ = Sum.inl (⟨c.tail, ⋯⟩, a')

Compute oddSplitEquiv forward via its inverse, last colour even.

theorem RS.oddSplitEquiv_inr {k ℓ d : ℕ} (c : MixedColouring k ℓ (d + 1)) (hc : ¬c.IsEven) (b' : Fin (2 * ℓ)) (hb : c (Fin.last d) = Sum.inr b') : (oddSplitEquiv k ℓ d) ⟨c, hc⟩ = Sum.inr (⟨c.tail, ⋯⟩, b')

Compute oddSplitEquiv forward via its inverse, last colour odd.

ColourPowerStep evaluation

theorem RS.cps_even_at_inl {k ℓ d : ℕ} (z₁ : TensorProduct ℂ ({ c : MixedColouring k ℓ d // c.IsEven } → ℂ) (Fin k → ℂ)) (z₂ : TensorProduct ℂ ({ c : MixedColouring k ℓ d // ¬c.IsEven } → ℂ) (Fin (2 * ℓ) → ℂ)) (c : MixedColouring k ℓ (d + 1)) (hc : c.IsEven) (a' : Fin k) (ha : c (Fin.last d) = Sum.inl a') : (colourPowerStep k ℓ d).evenEquiv (z₁, z₂) ⟨c, hc⟩ = (funTensorFun { c : MixedColouring k ℓ d // c.IsEven } (Fin k)) z₁ (⟨c.tail, ⋯⟩, a')

colourPowerStep.evenEquiv at a colouring whose last colour is even: the value comes from the even-even channel.

theorem RS.cps_even_at_inr {k ℓ d : ℕ} (z₁ : TensorProduct ℂ ({ c : MixedColouring k ℓ d // c.IsEven } → ℂ) (Fin k → ℂ)) (z₂ : TensorProduct ℂ ({ c : MixedColouring k ℓ d // ¬c.IsEven } → ℂ) (Fin (2 * ℓ) → ℂ)) (c : MixedColouring k ℓ (d + 1)) (hc : c.IsEven) (b' : Fin (2 * ℓ)) (hb : c (Fin.last d) = Sum.inr b') : (colourPowerStep k ℓ d).evenEquiv (z₁, z₂) ⟨c, hc⟩ = (funTensorFun { c : MixedColouring k ℓ d // ¬c.IsEven } (Fin (2 * ℓ))) z₂ (⟨c.tail, ⋯⟩, b')

colourPowerStep.evenEquiv at a colouring whose last colour is odd: the value comes from the odd-odd channel.

theorem RS.cps_odd_at_inl {k ℓ d : ℕ} (z₁ : TensorProduct ℂ ({ c : MixedColouring k ℓ d // c.IsEven } → ℂ) (Fin (2 * ℓ) → ℂ)) (z₂ : TensorProduct ℂ ({ c : MixedColouring k ℓ d // ¬c.IsEven } → ℂ) (Fin k → ℂ)) (c : MixedColouring k ℓ (d + 1)) (hc : ¬c.IsEven) (a' : Fin k) (ha : c (Fin.last d) = Sum.inl a') : (colourPowerStep k ℓ d).oddEquiv (z₁, z₂) ⟨c, hc⟩ = (funTensorFun { c : MixedColouring k ℓ d // ¬c.IsEven } (Fin k)) z₂ (⟨c.tail, ⋯⟩, a')

colourPowerStep.oddEquiv at a colouring whose last colour is even: the value comes from the odd-even channel.

theorem RS.cps_odd_at_inr {k ℓ d : ℕ} (z₁ : TensorProduct ℂ ({ c : MixedColouring k ℓ d // c.IsEven } → ℂ) (Fin (2 * ℓ) → ℂ)) (z₂ : TensorProduct ℂ ({ c : MixedColouring k ℓ d // ¬c.IsEven } → ℂ) (Fin k → ℂ)) (c : MixedColouring k ℓ (d + 1)) (hc : ¬c.IsEven) (b' : Fin (2 * ℓ)) (hb : c (Fin.last d) = Sum.inr b') : (colourPowerStep k ℓ d).oddEquiv (z₁, z₂) ⟨c, hc⟩ = (funTensorFun { c : MixedColouring k ℓ d // c.IsEven } (Fin (2 * ℓ))) z₁ (⟨c.tail, ⋯⟩, b')

colourPowerStep.oddEquiv at a colouring whose last colour is odd: the value comes from the even-odd channel.

Chain computation helpers

Full chain reduction on pure tensor generators

theorem RS.rhs_even_ee {k ℓ b : ℕ} (w₁ : (superPow (stdSuperPair k ℓ) b).even) (x₁ : (stdSuperPair k ℓ).even) : (colourPowerEquiv k ℓ (b + 1)).evenEquiv (w₁ ⊗ₜ[ℂ] x₁, 0) = (colourPowerStep k ℓ b).evenEquiv ((colourPowerEquiv k ℓ b).evenEquiv w₁ ⊗ₜ[ℂ] x₁, 0)

The RHS chain on a pure ee tensor: cpe(b+1) on (t ⊗ₜ x, 0) reduces to cps applied to the transported tensor.

theorem RS.rhs_even_oo {k ℓ b : ℕ} (w₂ : (superPow (stdSuperPair k ℓ) b).odd) (x₂ : (stdSuperPair k ℓ).odd) : (colourPowerEquiv k ℓ (b + 1)).evenEquiv (0, w₂ ⊗ₜ[ℂ] x₂) = (colourPowerStep k ℓ b).evenEquiv (0, (colourPowerEquiv k ℓ b).oddEquiv w₂ ⊗ₜ[ℂ] x₂)

The RHS chain on a pure oo tensor: cpe(b+1) on (0, s ⊗ₜ x) reduces to cps applied to the transported tensor.

theorem RS.rhs_odd_eo {k ℓ b : ℕ} (w₂ : (superPow (stdSuperPair k ℓ) b).even) (x₂ : (stdSuperPair k ℓ).odd) : (colourPowerEquiv k ℓ (b + 1)).oddEquiv (w₂ ⊗ₜ[ℂ] x₂, 0) = (colourPowerStep k ℓ b).oddEquiv ((colourPowerEquiv k ℓ b).evenEquiv w₂ ⊗ₜ[ℂ] x₂, 0)

The RHS chain on a pure eo tensor (odd part): cpe(b+1) on (t ⊗ₜ x, 0) reduces to cps applied to the transported tensor.

theorem RS.rhs_odd_oe {k ℓ b : ℕ} (w₁ : (superPow (stdSuperPair k ℓ) b).odd) (x₁ : (stdSuperPair k ℓ).even) : (colourPowerEquiv k ℓ (b + 1)).oddEquiv (0, w₁ ⊗ₜ[ℂ] x₁) = (colourPowerStep k ℓ b).oddEquiv (0, (colourPowerEquiv k ℓ b).oddEquiv w₁ ⊗ₜ[ℂ] x₁)

The RHS chain on a pure oe tensor (odd part): cpe(b+1) on (0, s ⊗ₜ x) reduces to cps applied to the transported tensor.

The merge coordinate product rule

theorem RS.colourMerge_coord {k ℓ : ℕ} (a b : ℕ) (v : (superPow (stdSuperPair k ℓ) a).even) (w : (superPow (stdSuperPair k ℓ) b).even) (c : MixedColouring k ℓ (a + b)) (hc : c.IsEven) : (colourPowerEquiv k ℓ (a + b)).evenEquiv ((powMerge (stdSuperPair k ℓ) a b).evenMap (evenPair v w)) ⟨c, hc⟩ = if h : c.firstHalf.IsEven then (colourPowerEquiv k ℓ a).evenEquiv v ⟨c.firstHalf, h⟩ * (colourPowerEquiv k ℓ b).evenEquiv w ⟨c.secondHalf, ⋯⟩ else 0

The merge coordinate product rule: coordinates of a merged even pair multiply over the halves, vanishing when the halves are odd.

theorem RS.colourMerge_coord_evenOdd {k ℓ : ℕ} (a b : ℕ) (v : (superPow (stdSuperPair k ℓ) a).even) (u : (superPow (stdSuperPair k ℓ) b).odd) (c : MixedColouring k ℓ (a + b)) (hc : ¬c.IsEven) : (colourPowerEquiv k ℓ (a + b)).oddEquiv ((powMerge (stdSuperPair k ℓ) a b).oddMap (v ⊗ₜ[ℂ] u, 0)) ⟨c, hc⟩ = if h : c.firstHalf.IsEven then (colourPowerEquiv k ℓ a).evenEquiv v ⟨c.firstHalf, h⟩ * (colourPowerEquiv k ℓ b).oddEquiv u ⟨c.secondHalf, ⋯⟩ else 0

The even-odd merge coordinate product rule: odd coordinates of a merged even-odd pair multiply over the halves, supported on even first halves.