lin-0133

10.2 The anatomy of a CoLT transition

A transition begins with a probe and ends with a decision about the maintained state. It preserves the distinctions introduced by the six-stage lincs workflow.

Definition 10.2 CoLT transition record

Given a state \(\mathfrak C_k\), a CoLT transition record is

\[ \tau _k= (\delta _k,o_k,\bar o_k,\lambda _k,r_k,\gamma _k,a_k), \]

with the following typed fields:

  1. \(\delta _k\in \mathcal T_k\) is an admitted probe;

  2. \(o_k=(o_k^0,o_k^1)\) records the observed base and tangent obstruction values;

  3. \(\bar o_k=\pi _k(o_k)\) is the obstruction after quotienting null variation;

  4. \(\lambda _k\) localizes \(\bar o_k\) over \(\mathcal U_k\);

  5. \(r_k\in \mathcal R_k\) is a proposed typed repair, possibly the null proposal or a request for more evidence;

  6. \(\gamma _k\) is a certificate containing provenance, preserved obligations, tests, uncertainty, and rejected alternatives; and

  7. \(a_k\in \{ \mathsf{admit},\mathsf{reject},\mathsf{abstain}\} \) is the result of applying \(\mathcal A_k\).

Only \(a_k=\mathsf{admit}\) authorizes the maintained successor \(\mathfrak C_{k+1}\). Rejection and abstention append records to the trace without silently changing \(D_k\).

A CoLT transition. The return edge changes the maintained state only after admission. Rejection and abstention still extend the audit trace.
Figure 10.1 A CoLT transition. The return edge changes the maintained state only after admission. Rejection and abstention still extend the audit trace.
Definition 10.3 CoLT trace

A CoLT trace of length \(n\) is

\[ \mathfrak C_0 \overset{\tau _0}{\Longrightarrow} \mathfrak C_1 \overset{\tau _1}{\Longrightarrow}\cdots \overset{\tau _{n-1}}{\Longrightarrow} \mathfrak C_n, \]

together with every rejected or abstained transition record encountered between the displayed admitted states. Each record must be type-correct for the state from which it was generated, and every state-changing arrow must carry an admission certificate.

The trace is consequently not just its successful path. Failed repairs, unresolved alternatives, and requests for new evidence are part of the reasoning object. They prevent the final conclusion from erasing how narrowly it was licensed.