lin-0041
1.10 Soundness, completeness, and the research frontier
Rules R1–R6 preserve their stated structural judgments in every LINCS realization satisfying their side conditions.
R1 follows from Axiom 1.1 and transport along the registered isomorphism of observer codomains. R2 is presentation descent. R3 is the detection and effectivity property of the declared cover. R4 is tangent functoriality. R5 is precisely the invariant-preservation obligation attached to the target edit. R6 is conservativity of the sketch extension. Each conclusion therefore follows from a named semantic hypothesis rather than from the rule label alone.
The proposition is intentionally relative. It does not show that the side conditions are empirically true, that the observer family is complete, or that every desirable repair can be derived. It is a schema-level soundness statement, not yet a metatheorem for one fixed formal syntax and semantics.
A genuine completeness theorem would require fixing:
a formal language of sketches, observers, and repairs;
a semantic equivalence relation on learning judgments;
an allowed class of quotients, covers, tangent transports, and theory extensions; and
a statement that every semantically valid transformation is derivable from a finite rule set.
That program is plausible for restricted fragments. For example, one could study finite sketches with effective finite covers, a fixed tangent signature, and a typed edit language. A universal calculus for arbitrary learning sketches is a much stronger claim and may require higher-categorical coherence rather than a small list of first-order rewrite rules.
The proposed repair calculus does not identify causal effects from observational data. It axiomatizes controlled transformations of learning models. When a learning sketch contains a grounded causal model, its structural rules may be combined with do-calculus; they do not replace it.