The merge coordinate product rule, odd input

Coordinates of a merged odd-even pair multiply over the halves, vanishing when the first half has even parity — the odd-input counterpart of ColourMerge.lean, whose split-equivalence, tensor-step and right-hand-side helpers it shares.

The four chain reductions run on the four parity patterns of a pure tensor, and the two parts of colourMerge_pair_odd are proved by one mutual induction on the second arity.

Parity helpers for the odd input

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 even and the first half is odd, the second half is odd.

Full chain reduction on pure tensor generators (odd input)

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

The merge coordinate product rule (odd input): coordinates of a merged odd-even pair multiply over the halves, vanishing when the first half is even.

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

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

theorem RS.single_val_ne {k ℓ n : ℕ} {p : MixedColouring k ℓ n → Prop} (x y : { c : MixedColouring k ℓ n // p c }) (h : ↑y ≠ ↑x) : Pi.single x 1 y = 0

Subtype coordinate singles evaluate by values: different.

theorem RS.single_val_same {k ℓ n : ℕ} {p : MixedColouring k ℓ n → Prop} (x y : { c : MixedColouring k ℓ n // p c }) (h : ↑x = ↑y) : Pi.single x 1 y = 1

Subtype coordinate singles evaluate by values: same.