Causal Non-Interference: Formal Definition and Core Theorems

We provide a formal definition of Causal Non-Interference (CNI) — a security property for governed AI systems that extends classical non-interference (Goguen (2) the CVG Separation Invariant (VALID ≠ MANDATE) is a logical consequence of CNI, not an independent axiom; (3) the Audit Illusion is formally a CNI violation through identifiability-state misclassification; and (4) the Structural Limit Theorem is the causal-geometric characterisation of precisely the condition under which strict CNI is non-trivially binding. The four standard ML deployment strategies — shadow, canary, A/B, interleaved — correspond to the four levels of the identifiability lattice, yielding the first formal safety criterion for deployment strategy selection grounded in causal structure rather than operational heuristics. Version 1. 1 incorporates §5a (Probe Stability Amendments): three new formal objects — the Visibility Function V (ΔA, t), probe-induced drift δθ (ΔA, t, λ), and the Probe Stability Threshold Δθₘax — formalise the maximum tolerable actor-adaptation drift during a probe episode and provide both a pre-activation design constraint and a runtime enforcement mechanism (the Probe Stability Violation monitor). These objects provide a partial formal response to Open Question Q2 (decidability of idₛtate at runtime) within the bounded context of active probe episodes. Three open questions remain: CNI compositionality across system boundaries (Q1), full decidability of idₛtate outside probe episodes (Q2), and probabilistic extension for stochastic AI systems (Q3).