lin-0038

1.7 Six rule schemas

The following rules form a candidate calculus. Each rule has a semantic side condition. Omitting the side condition turns a licensed transformation into an unsupported rewrite.

Rule R1: observer substitution.

By Axiom 1.1, every observer is a map out of the same typed obstruction. Suppose \(\omega :\mathcal O_{\mathbb S}(D)\to Z\) and \(\omega ':\mathcal O_{\mathbb S}(D)\to Z'\), and suppose a registered isomorphism \(i:Z\cong Z'\) satisfies

\[ \omega '=i_{\mathrm{hom}}\circ \omega . \]

Then \(\omega \) may be replaced by \(\omega '\) in a diagnostic judgment, with its value transported along \(i\). More general lossy observer changes require an explicit statement of which judgments they preserve. This rule changes how failure is seen, not what failure means.

Rule R2: presentation elimination.

If the observer and proposed repair descend through \(\pi :P\to M\), then a judgment on representatives may be replaced by a judgment on the quotient model:

\[ \frac{ T\pi \circ V_P=V_M\circ \pi \qquad \omega _P=\omega _M\circ \pi }{ \Gamma ;\mathbb S\vdash e_P \; \Longrightarrow \; \Gamma ;\mathbb S\vdash e_M }. \]

Gauge-dependent variation is thereby deleted from the learning judgment.

Rule R3: localization and gluing.

Let \(\{ U_i\to U\} \) be a declared complete cover. A global diagnosis may be replaced by local diagnoses when the cover detects the relevant obstruction. Compatible local repairs may be replaced by a global repair only when descent is effective:

\[ \left. \begin{gathered} e_i|_{U_{ij}}\cong e_j|_{U_{ij}} \quad \text{with coherent descent data},\\ \text{the registered descent problem is effective} \end{gathered} \right\} \quad \Longrightarrow \quad \begin{gathered} \exists \, e_U,\\[-2pt] e_U|_{U_i}\cong e_i \end{gathered}. \]

Compatibility without effectivity licenses local agreement, not a global solution.

Rule R4: tangent transport.

An admissible repair may be transported to the tangent level:

\[ \frac{ \Gamma ;\mathbb S\vdash \alpha :D\Rightarrow D' }{ \Gamma _T;\mathbb S\vdash T\alpha :TD\Rightarrow TD' }. \]

Here \(\Gamma _T\) is \(\Gamma \) transported through the registered tangent interface; its existence is part of the tangent-admissibility side condition. The reverse inference is not automatic. A tangent repair need not integrate to a finite base repair, and an interaction residual need not identify which base mechanism should change.

Rule R5: target surgery.

Suppose \(e\) changes a registered target \(K\) and preserves every obligation in \(\mathcal I\). Then one may reason in the edited realization \(D[e/K]\) while retaining the non-target judgments:

\[ D\models \mathcal I \ \text{and} e\models \operatorname {Pres}(\mathcal I) \quad \Longrightarrow \quad D[e/K]\models \mathcal I. \]

This is the closest LINCS analogue of graph surgery. It is a structural intervention rule. It acquires Pearl-style causal semantics only when \(K\) denotes a grounded mechanism and the edit implements a realizable intervention protocol.

Rule R6: conservative declaration extension.

Let \(i:\mathbb S\hookrightarrow \mathbb S^+\) add objects, arrows, probes, or axioms. If \(i\) is conservative for the old language and the prior evidence transports along \(i\), judgments expressed entirely in \(\mathbb S\) remain licensed in \(\mathbb S^+\):

\[ \mathbb S^+\models i(\varphi ) \quad \Longleftrightarrow \quad \mathbb S\models \varphi \qquad (\varphi \text{ in the old language}). \]

This rule formalizes theory augmentation without silently rewriting earlier successes. It is central to abductive repair.

Appearance, reality, and declaration extension.

McCarthy’s distinction between appearance and reality gives R6 an epistemological interpretation [ McCarthy , 2007 ] . Let

\[ O:\mathcal R\longrightarrow \mathcal A \]

be an observation functor from a category of candidate realities to a category of appearances. Given appearance data \(A:\mathcal E\to \mathcal A\), inference of a reality asks for a lift

Commutative diagram illustrating 1.7 Six rule schemas.

with \(O\circ \widehat A=A\), or with a specified comparison when strict equality is not the intended semantics. The lift need not exist or be unique. If \(O\) is not faithful on the relevant structure, distinct realities may generate indistinguishable appearances. Additional views, actions, and experiments enlarge the probe family but do not guarantee identification.

When no object in the current declaration can support a satisfactory lift, R6 permits a new latent generator or law to be proposed in \(\mathbb S^{+}\). Atomic theory is the canonical example: atoms were introduced as theoretical objects behind macroscopic appearances rather than read directly from them. Such an extension is admitted only if it transports established evidence, preserves successful old judgments, and supports independent consequences. The new vocabulary is a candidate explanation, not its own validation.

Design principle

A repair rule should state four things: what may change, what must remain invariant, how the change propagates, and which evidence is still required. The rule licenses a candidate transformation; admission remains a separate decision.