Effective nonforking sections in stable theories

Definitions and mathematical statement

The extracted Question 6 asks only whether there is a computable section. Its verification locates the question in Section 1.3, "Continuous sections (Miller)," but does not reproduce the entire surrounding formulation. The paired aid studies the following precise setting.

Let $M\prec N$ be a fixed countable elementary pair in a stable computable language, with decidable elementary diagrams and an effective inclusion. Let $S_1(M)$ and $S_1(N)$ be the spaces of complete one-types, and let \[ r:S_1(N)\to S_1(M),\qquad q\mapsto q|_M. \] A section $s$ satisfies $r\circ s=\operatorname{id}$. Use Type-2 names that give the characteristic function of membership for all formulas with parameters, rather than only enumerating positive information. The source question concerns computation with the stated input name, not just an abstract set-theoretic right inverse.

The aid reports a uniform one-jump upper bound for the canonical nonforking section. For $p\in S_1(M)$, stability supplies, for each formula $\varphi(x;y)$, a definition $d(y,c)$, $c\in M$, such that \[ \varphi(x;b)\in p\quad\Longleftrightarrow\quad M\models d(b,c)\qquad(b\in M). \] Candidate formulas and finite parameter tuples can be enumerated. Correctness of a candidate is a $\Pi^0_1(p)$ condition, so $p'$ selects a correct one. Evaluating it on parameters from $N$, using its decidable diagram, computes the nonforking extension $s_{\mathrm{nf}}(p)$. Thus \[ s_{\mathrm{nf}}(p)\leq_T p' \] uniformly relative to the specified effective presentations. This is not a computation from $p$ alone and is not an affirmative solution of the jump-free section question.

For the theory of an infinite pure set, the aid gives a no-jump special case when the elementary inclusion has decidable range. Quantifier elimination reduces each output formula to Boolean combinations of equalities $x=b$. The extension answers $x=b$ by the input type when $b\in M$, and answers false for $b\in N\setminus M$. This computes the canonical section directly from $p$, without deciding globally whether $p$ is realized. It does not prove a no-jump result for all stable theories, and a bound on the canonical section does not classify every possible section.

Short English statement

The supplied reconstruction concerns sections of restriction between type spaces for a decidable stable elementary pair. The canonical nonforking section is reported computable from one jump of the type name; pure equality admits direct computation under a decidable-inclusion hypothesis. The general jump-free question and the omitted source context remain separate.

Sources

• Local source record: catalogue entry, catalogue entry; canonical aim-logic-notes.json, notes[83], Question 6. Title: "Effective nonforking sections in stable theories."
• AIM list Computable stability theory, Section 1.3 "Continuous sections (Miller)," supplied reference https://aimath.org/pastworkshops/computestabproblems.pdf. The extracted question alone does not identify the map; this draft uses the aid's reconstruction without accessing a PDF.
• Attempt 1 supplies characteristic-function Type-2 coding, the one-jump candidate-definition argument and the pure-equality no-jump example. No full authoritative external references or exact surrounding source quantifiers are supplied.
• Registry dated 14 August 2026: "partially_solved," "PARTIAL-PROGRESS," statement status "exact"; attempt partial, research-run status unknown, rigor "proved," novelty confidence low. The machine-generated, non-peer-reviewed aid requires independent verification before citation.