Crossing data for free cancellation in braid closures

An inverse pair inserted at the top of a braid word contributes a Reidemeister-II clasp to its closure. This file records the local crossing data needed by the eventual diagrammatic identification: old crossings retain their signs, and the two new crossings have opposite signs and opposite over-pair indicators. The existing DoubleCrossing API supplies the two internal arcs; the remaining closure theorem must match the external arcs with a PDCode.insertClasp and prove its face condition.

The pair is appended so its crossing names are the final two Fin indices. This is the numbering used by PDCode.insertClasp, and lets later proofs compare old blocks by Fin.castAdd 2.

theorem TauCeti.BraidWord.crossingSign_closure_append_freeCancel_old {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε : ℤˣ) (j : Fin (List.length v)) : (v ++ [(i, ε), (i, -ε)]).closure.crossingSign (Fin.cast ⋯ (Fin.castAdd 2 j)) = v.closure.crossingSign j

The sign of an old crossing is unchanged when an inverse pair is appended.

theorem TauCeti.BraidWord.crossingSign_closure_append_freeCancel_first {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε : ℤˣ) : (v ++ [(i, ε), (i, -ε)]).closure.crossingSign ⟨List.length v, ⋯⟩ = ↑ε

The first crossing of an appended inverse pair has the sign of its letter.

theorem TauCeti.BraidWord.crossingSign_closure_append_freeCancel_second {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε : ℤˣ) : (v ++ [(i, ε), (i, -ε)]).closure.crossingSign ⟨List.length v + 1, ⋯⟩ = -↑ε

The second crossing of an appended inverse pair has the opposite sign.

theorem TauCeti.BraidWord.overPair_closure_append_freeCancel_second_eq_not_first {n : ℕ} (v : BraidWord n) (i : Fin (n - 1)) (ε : ℤˣ) : (v ++ [(i, ε), (i, -ε)]).closure.overPair ⟨List.length v + 1, ⋯⟩ = !(v ++ [(i, ε), (i, -ε)]).closure.overPair ⟨List.length v, ⋯⟩

Opposite appended letters produce opposite over-pair indicators at the two new crossings.