The fibre parametrization

The colouring of an edge subset with colouring data: participating flags carry the odd edge colour on the representative slot and its partner on the partner slot; the rest carry the even colour.

noncomputable def RS.colouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : MixedColouring k ℓ (edgeCount W + edgeCount W)

The colouring of an edge subset with colouring data.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.colourFlags_colouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : colourFlags W (colouringOf W F ψ φ) = F.flags

The pattern of the data colouring is the subset.

theorem RS.EdgeSubset.card_even {α : Type} {W : Fragment α} (F : EdgeSubset W) : Even F.flags.card

Closed subsets have evenly many flags.

theorem RS.colouringOf_isEven {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : (colouringOf W F ψ φ).IsEven

The data colouring is even.

def RS.diagPartner {k ℓ : ℕ} (x : Fin k ⊕ Fin (2 * ℓ)) : Fin k ⊕ Fin (2 * ℓ)

The diagonal partner of a colour: even colours repeat, odd colours pair symplectically.

Equations

• RS.diagPartner (Sum.inl a) = Sum.inl a
• RS.diagPartner (Sum.inr u) = Sum.inr (RS.oddPartner ℓ u)

def RS.Diagonal {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) : Prop

Diagonal colourings: the partner slot carries the diagonal partner of the representative slot.

Equations

• RS.Diagonal W c = ∀ (i : Fin (RS.edgeCount W)), c (Fin.natAdd (RS.edgeCount W) i) = RS.diagPartner (c (Fin.castAdd (RS.edgeCount W) i))

theorem RS.colouringOf_diagonal {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : Diagonal W (colouringOf W F ψ φ)

The data colouring is diagonal.

theorem RS.mem_colourFlags_iff {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (g : W.Flag) : g ∈ colourFlags W c ↔ (c ((starFlagEnum W) g)).isRight = true

Pattern membership is slot oddness.

noncomputable def RS.evenDataOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hfibre : colourFlags W c = F.flags) : { f : W.Flag // f ∉ F.flags } → Fin k

The even data of a pattern colouring.

Equations

• RS.evenDataOf W F c hfibre p = (c ((RS.starFlagEnum W) ↑p)).getLeft ⋯

theorem RS.isRight_of_mem {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hfibre : colourFlags W c = F.flags) (g : W.Flag) (hg : g ∈ F.flags) : (c ((starFlagEnum W) g)).isRight = true

Slot oddness of a participating flag.

noncomputable def RS.oddDataOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hfibre : colourFlags W c = F.flags) : ↥F.flags → Fin (2 * ℓ)

The odd data of a pattern colouring: the value at the representative slot of the flag's edge.

Equations

• RS.oddDataOf W F c hfibre p = if ↑((RS.starFlagEnum W) ↑p) < RS.edgeCount W then (c ((RS.starFlagEnum W) ↑p)).getRight ⋯ else (c ((RS.starFlagEnum W) (W.pairing ↑p))).getRight ⋯

theorem RS.starFlagEnum_pairing_low (W : ClosedFragment) (g : W.Flag) (h : ↑((starFlagEnum W) g) < edgeCount W) : (starFlagEnum W) (W.pairing g) = Fin.natAdd (edgeCount W) ⟨↑((starFlagEnum W) g), h⟩

The pairing flips low slots high.

theorem RS.starFlagEnum_pairing_high (W : ClosedFragment) (g : W.Flag) (h : ¬↑((starFlagEnum W) g) < edgeCount W) : (starFlagEnum W) (W.pairing g) = Fin.castAdd (edgeCount W) ⟨↑((starFlagEnum W) g) - edgeCount W, ⋯⟩

The pairing flips high slots low.

theorem RS.oddDataOf_constancy {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hfibre : colourFlags W c = F.flags) (p : ↥F.flags) : oddDataOf W F c hfibre ⟨W.pairing ↑p, ⋯⟩ = oddDataOf W F c hfibre p

The odd data is pairing-constant.

theorem RS.evenDataOf_constancy {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hfibre : colourFlags W c = F.flags) (hdiag : Diagonal W c) (p : { f : W.Flag // f ∉ F.flags }) : evenDataOf W F c hfibre ⟨W.pairing ↑p, ⋯⟩ = evenDataOf W F c hfibre p

The even data is pairing-constant on diagonal colourings.

noncomputable def RS.evenColouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hfibre : colourFlags W c = F.flags) (hdiag : Diagonal W c) : F.EvenColouring k

The even colouring of a diagonal pattern colouring.

Equations

• RS.evenColouringOf W F c hfibre hdiag = ⟨RS.evenDataOf W F c hfibre, ⋯⟩

noncomputable def RS.oddColouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hfibre : colourFlags W c = F.flags) : F.OddColouring ℓ

The odd colouring of a pattern colouring.

Equations

• RS.oddColouringOf W F c hfibre = ⟨RS.oddDataOf W F c hfibre, ⋯⟩

theorem RS.colouringOf_reconstruct {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hfibre : colourFlags W c = F.flags) (hdiag : Diagonal W c) : colouringOf W F (evenColouringOf W F c hfibre hdiag) (oddColouringOf W F c hfibre) = c

Reconstruction: a diagonal pattern colouring is the data colouring of its extracted data.

theorem RS.oddColouringOf_colouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : oddColouringOf W F (colouringOf W F ψ φ) ⋯ = φ

Round trip, odd data: extraction inverts construction.

theorem RS.evenColouringOf_colouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : evenColouringOf W F (colouringOf W F ψ φ) ⋯ ⋯ = ψ

Round trip, even data.