Finite iteration of the actual Alice Introspect replacement #
Starting with the original projective family, each successor is constructed from the current game's tests. The numerical inverse threshold discharges every smallness premise. All other questions retain their extensions, and all fixed hiding errors and both primitive Z errors are preserved exactly; the second player's hiding errors in both roles.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md). Each stage adjoins to the
first player an ancilla register whose size the Kraus–Halmos dilation chooses
(exists_intro_successor), so the model changes type from one stage to the next: the iterated
model is a model over the second player's algebra, packed with its algebras (ModelOver). Every
POVM strategy of it reduces to one of the original model (BipartiteModel.POVMReduces), which is
how a value model dominating the original model dominates it. The matrix version's explicit
carrier introIterationAux, state introIterationState and repeated extension
introIterationExtend have no counterpart: the iterated model carries them.
A concrete projective strategy family exists after every finite Alice stage, in a model reducing to the original one. The original primitive bounds and explicit positive threshold suffice; no future structural invariant, future error bound, or stage-smallness conclusion is assumed. The full option-valued invariant includes malformed answers and the support of all valid answers.