Partial closure: gluing a fragment into a test fragment

The accompanying paper's G_z (Lemma 3.3(b)): given a (u, v)-fragment z and a test fragment G on the interleaved boundary (s + u) + (t + v), glue each open end of z to the matching z-block end of G. The survivors are exactly the x-block ends of G, so the result is an (s + t)-fragment. The absorption theorem pairClose (tensorFragment x z) G ≃ pairClose x (partialClose z G) lives in TensorIdeal.lean; this file provides the construction: the gluing pair list, its well-formedness, the survivor identification, and congruence.

noncomputable def RS.zClosePairs (s t u v : ℕ) : List ((Fin (u + v) ⊕ Fin (s + u + (t + v))) × (Fin (u + v) ⊕ Fin (s + u + (t + v))))

The z-gluing pairs: z's high block against the last block of G, then z's low block against the second block of G (top pair first within each block).

Equations

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

theorem RS.mem_zClosePairs_flat (s t u v : ℕ) (x : Fin (u + v) ⊕ Fin (s + u + (t + v))) : x ∈ List.flatMap (fun (p : (Fin (u + v) ⊕ Fin (s + u + (t + v))) × (Fin (u + v) ⊕ Fin (s + u + (t + v)))) => [p.1, p.2]) (zClosePairs s t u v) ↔ (∃ (a : Fin (u + v)), x = Sum.inl a) ∨ ∃ (b : Fin (s + u + (t + v))), x = Sum.inr b ∧ (s ≤ ↑b ∧ ↑b < s + u ∨ s + u + t ≤ ↑b)

Membership in the flattened z-gluing pairs: every z-label, and the two z-blocks of G-labels.

theorem RS.zClosePairs_wf (s t u v : ℕ) : Fragment.PairsWF (zClosePairs s t u v)

The z-gluing pairs are well-formed.

def RS.pcSurvPred (s t u v : ℕ) : Fin (u + v) ⊕ Fin (s + u + (t + v)) → Prop

The survivor predicate of the z-gluing: no z-label survives, and a G-label survives iff it lies in one of the two x-blocks.

Equations

• RS.pcSurvPred s t u v = Sum.elim (fun (x : Fin (u + v)) => False) fun (b : Fin (s + u + (t + v))) => ↑b < s ∨ s + u ≤ ↑b ∧ ↑b < s + u + t

theorem RS.pcSurv_iff (s t u v : ℕ) (x : Fin (u + v) ⊕ Fin (s + u + (t + v))) : x ∉ List.flatMap (fun (p : (Fin (u + v) ⊕ Fin (s + u + (t + v))) × (Fin (u + v) ⊕ Fin (s + u + (t + v)))) => [p.1, p.2]) (zClosePairs s t u v) ↔ pcSurvPred s t u v x

Avoiding the z-gluing pairs is the survivor predicate.

def RS.pcSurvValEquiv (s t u v : ℕ) : { x : Fin (u + v) ⊕ Fin (s + u + (t + v)) // pcSurvPred s t u v x } ≃ Fin (s + t)

The surviving G-labels of the z-gluing, identified with the (s + t)-boundary: first x-block by value, second by offset.

Equations

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

noncomputable def RS.pcSurvEquiv (s t u v : ℕ) : Fragment.FoldSurviving (Fin (u + v) ⊕ Fin (s + u + (t + v))) (zClosePairs s t u v) ≃ Fin (s + t)

The survivor identification of the z-gluing.

Equations

• RS.pcSurvEquiv s t u v = (Equiv.subtypeEquivRight ⋯).trans (RS.pcSurvValEquiv s t u v)

noncomputable def RS.partialClose {s t u v : ℕ} (z : Fragment (Fin (u + v))) (G : Fragment (Fin (s + u + (t + v)))) : Fragment (Fin (s + t))

Partial closure: glue every open end of z into the matching z-block end of the test fragment G; the surviving x-block ends form the (s + t)-boundary.

Equations

• RS.partialClose z G = ((z.disjUnion G).glueList (RS.zClosePairs s t u v) ⋯).relabel (RS.pcSurvEquiv s t u v)