An introspection stage exists for seven-level normal form verifiers

MIPRE.Introspection ℓ (blueprint thm:introspection) records the data and guarantees of the introspection transformation for $\ell$-level normal form verifiers: constants $a \ge 1$ and $0 < b \le 1$ of the soundness loss $\delta(\varepsilon, n) = a\bigl((\lambda n)^a \varepsilon^b + (\lambda n)^{-b}\bigr)$; a complexity constant $C$; a $5$-level introspective sampler $\mathcal{S}^{\mathrm{intro}}_\lambda$ depending only on $\lambda$, with program computable from $\lambda$ in polynomial time; the polynomial-time compute from a verifier's programs and $\lambda$ to the introspective decider's program; the output, a $5$-level verifier with that sampler and decider; the complexity clauses at every input and index $n$ (sampler within $(\lambda n+1)^C$, dimension at most $(\lambda n+1)^C$, decider within $2^{(\lambda n+1)^C}$, both at degree $C$ in the input size, no answer longer than $2^{(\lambda n+1)^C}$ accepted) and the size bound $|\mathcal{D}^{\mathrm{intro}}| \le C(\lambda+1)^C$; completeness: for a $\lambda$-bounded $\ell$-level $\mathcal{V}$, a value-$1$ PCC strategy for $\mathcal{V}_{2^n}$ (answers at most $(2^n)^\lambda$) gives one for the output at $n$ (answers at most $2^{(\lambda n+1)^C}$); soundness: for $\lambda$-bounded $\mathcal{V}$, $n \ge 1$ and $\varepsilon > 0$, $\mathrm{val}^*(\text{output}_n) > 1 - \varepsilon$ implies $\mathrm{val}^*(\mathcal{V}_{2^n}) \ge 1 - \delta(\varepsilon, n)$. The statement is that the contract holds at $\ell = 7$:

It is one of the three stage contracts (with AnswerReduction 5 and Repetition 7) from which GapCompression.ofPipeline builds a GapCompression; every conditional glue theorem of this upload imports it.

Formalization Note In the repository the inhabitant is MIPRE.Introspection.seven : Introspection 7 (MIPRE/Background/Introspection/Compiler.lean), Classical.choice exists_seven, with exists_seven proved from the Pauli basis test thm:qld as its only rigidity input (blueprint lem:introspection-supply). The contract uses the ambient running-time convention: exponent $(\lambda n+1)^C$ in place of the paper's $2^{C\lambda n}$, degrees in the input size, soundness only for $n \ge 1$ (the input is bounded at $2 \le 2^n$), and the paper's $a > 0$ normalized to $a \ge 1$. The platform holds the statement only: the development proves it, in code the platform cannot host yet.