Monotonicity of the interface re-indexing equivalences

The gluing chain transports corrected constrained values along label re-indexings; the through-factor is orientation-antisymmetric, so only monotone relabelings preserve the corrected value. This file certifies the chain's equivalences as order isomorphisms for the lexicographic order on sums:

• finSumFinOrderIso: finSumFinEquiv as an order isomorphism;
• interfaceStepOrderIso: the label re-indexing after gluing the top interface pair, as an order isomorphism;
• application lemmas (interfaceStepEquiv_apply_inl, interfaceStepEquiv_apply_inr) letting the chain rewrite states through the isos concretely, on top of the removals' value computations in Composition.lean.

Instance discipline. Mathlib carries a global Preorder (α ⊕ β) (the disjoint order, where inl and inr are incomparable), so a letI := sumLexLinearOrder α β does not reliably route </≤ notation to the lexicographic order — instance search can still pick the global disjoint order. Every statement here therefore pins the sum orders explicitly through the reducible aliases sumLexPreorder/sumLexLE/sumLexSubtypeLinearOrder/… below, which are definitionally the projections of sumLexLinearOrder.

Pinned instances for the lexicographic sum order

@[reducible, inline]

abbrev RS.sumLexPreorder (α β : Type) [LinearOrder α] [LinearOrder β] : Preorder (α ⊕ β)

The lexicographic preorder on a plain sum, as an explicit term (never registered as an instance): pin it with @ in statements.

Equations

• RS.sumLexPreorder α β = (RS.sumLexLinearOrder α β).toPreorder

@[reducible, inline]

abbrev RS.sumLexLE (α β : Type) [LinearOrder α] [LinearOrder β] : LE (α ⊕ β)

The lexicographic ≤ on a plain sum, as an explicit term.

Equations

• RS.sumLexLE α β = (RS.sumLexPreorder α β).toLE

@[reducible, inline]

abbrev RS.sumLexSubtypeLinearOrder (α β : Type) [LinearOrder α] [LinearOrder β] (p : α ⊕ β → Prop) : LinearOrder (Subtype p)

The linear order induced on a subtype of the lexicographically ordered sum.

Equations

• RS.sumLexSubtypeLinearOrder α β p = Subtype.instLinearOrder p

@[reducible, inline]

abbrev RS.sumLexSubtypePreorder (α β : Type) [LinearOrder α] [LinearOrder β] (p : α ⊕ β → Prop) : Preorder (Subtype p)

The preorder induced on a subtype of the lexicographically ordered sum.

Equations

• RS.sumLexSubtypePreorder α β p = (RS.sumLexSubtypeLinearOrder α β p).toPreorder

@[reducible, inline]

abbrev RS.sumLexSubtypeLE (α β : Type) [LinearOrder α] [LinearOrder β] (p : α ⊕ β → Prop) : LE (Subtype p)

The ≤ induced on a subtype of the lexicographically ordered sum.

Equations

• RS.sumLexSubtypeLE α β p = (RS.sumLexSubtypePreorder α β p).toLE

Strictly monotone equivalences of linear orders

theorem RS.strictMono_equiv_symm {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃ β) (h : StrictMono ⇑e) : StrictMono ⇑e.symm

The inverse of a strictly monotone equivalence between linear orders is strictly monotone.

def RS.orderIsoOfStrictMonoEquiv {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃ β) (h : StrictMono ⇑e) : α ≃o β

A strictly monotone equivalence between linear orders, as an order isomorphism (keeping the underlying equivalence on the nose).

Equations

• RS.orderIsoOfStrictMonoEquiv e h = e.toOrderIso ⋯ ⋯

@[simp]

theorem RS.orderIsoOfStrictMonoEquiv_apply {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃ β) (h : StrictMono ⇑e) (x : α) : (orderIsoOfStrictMonoEquiv e h) x = e x

The order isomorphism built from a strictly monotone equivalence acts as that equivalence.

@[simp]

theorem RS.orderIsoOfStrictMonoEquiv_toEquiv {α β : Type} [LinearOrder α] [LinearOrder β] (e : α ≃ β) (h : StrictMono ⇑e) : (orderIsoOfStrictMonoEquiv e h).toEquiv = e

And carries it as its underlying equivalence.

finSumFinEquiv is monotone for the lexicographic order

theorem RS.finSumFinEquiv_strictMono (m n : ℕ) : StrictMono ⇑finSumFinEquiv

