Materializing actual positional row buffers

Flattening one exact-width row per constraint is exactly the existing incidence-order buffer. This original representation bookkeeping is shared by initialization and blossom references.

theorem Cslib.Logic.PL.CSP.Solver.materialize_labels (F : CSP Table ℕ) (rows : List (List Bool)) (hlen : rows.length = List.length F) (hw : ∀ (i : Fin (List.length F)), (rows.getD ↑i []).length = F[↑i].2.length) : List.map (Blossom.labels F rows) F.incidenceList = rows.flatten

Materializing a complete row buffer in incidence order is exactly list flattening. Both the number of rows and every actual scope width are explicit hypotheses.