ora-0181

16.2 A transport theorem

Theorem 16.3 Compositional transport of learned structure

Let \(E_0\xrightarrow {f}E_1\xrightarrow {g}E_2\) be environment morphisms. Suppose \(\tau _f\) and \(\tau _g\) are admissible structural transports, their Beck–Chevalley mates satisfy the pasting law, their observer comparisons are conservative on the settled doctrine, and their safety comparisons preserve admission. Then

\[ \tau _{g\circ f}\simeq \tau _g\circ \tau _f \]

is an admissible structural transport. The transported universal witness, settled answers, and repair certificates remain valid in \(E_2\). If the tangent comparisons are invertible and coherent, the same conclusion holds for tangent knowledge.

Proof ▼

Beck–Chevalley pasting identifies the composite of the two transport-then-extension comparisons with the comparison for \(g\circ f\). Naturality transports the universal witness. Conservativity of the observer comparisons composes, as does preservation of the safety subobjects. Registered repair certificates transport through the same comparison cells. For tangent knowledge, paste the two comparisons with \(T\); coherence gives the required comparison for the composite.

The theorem gives sufficient conditions, not free transfer. When a mate is not invertible, its failure is informative: it measures the precise defect between reusing the old construction and relearning after transport.