Infinitesimal Causality

Topos causal models recast causal inference inside a topos: a causal world is a presheaf, an intervention is a sub-model named by a characteristic map into the subobject classifier $\Om$, and reasoning is Kripke-Joyal forcing in an intuitionistic internal language. We give the first axiom-free machine-checked account of this 1-topos core, in Cubical Agda over a previously verified probability monad and do-calculus; the framework is otherwise developed on paper, with central claims stated rather than proved. Three of our results go beyond faithful transcription. We exhibit a contextuality obstruction the programme does not treat: pairwise-consistent local causal data with no global model, detected by a degree-one holonomy class. We delimit the claim that interventions are modelled by the subobject classifier: an intervention and an observation name the same subobject, so $\Om$ fixes the target of a do-operation but not the operation itself, which is surgery on the kernels --- where, on a confounder, the interventional and observational laws differ. And we settle the modal unit --- inflationarity is derivable from $j\top = \top$ and naturality, not a fourth axiom. We also machine-check the classifier of sieves with its classification theorem, the pullback collating local mechanisms, and the Kripke-Joyal forcing clauses. The development assumes no axioms and typechecks under Agda's \texttt{--safe} flag, with the ordered field discharged at $\mathbb{Q}$; type-level sheafification and a directed do-calculus are future work.

Pearl's structural causal model (SCM) framework, built on directed acyclic graphs (DAGs) and the do-calculus, is the dominant formal language for causal reasoning. Yet it carries two structural restrictions: every relationship must be pre-specified as a directed causal edge, and feedback cycles are forbidden. This paper examines two classes of phenomena that strain these restrictions. First, symmetric physical and economic constraints, the ideal gas law being the canonical case, carry no intrinsic causal direction. Direction emerges only under intervention, and which variable is solved for must be specified as part of the intervention. We formalize such constraints as causal zeros within an Extended Causal Model by adding an activation operator, subject to local solvability and graph-admissibility conditions. Second, for the class of finite-propagation state-space systems considered here, we treat apparent instantaneous cycles as artifacts of suppressed time and ground both causal zeros and feedback in Causal Differential Equations (CDEs). In these, the transient regime is a time-unrolled acyclic causal process, and causal zeros arise as the defining functions of attracting equilibrium manifolds; periodic and chaotic attractors define further regimes of the same dynamics, treated through attractor-relative intervention. We give the extended do-calculus, identifiability conditions, counterfactual semantics, and open problems.

Causal discovery algorithms learn a network that describes the causal dependencies among random variables. A common workflow involves first utilizing conditional independence properties on observational data to determine partially directed causal relationships, then applying interventions to orient the unknown causal directions. A critical assumption for the first step is faithfulness: a requirement that causally linked variables exhibit statistical dependence. Many natural systems include buffering and stabilizing pathways that cancel out to achieve systemic robustness. This cancellation of pathways violates faithfulness, leading causal discovery algorithms to incorrectly remove causal dependencies. In this paper, we argue that hard interventions contain information about the presence/absence of causal linkage that is overlooked in the first stage of structure discovery. We show that a mild assumption -- called intervention-immediacy faithfulness -- that allows cancellations, is sufficient to nonparametrically identify causal structures with hard interventions. These results position interventions as the primary carriers of information about causal structure, which should take precedence over conditional independence testing. To flip the paradigm, we also specify equivalence classes when the identification criteria are not met due to limitations in the scope of interventions.