The strand, and the two branches of a glue

The flag model itself — fragments, relabelling, disjoint union, and the single-pair gluing primitive — is defined in RS/Definitions.lean. This module carries the strand (the identity 2-fragment), the two branch equations of gluePair, and the sanity checks that closing the strand onto itself yields one free circle and no flags.

The strand

def RS.Fragment.strand : Fragment (Fin 2)

The strand: a single edge with two boundary flags and no internal vertices. The identity 2-fragment.

Equations

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

The two branches of a glue

theorem RS.Fragment.gluePair_eq_closed {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) : W.gluePair i j hij = W.gluePairClosed i j hclosed

The closed branch of gluePair.

theorem RS.Fragment.gluePair_eq_open {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) : W.gluePair i j hij = W.gluePairOpen i j hij hopen

The open branch of gluePair.

Sanity checks