Description: Define the class of grade- and blocklift-stable partition-side general
partition-equivalence spans. It consists of those
<. r , n >. e. PetParts such that <. r , n >. remains in
PetParts after shifting one grade along SucMap (via
ShiftStable ). Concretely: <. r , n >. e. PetParts and there
exists a predecessor m with suc m = n such that
<. r , m >. e. PetParts (encoded by SucMap o. PetParts inside
ShiftStable ). I.e., it introduces the external (tower/grade)
stability axis. This is the "4th level" for pet (see dfpet2parts2 ):
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 ). Pet2Parts adds the external grade (tower) stability
axis via df-shiftstable 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 / dfdisjs7 , whereas pet has an additional grade
axis that must be imposed separately. (Contributed by Peter Mazsa, 19-Feb-2026)
Could not format Pet2Parts = ( SucMap ShiftStable PetParts ) : No typesetting found for wff Pet2Parts = ( SucMap ShiftStable PetParts ) with typecode wff