Strength of BTEE What is the consistency strength of Basic Theory of Elementary Embeddings (BTEE) from The spectrum of elementrary embeddings j : V → V by Paul Corazza?
BTEE uses the language of $(V,∈,j)$ and asserts:
ZFC (without separation and replacement for formulas using $j$)
(schema) $j$ a is nontrivial elementary embedding of $V$ into $V$ (for formulas without $j$)
critical point: the least ordinal moved by $j$ exists.
Without critical point, the theory would be conservative over ZFC.  With full replacement (and given the axiom of choice), the theory would be inconsistent; and there is a hierarchy between the two extremes.
BTEE suffices for a basic theory of $j$.  For every natural number $n$, BTEE proves that $κ = \mathrm{crit}(j)$ is $n$-ineffable and totally indescribable (see the linked paper).  However, the only upper bound on the strength of BTEE in the paper is $ω$-Erdős.
This question is in Q/A format.
 A: BTEE is conservative over the stationary reflection principle (SRP), i.e. ZFC + (schema) {there is $n$-subtle cardinal}$_{n∈\mathbb{N}}$. Using $n$-ineffable in the schema is equivalent.
Note that we get conservativity and not just equiconsistency, and also that (without full conservativity) SRP shows up in a number of other results including in a basic axiomatization of reflective cardinals of finite orders (an extension of the language of set theory), and (separately) in Harvey Friedman's natural arithmetic statements independent of ZFC.
As noted above, for every $n$, BTEE implies existence of $n$-subtle cardinals.
For the converse, given a proposition $A$, consistency of ZFC + $A$ + (schema) {there is $n$-subtle cardinal}$_{n∈\mathbb{N}}$ implies existence of a model $M$ of ZFC + $A$ + $n$-subtle cardinal for a nonstandard number $n$, plus existence of $λ$ with $V_λ^M≺M$.  Fix such an $M$ and an $M$-well-ordering $<^*$ of $V_λ^M$, and (in $M$; $n$ is nonstandard outside of $M$) use an $n$-subtle cardinal $<λ$ to produce an $n$-tuple $(κ_1,...,κ_n)$ of good indiscernibles for $(V_λ^M, ∈^M, <^*)$.  ("good" is a technical term here and is why we need the $n$-subtle cardinal; it will ensure that $j$ does not move $M$-ordinals below $κ_1$.)  Let $M'$ be the $(V_λ^M, ∈^M, <^*)$ Skolem hull of the first $ω$ of these indiscernibles (as computed in $V$ so all Gödel numbers are standard).  $(M',∈^M,j)$ satisfies BTEE + $A$ where $j(κ_i)=κ_{i+1}$ and $j$ is extended to all sets in $M'$ using the Skolem hull.
Adding induction (and especially transfinite induction) would significantly increase the strength.  For the strength of existence of a well-founded model of BTEE, see this question.
$n$-huge cardinals
Nonstandard models can also be used to show that WA0 (bounded quantifier Wholeness Axiom, which consists of BTEE and separation for bounded quantifier $j$-formulas) is conservative over ZFC + (schema) {there is $n$-huge $κ$ with $V_κ≺_{Σ_n}V$}$_{n∈\mathbb{N}}$ .  (In turn, this is $Σ_2^V$ conservative over ZFC + (schema) {there is $n$-huge $κ$}$_{n∈\mathbb{N}}$ .)
One direction is proved in the linked paper.  For the converse, given a proposition $A$, consistency of ZFC + $A$ + (schema) {there is $n$-huge $κ$ with $V_κ≺_{Σ_n}V$}$_{n∈\mathbb{N}}$ implies existence of a model $M$ of ZFC + $A$ + $n$-huge cardinal $κ$ for a nonstandard number $n$, and with $V_κ^M≺M$.  Starting with such $M$ and an $n$-huge embedding $j$ in $M$ with $κ = \mathrm{crit}(j)$, let $M' = \{x∈M: ∃m<ω \,\, x ∈^M j^m(V_κ^M)\}$.  (Note that we use $ω$ rather than $ω^M$.) $(M', ∈^M, j)$ satisfies WA0 + $A$.