finSumFinEquiv is strictly monotone for the lexicographic sum order: it lays the left block below the right.

def RS.finSumFinOrderIso (m n : ℕ) : Fin m ⊕ Fin n ≃o Fin (m + n)

finSumFinEquiv as an order isomorphism for the lexicographic order on Fin m ⊕ Fin n.

Equations

• RS.finSumFinOrderIso m n = RS.orderIsoOfStrictMonoEquiv finSumFinEquiv ⋯

@[simp]

theorem RS.finSumFinOrderIso_apply (m n : ℕ) (x : Fin m ⊕ Fin n) : (finSumFinOrderIso m n) x = finSumFinEquiv x

The order isomorphism acts as finSumFinEquiv.

@[simp]

theorem RS.finSumFinOrderIso_toEquiv (m n : ℕ) : (finSumFinOrderIso m n).toEquiv = finSumFinEquiv

And carries it as its underlying equivalence.

The removal equivalences are strictly monotone

theorem RS.finRemoveEquiv_symm_strictMono {n : ℕ} (a : Fin (n + 1)) : StrictMono ⇑(finRemoveEquiv a).symm

Reinstating a removed point is strictly monotone: succAbove shifts indices up without reordering them.

theorem RS.finRemoveEquiv_strictMono {n : ℕ} (a : Fin (n + 1)) : StrictMono ⇑(finRemoveEquiv a)

Hence removing a point is too.

theorem RS.rightRemoveEquiv_strictMono (t u : ℕ) : StrictMono ⇑(rightRemoveEquiv t u)

Removing label t on the right is strictly monotone.

The interface step is an order isomorphism

theorem RS.interfaceStepEquiv_apply_inl (s t u : ℕ) (v : Fin (s + t + 1)) (h : Sum.inl v ≠ Sum.inl ⟨s + t, ⋯⟩ ∧ Sum.inl v ≠ Sum.inr ⟨t, ⋯⟩) : (interfaceStepEquiv s t u) ⟨Sum.inl v, h⟩ = Sum.inl ((finRemoveEquiv ⟨s + t, ⋯⟩) ⟨v, ⋯⟩)

The step re-indexing on a surviving left label: the left removal, injected.

theorem RS.interfaceStepEquiv_apply_inr (s t u : ℕ) (w : Fin (t + 1 + u)) (h : Sum.inr w ≠ Sum.inl ⟨s + t, ⋯⟩ ∧ Sum.inr w ≠ Sum.inr ⟨t, ⋯⟩) : (interfaceStepEquiv s t u) ⟨Sum.inr w, h⟩ = Sum.inr ((rightRemoveEquiv t u) ⟨w, ⋯⟩)

The step re-indexing on a surviving right label: the right removal, injected.

theorem RS.interfaceStepEquiv_strictMono (s t u : ℕ) : StrictMono ⇑(interfaceStepEquiv s t u)

The step re-indexing is strictly monotone for the lexicographic order: left labels stay below right ones and each block's removal preserves order. This is what lets the gluing chain carry corrected values, the through-factor being orientation-antisymmetric.

noncomputable def RS.interfaceStepOrderIso (s t u : ℕ) : { x : Fin (s + t + 1) ⊕ Fin (t + 1 + u) // x ≠ Sum.inl ⟨s + t, ⋯⟩ ∧ x ≠ Sum.inr ⟨t, ⋯⟩ } ≃o Fin (s + t) ⊕ Fin (t + u)

The interface-step re-indexing (interfaceStepEquiv) as an order isomorphism for the lexicographic orders.

Equations

• RS.interfaceStepOrderIso s t u = RS.orderIsoOfStrictMonoEquiv (RS.interfaceStepEquiv s t u) ⋯

@[simp]

theorem RS.interfaceStepOrderIso_apply (s t u : ℕ) (x : { x : Fin (s + t + 1) ⊕ Fin (t + 1 + u) // x ≠ Sum.inl ⟨s + t, ⋯⟩ ∧ x ≠ Sum.inr ⟨t, ⋯⟩ }) : (interfaceStepOrderIso s t u) x = (interfaceStepEquiv s t u) x

The step order isomorphism acts as the step equivalence.

@[simp]

theorem RS.interfaceStepOrderIso_toEquiv (s t u : ℕ) : (interfaceStepOrderIso s t u).toEquiv = interfaceStepEquiv s t u

And carries it as its underlying equivalence.