Fragment composition

Composition of fragments (Fragment.compose, defined in RS/Definitions.lean) glues the last t boundary labels of an (s + t)-fragment to the first t of a (t + u)-fragment through the iterated single-pair primitive, re-indexing the surviving labels by one-point removals.

This module carries the value computations for those removals: the gluing chain rewrites boundary states through the re-indexings, so it needs each surviving label's new index as an explicit natural number.

Value computation for the one-point removals

A removal is inverted by Fin.succAbove, which shifts the indices at or above the removed point up by one. Reading that off gives each surviving label's new index as an explicit natural number.

theorem RS.finRemoveEquiv_apply_val {n : ℕ} (a : Fin (n + 1)) (x : { x : Fin (n + 1) // x ≠ a }) : a.succAbove ((finRemoveEquiv a) x) = ↑x

Fin.succAbove at the removed point inverts finRemoveEquiv.

theorem RS.finRemoveEquiv_val {n : ℕ} (a : Fin (n + 1)) (x : { x : Fin (n + 1) // x ≠ a }) : ↑((finRemoveEquiv a) x) = if ↑↑x < ↑a then ↑↑x else ↑↑x - 1

The index a surviving label takes after a one-point removal.

theorem RS.finRemoveEquiv_top_val {n : ℕ} (x : { x : Fin (n + 1) // x ≠ ⟨n, ⋯⟩ }) : ↑((finRemoveEquiv ⟨n, ⋯⟩) x) = ↑↑x

Removing the top point leaves every surviving label's index unchanged.

theorem RS.rightRemoveEquiv_apply_val (t u : ℕ) (x : { x : Fin (t + 1 + u) // x ≠ ⟨t, ⋯⟩ }) : ↑(⟨t, ⋯⟩.succAbove ((rightRemoveEquiv t u) x)) = ↑↑x

Fin.succAbove at t inverts rightRemoveEquiv.

theorem RS.rightRemoveEquiv_val (t u : ℕ) (x : { x : Fin (t + 1 + u) // x ≠ ⟨t, ⋯⟩ }) : ↑((rightRemoveEquiv t u) x) = if ↑↑x < t then ↑↑x else ↑↑x - 1

The index a surviving label takes after removing label t on the right.