# Verification report: AIM-LOGIC-0084

Title: Sharp Computability Bounds for Nonforking Sections.
Author: Alper Ferudun, Mercury Software GmbH.
Prepared: 28 September 2026. Status: complete self-audited theorem,
unrefereed preprint; not independent or proof-assistant verification.

## Accepted mathematical claims

1. For a complete stable theory in a computable countable language and
   separately decidable countable models M elementary in N, a computable
   elementary embedding permits a section computable from p joined with 0'.
   No decidability of the embedding range is needed for this upper bound.
2. For the effective theory of infinitely many infinite equivalence classes,
   a decidable-range elementary inclusion has an X-computable section iff
   D(M,N) = {b in N: its E-class meets M} is Turing reducible to X.
3. An explicit permanent-stage-tagged construction realizes every c.e.
   degree as the degree of D(M,N), so the fixed 0' upper bound is sharp.
4. A decidable full diagram of (N,P), P naming M, yields a computable section
   for every stable theory. This stronger input is not refuted.

Type names are characteristic functions on formulas with named parameters.
The original source leaves this coding unspecified. No claim is made that
every reasonable input representation has the same negative answer. No claim
is made that a computable type has a noncomputable individual extension.

## Written-proof checks

The detailed originating-researcher audit addresses immutable stage labels,
infinite model axioms, effective quantifier elimination and elementarity,
computability of the generic input, finite use of arbitrary formula queries,
adaptive transcript agreement, forced principal outputs, both directions of
the finite decision rule, consistency of the general trace-defined section,
the fixed auxiliary jump, and the full-pair versus separate-diagram boundary.
No mathematical gap in the stated theorem was found in that audit.

The noncomputability argument uses a finite computation at the new-class
input and compares it with principal inputs. It does not use an effective
compactness theorem, a modulus of continuity, or a validity test for type
names. The source package contains the full proof and audit.

## Finite exact regression tests

Checker SHA-256:
`761b6b8c921da0611c91757ac772b800b5debd1d966536c1d60502d569f54d05`.

- 81 synthetic schedules (four indices, each absent or entering at stage 0/6).
- 60 sampled M-elements and 68 sampled N-elements per schedule.
- Exact tuple equality, integer, and Boolean arithmetic; no floating point.
- Python 3.13.5: PASS, 1,925,316 assertions.
- Python 3.12.14: PASS, 1,925,316 assertions.

Both runs execute the same checker and are not independent reviews. They do
not decide the actual halting set, exhaust first-order syntax, or establish
the infinite-model axioms by enumeration. Those claims are proved in the text.

## Source and integrity checks

Before drafting, all ten SHA-256 hashes in the 28 September proof-acceptance
record matched their files. All four source PDFs matched their stored hashes
and byte sizes. Source PDFs remain private research inputs and are not
redistributed in the release ZIP. The exact AIM question, classical trace
definability, and the related 2026 definition-selection preprint are identified
in the bibliography and accompanying source review. Absence of a direct
predecessor in a bounded search is not a proof of priority.

## Compilation and visual QA

- Built-in desktop LaTeX compiler: success for the standalone current source.
- Existing Tectonic 0.17.0 publication export: success, 6 pages, 82,035 bytes.
- Final TeX log: no warning, undefined reference, overfull/underfull box, or
  missing-character diagnostic matched the explicit inspection.
- All six pages rendered with Poppler at 100 dpi and visually inspected.
- Title, sole author byline, author-footnote affiliation/contact, theorem and
  equation layout, mathematical symbols, citations and page numbers checked.
- No separate AI-assistance heading; disclosure occurs in ordinary prose.

Initial local export could not download the uncached lmodern package under
restricted network access; the approved run against the official Tectonic
bundle succeeded. This was an environment failure, not a mathematical or
LaTeX-source defect. The local operation log retains this diagnosis.

Mathematical acceptance, source interpretation, novelty, package readiness,
and actual publication are separate. A reserved DOI or saved repository draft
does not establish publication or external validation.