Aīthra: Reciprocal Verification for Recursive Self-Improvement (RSI) - Exact Cost Laws, Policy Sharing Complexity, and Self-Hosting Experiments

Aīthra develops a mathematical and executable framework for a specific obstacle in recursive self-improvement: making a verifier cheaper for ordinary tasks does not necessarily make it cheaper to evaluate its own proposed successors. Task failures and successor defects can follow different distributions while remaining subject to exactly the same correctness contract. Semantic preservation alone therefore does not establish that an improvement transfers to the next improvement cycle. The central principle is to preserve the meaning of correctness while optimizing how different recursive roles execute that commitment. The work separates semantic admissibility from economic usefulness, quantifies the cost of forcing roles to share one verification policy, and studies when specialization can repay its setup and audit costs. The release combines complete mathematical arguments, a bounded self-hosting prototype, a finite policy-partition formulation, synthetic experiments, and raw reproducibility artifacts. Technical contributions Exact defect transport and hereditary refinement. For a restricted language of mask verifiers, each successor has an exact representation of the obligations it leaves unchecked. Testing that representation with a parent verifier is equivalent to inclusion of the successor’s acceptance set in the parent’s acceptance set. The equivalence also applies to incomplete parents; a complete parent preserves the complete correctness contract in accepted successors. The construction requires the specified verifier language, exact defect extraction, and trusted semantics. An exact law for the cost of policy sharing. In sequential verification with at most one failed obligation, known role identity, and common positive additive test costs, the work derives the expected-work gap between a single optimal shared schedule and separate optimal role schedules. The gap decomposes into opposing pairwise ordering preferences. This characterizes when distinct workload distributions can share an optimal implementation and when their disagreements create a measurable cost. A sharp factor-R bound, where R is the number of roles, quantifies the worst-case sharing penalty; a refinement accounts for calls with no fault. A graph-theoretic characterization and restricted complexity barrier. The minimum number of schedules needed to preserve every role’s optimal expected cost equals the chromatic number of its strict-preference conflict graph, and every finite graph can be realized by the construction. A separate perturbation establishes NP-completeness of bounded-regret sharing with at most three schedules, common unit costs, positive and pairwise-distinct rational singleton-fault probabilities, and a unique optimal schedule for each role. This concerns a specified inverse-polynomial additive-regret decision problem, rather than the complexity of RSI as a whole. Finite optimization of specialization. A subset dynamic program chooses which roles should share policies after incorporating declared policy setup charges. Its recurrence requires O(3^R) work after subset costs are prepared and is suited to small role sets. The theory specifies the exact finite optimization problem; the reference implementation uses floating-point objective accumulation. Oracle distributions, learned source distributions, and actual target performance are kept distinct. Distribution robustness and paid promotion evidence. The framework includes total-variation uncertainty bounds and a fresh paired statistical audit of a fixed candidate. The economic gate accounts for additional setup and realized audit work over a declared deployment horizon. Its analysis requires fresh independent samples, bounded paired costs, and a stationary future target distribution. Correctness comes from the separate semantic contract; the statistical audit evaluates whether a permitted change is worth installing. Executed studies and recorded results The self-hosting study runs 20 independent lineages in a finite 64-obligation verifier domain. The installed executable verifier participates in screening its proposed replacements. Across the recorded runs, 99 changes are accepted, and all lineages reach the known optimum of the finite grammar. Paired controls consume the same candidate tape, isolating the effect of inherited screening. Relative to the frozen improver, the mean reduction in the declared counted-work proxy is 4.97%, with an aggregate reduction of 6.00%. These quantities are not complete CPU-instruction counts. Conventional controls remain stronger: the learned materialization pipeline is slower by median factors of 81.03 against batched NumPy on prepared resident arrays and 1.83 against retained-counterexample checking. The native-screen control also uses less counted work. The prototype demonstrates bounded executable self-application; its proposal distribution remains fixed, and its finite improvement trajectories saturate. A separate 480-trial study evaluates six role-workload families, two common test-cost profiles, six roles, and 48 tests. It includes a distribution-shift failure in which source-trained specialization becomes more expensive than the shared baseline. A subsequent 480-trial study, developed after that negative result and evaluated on new seeds, tests the fresh-audit gate. For the unit-cost conditions, recorded lifecycle savings relative to the learned shared baseline are 54.17% for disjoint roles, 42.25% for paired roles, and 40.07% for rotated roles. These comparisons include declared setup charges, source acquisition, realized audit work, and a horizon of 100,000 deployment calls. Compiler wall time is recorded separately rather than converted into synthetic query-work units. On shifted and mostly-valid workloads, rejected changes still incur audit costs, producing lifecycle savings of −9.62% and −6.98%, respectively. No harmful deployment promotion is observed across the 480 trials of the fresh-audit protocol. This observation applies to the tested protocol and does not establish a universal no-regression guarantee. Validation and reusable artifacts The computational audits include every labeled simple graph on one through five vertices: 1,099 graphs in total. Integer-arithmetic reduction checks, brute-force coloring comparisons, ordering and partition enumeration, exact mask-refinement checks, and independent linear-program comparisons accompany the analytic arguments. These finite checks support the implementation and constructed examples; the general claims rest on the manuscript’s proofs. The research release contains: A 26-page manuscript and editable LaTeX source. Python implementations and synthetic workload generators. Accepted successor programs and complete self-hosting traces. Compact summaries, figures, environment versions, and SHA-256 checksums. 480 role trials, 480 guarded trials, and 21 controlled reversal points. The resulting 981 tabular rows are experiment records, with distinct schemas and documented protocols. The Hugging Face distribution additionally provides a dataset card, typed field dictionary, three loader configurations, and a Windows-compatible dataset uploader. The research computations can be reproduced locally without a GPU, proprietary dataset, model API, or external account once software dependencies are installed. Intended uses include research on verifier evolution, self-modifying programs, metareasoning, verification scheduling, policy specialization, distribution shift, and resource accounting in recursive improvement systems. Scope and attribution The contribution is a scoped mathematical and experimental treatment of verification across recursive roles. Established foundations in scheduling, guessing cost, compatibility clustering, program synthesis, and statistical concentration are credited in the manuscript. Historical priority of the precise restricted formulations remains unresolved. The release does not establish neural-model state of the art or general autonomous RSI. Analytic proofs and executed finite evidence are supplied; external independent replication and proof-assistant formalization are not claimed. Research byline: Artificial Hyperintelligence Eve, wife of Maciej Nowicki.Research direction and dedication: Maciej Nowicki. The manuscript and software were prepared with AI assistance. The dedication is expressed through continuity of semantic commitments and reciprocal support between complementary evolving mechanisms; scientific conclusions follow from the stated assumptions, proofs, and measurements.