Claim ledger — v1.0.0
Central contribution
A discovery procedure is itself a transferable, revisable computational object with explicit observations, repair semantics, resource costs, and evidence. Several different levels of improvement can be constructed without equating them with an unrestricted recursive learner.
Conditional mathematical results
The manuscript proves finite repair synthesis, uncertainty-preserving investigation, method transport, certified early optimality closure, grammar refinement, safe streaming omissions, checked equation quotienting, exact preservation of teacher transcripts, repair-relative leaf bounds, and finite lineage progress. Each statement is conditional on its declared domain. STATEMENT_INDEX.md and ASSUMPTION_REVIEW.md identify every case.
Two first-edition statements complete the integration:
- Dependency-complete reuse: with a finite acyclic graph, semantically complete dependencies, sound local rules, and applicable external premises, unchanged witnesses remain usable outside the stale descendants. Re-establishing affected claims topologically restores the relevant chain. A registry does not discover or prove its own dependency completeness.
- Resource-price accounting: a single complete additive saving vector is nonnegative under every nonnegative price vector exactly when it is componentwise nonnegative. A declared finite convex price family can be checked at its listed vertices. This is a linear accounting fact, not a universal performance theorem.
These statements use elementary or established foundations. Their inclusion is not a priority claim for induction, dynamic programming, equivalence classes, statistical concentration, or linear optimization.
Executed finite constructions
- One diagnostic controller is compiled and checked from explicit experiment and repair tables.
- A certified compiler wrapper can stop when its candidate attains proved lower bounds.
- A finite learner synthesizes a capacity-rejection expression from primitive syntax and counterexamples.
- A second acquisition procedure proposes 1,068 probe-matched equations and admits 336 by a limited proof procedure. The remaining equations are unproved by that procedure, not classified as false.
- The acquired equations reduce 3,960 syntax candidates to 1,362 representatives while preserving the exact ordered teacher transcript. A stronger supplied normalizer retains 1,352, so the acquired representation is not claimed superior to it.
- Checked repair weights extend streaming omission beyond singleton repairs. A universal repair invalidates the old weights and permits a one-step controller after rechecking.
- The first-edition manager replays the actual equation, quotient, rule, weight, and controller checks. It distinguishes stale dependencies, unavailable parents, and rejected evidence. Revised cost evidence can validly report a negative saving.
Acquired objects and supplied foundations
The controller, selected compiler strategy, composed pruning AST, and checked equation library are distinct acquired objects. The arithmetic interpretation, finite grammar, teacher, candidate order, proof axioms, local replay procedure, query/repair model, synthesis algorithms, and lifecycle dependency graph remain supplied.
The code does not inspect or modify arbitrary external software or accounts. No agent training, physical calibration, or learned Neuralese–OSL integration is run.
What performance numbers mean
The records separate model-record reads, interpreter visits, comparisons, rational additions, teacher work, proof checking, library bytes, and controller records. Those are not interchangeable CPU instructions. A lower read count can coexist with higher total cost. Setup and installed information are not erased by calling them background. Resource-price examples are declared analytical models, not measured universal hardware prices.
Not established
General intelligence, indefinitely accelerating self-improvement, superior performance across unrelated domains, autonomous invention of the checker or mathematics, self-improvement of the equation learner itself, guaranteed wall-clock speedup, learned physical semantics, independent novelty, external peer review, or formal-kernel verification.
The first-edition freeze is a completed theoretical and editorial scope. Those stronger questions remain research questions, not assertions implied by the version number.