Very nice! But can you clarify what is the exact statement of downward LS you are using? I ask because some natural-seeming versions already imply that every infinite set is Dedekind infinite.

To my way of thinking, TC is similar in spirit to RR---it is a natural strengthening of RR.

It lies exactly at RR.

I'm not sure about that.

It provides a lower bound, as requested.

Regarding transfinite shifts, a shift is just a final segment, and this is a perfectly sensible notion for transfinite sequences. And there are only finitely many possible order types realized, as explained here: jdh.hamkins.org/…

These are all very elementary standard facts about well orders. Best to prove that every order preserving map from an ordinal to itself has $x\leq f(x)$, proved by induction. This immediately implies several of the other facts here.

Yes, that's right. It follows basically by definition of cardinals as initial ordinals in AC.

@blk It will be more interesting if you are able to articulate the desired features in your operation, and the problem will become to prove there is no such operation. What counts as a shift-like operation?

We know that it is relatively consistent that inconsistency arises at any given place in the hierarchy of consistency strength. It is consistent to hold that 3 inaccessibles are inconsistent, but not 2, or that a $\kappa^{+(17)}$-supercompact $\kappa$ is inconsistent, but not a $\kappa^{+(16)}$-supercompact $\kappa$, and so forth. So how can there be a robust concept of "near inconsistency"? Inconsistency could be anywhere, at any given level, even in your systems, and we don't have any way of finding out, except by exhibiting actual inconsistencies, which are few.

@FarmerS Ah, you are right. I had thought it was easy to ensure that condition simply by only placing constructible sets in at the right pace, but this can conflict with the constructibility requirement of the first requirement.

Yes, in $L$ we put only constructible sets into $L_{\alpha+1}$, but you allow more sets to go into $\mathfrak{L}_{\alpha+1}$, which opens the door eventually to put any given set in, by first gradually adding its hereditary elements.