| Description: Define the class of
grade- and blocklift-stable partition-side general
partition-equivalence spans. It consists of those
⟨𝑟, 𝑛⟩ ∈ PetParts such that
⟨𝑟,
𝑛⟩ remains in
PetParts after shifting one grade along SucMap (via
ShiftStable). Concretely: ⟨𝑟, 𝑛⟩ ∈ PetParts
and there
exists a predecessor 𝑚 with suc 𝑚 = 𝑛 such that
⟨𝑟, 𝑚⟩ ∈ PetParts (encoded by
SucMap ∘ PetParts inside
ShiftStable). I.e., it introduces the external
(tower/grade)
stability axis. This is the "4th level" for pet 39135
(see dfpet2parts2 39143):
beyond (i) carrier membership partition, (ii) disjointness, and (iii)
semantic equilibrium, we require (iv) stability under a canonical grade
shift. PetParts already enforces disjointness and
the quotient-carrier
equation for the lifted span (hence semantic equilibrium via
dfpetparts2 39142). Pet2Parts adds the
external grade (tower) stability
axis via df-shiftstable 38652 with SucMap.
This (iv) is why we need
explicit second-level Pet2Parts, while Disjs typically does not:
Disjs already packages its own internal two-step
consistency (carrier
+ map) by dfdisjs6 39112 / dfdisjs7 39113, whereas pet 39135
has an additional grade
axis that must be imposed separately. (Contributed by Peter Mazsa,
19-Feb-2026.) |
