theorem Hex.GraphIso.Nauty.SmallShape.mono {n base level : Nat} {ptn out : Array Nat} (hs : ptn.size = n) (ht : out.size = n) (hend : ptn[n - 1]! ≤ base) (hg : ∀ (q : Nat), ptn[q]! ≤ base → out[q]! ≤ level) (h : SmallShape n base ptn) : SmallShape n level out

Adding boundaries can only shrink cells. A surviving triple fills its unique old triple, so the small-cell shape is preserved at any later level.

theorem Hex.GraphIso.Nauty.NodeShape.mono {n base level : Nat} {ptn out : Array Nat} (hs : ptn.size = n) (ht : out.size = n) (hend : ptn[n - 1]! ≤ base) (hg : ∀ (q : Nat), ptn[q]! ≤ base → out[q]! ≤ level) (h : NodeShape n base ptn) : NodeShape n level out

Both shapes admitted by the cheap guard survive boundary refinement. This proof uses no graph dispatch or refinement implementation.