Per Fun Math Stuff and the Philosopher's Stone #1.
1a. We can obtain something like the same results as the Restriction Technique (which caveats or conditionalizes the T-Schema) with Quantification Restriction/Typing. I alluded to Quantification Typing in my draft as a reply to context instability woes surrounding the T-Schema (contra Read).
1b. Strengthening my argument further: we can also think of a consistent T-Schema as being expressed in two ways: (The Pure Classical Form) T𝑓(s) ↔ s (albeit with Quantification Typing - e.g. more precisely expressed as: ∀x(T𝑓(x) ↔ x) such that x ranges over Truth-Based/Truth-Grounded sentences).
1c. Or, the Restricted form p → (T𝑓(s) ↔ s) - more precisely ∀y∀x(y → (T𝑓(x) ↔ x)) (or ∀y(y → ∀x(T𝑓(x) ↔ x))) where x,y is allowed to range over any sentence type.
1d. I think the observation above (in tandem with the basic fact that if p is a tautology so too is q implies p) makes my view far more palatable. Proponents of the T-Schema get to keep an analytically true axiom (if the T-Schema is as they insist since they also insist it's Analytic) that's aesthetically the same (lexicographically isomorphic but Quantifier Type Restricted).
2a. Curry–Howard Correspondence can be used to frame my formal definition of Alethic Paradox (the very first to my knowledge): an Alethic Paradox is any proof to contradiction whose shortest proof requires the use of T-Schema or F-Schema.
2b. Apparently, Curry–Howard Correspondence is often used in tandem with topological (or tableaux) notions (Paths) and Normalization Techniques that simplify or shorten a "route" from an expression to some ending expression (preventing "meandering" or "wandering off the trail"). In this way, we can establish the "sameness" of techniques through a variety of ways (not just via "sameness" in computable models).