# SPDX-License-Identifier: MPL-2.0

# isotopy.tangle — Exploring isotopy equivalence

#

# The key insight of TANGLE: two braids can be structurally different

# (different sequences of generators) but topologically equivalent

# (same knot/link when closed). The `~` operator checks this.

#

# Demonstrates:

# - Isotopy equivalence vs structural equality (D1.2)

# - Reidemeister moves (D1.16)

# - The deep duality between syntax and topology

# --- Reidemeister II: inverse cancellation ---

# s1 followed by s1^-1 is isotopic to doing nothing

assert braid[s1, s1^-1] ~ identity

# This works at any position in the word

assert braid[s2, s1, s1^-1, s2] ~ braid[s2, s2]

# But structurally they are NOT equal

assert braid[s1, s1^-1] == braid[s1, s1^-1]

# --- Far commutativity ---

# Generators on distant strands can commute: s1 s3 = s3 s1

# (because |1-3| >= 2)

# s1 and s3 commute, so s1 s3 s1^-1 ~ s3

assert simplify(braid[s1, s3, s1^-1]) ~ braid[s3]

# --- Self-isotopy ---

# Every braid is isotopic to itself

assert braid[s1, s2, s1] ~ braid[s1, s2, s1]

assert identity ~ identity

# --- Isotopy of closed braids ---

# The closure of isotopic braids gives the same knot

assert close(braid[s1, s1^-1]) ~ close(identity)

# --- Pipeline and composition are isotopic ---

# >> is syntactic sugar for . (D1.20)

assert (braid[s1] >> braid[s2]) ~ (braid[s1] . braid[s2])