Boundary chord labels

The label of a boundary flag, extraction lemmas, and the crossing relation rewritten as an order condition on the four labels — the concrete bridge from chordCrossingCount to the abstract chord parity layer.

noncomputable def RS.EdgeSubset.boundaryLabel {α : Type} {W : Fragment α} (F : EdgeSubset W) {f : W.Flag} (hf : f ∈ F.boundaryFlags) : α

The boundary label of a boundary flag.

Equations

• F.boundaryLabel hf = Classical.choose ⋯

theorem RS.EdgeSubset.attach_boundaryLabel {α : Type} {W : Fragment α} {F : EdgeSubset W} {f : W.Flag} (hf : f ∈ F.boundaryFlags) : W.attach f = Sum.inr (F.boundaryLabel hf)

The defining equation of the boundary label.

theorem RS.EdgeSubset.boundaryLabel_eq_of_attach {α : Type} {W : Fragment α} {F : EdgeSubset W} {f : W.Flag} {i : α} (hf : f ∈ F.boundaryFlags) (h : W.attach f = Sum.inr i) : F.boundaryLabel hf = i

The label determines the attachment.

theorem RS.EdgeSubset.boundaryFlag_boundaryLabel {α : Type} {W : Fragment α} {f : W.Flag} {F : EdgeSubset W} (hf : f ∈ F.boundaryFlags) : W.boundaryFlag (F.boundaryLabel hf) = f

A boundary flag is the flag of its own label.

theorem RS.EdgeSubset.boundaryLabel_inj {α : Type} {W : Fragment α} {F : EdgeSubset W} {f g : W.Flag} (hf : f ∈ F.boundaryFlags) (hg : g ∈ F.boundaryFlags) (h : F.boundaryLabel hf = F.boundaryLabel hg) : f = g

Distinct boundary flags carry distinct labels.

theorem RS.EdgeSubset.boundaryLabel_congr {α : Type} {W : Fragment α} {F : EdgeSubset W} {f g : W.Flag} (hf : f ∈ F.boundaryFlags) (hg : g ∈ F.boundaryFlags) (h : f = g) : F.boundaryLabel hf = F.boundaryLabel hg

The boundary label does not depend on the membership proof.

theorem RS.EdgeSubset.chordCross_iff_labels {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (b b' : ↥F.boundaryFlags) : ChordCross κ b b' ↔ F.boundaryLabel ⋯ < F.boundaryLabel ⋯ ∧ F.boundaryLabel ⋯ < F.boundaryLabel ⋯ ∧ F.boundaryLabel ⋯ < F.boundaryLabel ⋯ ∧ F.boundaryLabel ⋯ < F.boundaryLabel ⋯ ∧ F.boundaryLabel ⋯ < F.boundaryLabel ⋯

The crossing relation on labels: ChordCross is exactly the four-label interleaving condition (each chord low-to-high, the first chord starting first).

theorem RS.sum_quad {β : Type} [DecidableEq β] {x y z w : β} (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) (f : β → ℕ) : ∑ t ∈ {x, y, z, w}, f t = f x + (f y + (f z + f w))

Expansion of a sum over a four-element finset literal.