Probably not (ed: probably not unless you are doing it to discuss the the larger path to being able to enable this, rather than opening it to propose adding it to the existing type system)
In terms of being able to type an ordinal, there’s prior work that’s largely seen as a failure (see various threads about why the numeric tower doesn’t work for typing).
In terms of mutability, lossless mathematical operations, etc, it’s not something that fits into python’s type system compatibly with those chosen foundation right now.
You can view this thread about why collections.abc.Hashable is “Broken” by the current foundation of the type system, the same applies to any type that indicates “this type doesn’t do something” (such as allow mutating) because subtypes are not prohibited from adding behavior. This has a path to being fixable, but the general idea of encoding certain properties of types that aren’t statically determinable is going to be a hard sell prior to fixing those, and there’s been very little appetite shown by type checker authors on topics like this.
It’s not impossible to model these things in a type system, but it’s not reasonably possible to model these in python’s static type system without changes to the foundation to have it be correct.