The diagonal cap pairing

The colour-side closed form of the cap value, defined by the very recursion the peel induction produces: the peel coefficient at the peeled colouring times the split factor — the smaller diagonal against the two-position form entry, vanishing on odd halves.

def RS.peelColour {k ℓ : ℕ} (m : ℕ) (c : MixedColouring k ℓ (m + 1 + (m + 1))) : MixedColouring k ℓ (m + m + 2)

The peeled colouring: the inverse peel reindex.

Equations

• RS.peelColour m c j = c ((RS.capPeelPerm m)⁻¹ ((finCongr ⋯).symm j))

theorem RS.peelColour_spec {k ℓ : ℕ} (m : ℕ) (c : MixedColouring k ℓ (m + 1 + (m + 1))) : (peelColour m c ∘ ⇑(finCongr ⋯)) ∘ ⇑(capPeelPerm m) = c

The peeled colouring undoes the peel reindex.

theorem RS.eq_peelColour_of {k ℓ : ℕ} (m : ℕ) {c : MixedColouring k ℓ (m + 1 + (m + 1))} {c' : MixedColouring k ℓ (m + m + 2)} (hspec : (c' ∘ ⇑(finCongr ⋯)) ∘ ⇑(capPeelPerm m) = c) : c' = peelColour m c

The peeled colouring is the unique solution of the peel reindex equation.

theorem RS.peelColour_isEven {k ℓ : ℕ} (m : ℕ) {c : MixedColouring k ℓ (m + 1 + (m + 1))} (hc : c.IsEven) : (peelColour m c).IsEven

The peeled colouring preserves parity.

theorem RS.peelColour_apply {k ℓ : ℕ} (m : ℕ) (c : MixedColouring k ℓ (m + 1 + (m + 1))) (j : Fin (m + m + 2)) : peelColour m c j = c ⟨capPeelInv m ↑j, ⋯⟩

The peeled colouring on values.

theorem RS.peelColour_low {k ℓ : ℕ} (m : ℕ) (c : MixedColouring k ℓ (m + 1 + (m + 1))) (j : Fin (m + m + 2)) (h : ↑j < m) : peelColour m c j = c ⟨↑j, ⋯⟩

The peel fixes the low first-half slots.

theorem RS.peelColour_pairSnd {k ℓ : ℕ} (m : ℕ) (c : MixedColouring k ℓ (m + 1 + (m + 1))) : peelColour m c ⟨m + m + 1, ⋯⟩ = c ⟨m + 1 + m, ⋯⟩

The second peeled-pair slot carries the last slot.

noncomputable def RS.betaDiag {k ℓ : ℕ} (m : ℕ) : MixedColouring k ℓ (m + m) → ℂ

The diagonal cap pairing: the colour-side cap value.

Equations

• One or more equations did not get rendered due to their size.
• RS.betaDiag 0 x_2 = 1

theorem RS.betaDiag_zero {k ℓ : ℕ} (c : MixedColouring k ℓ 0) : betaDiag 0 c = 1

The base of the diagonal pairing.

theorem RS.betaDiag_succ {k ℓ : ℕ} (m : ℕ) (c : MixedColouring k ℓ (m + 1 + (m + 1))) : betaDiag (m + 1) c = wordSign (adjWord (capPeelPerm m)) (peelColour m c ∘ ⇑(finCongr ⋯)) * if _h : (peelColour m c).firstHalf.IsEven then betaDiag m (peelColour m c).firstHalf * colourFormEntry k ℓ ((peelColour m c).secondHalf 0) ((peelColour m c).secondHalf 1) else 0

The successor equation of the diagonal pairing.