Six Birds: Foundations of Emergence Calculus
Ioannis Tsiokos
cs.LO
Jan 28, 2026 · v1
TL;DR
A small Lean development formalizes the order-theoretic core: closure operators, fixed points, closure ladders, iterate stabilization, Galois-insertion reflection, and idempotent endomaps.
Abstract
We develop a discipline-agnostic emergence calculus that treats theories as fixed points of idempotent operators acting on descriptions. We show that, once processes are composable but access to the underlying system is mediated by a bounded observational interface, a canonical toolkit of six closure-changing primitives (P1–P6) is unavoidable. The framework unifies order-theoretic closure operators with dynamics-induced endomaps $E_{τ,f}$ built from a Markov kernel, a coarse-graining lens, and a time scale $τ$. We introduce a computable total-variation idempotence defect for $E_{τ,f}$; small retention error implies approximate idempotence and yields stable "objects" packaged at the chosen $τ$ within a fixed lens. For directionality, we define an arrow-of-time functional as the path-space KL divergence between forward and time-reversed trajectories and prove it is monotone under coarse-graining (data processing); we also formalize a protocol-trap audit showing that protocol holonomy alone cannot sustain asymmetry without a genuine affinity in the lifted dynamics. Finally, we prove a finite forcing-style counting lemma: relative to a partition-based theory, definable predicate extensions are exponentially rare, giving a clean anti-saturation mechanism for strict ladder climbing.
Problem
The goal is a discipline-agnostic calculus of emergence. It should explain when coarse descriptions become theories with stable objects, how strict theory extension stays possible, and how directionality claims can be audited honestly under bounded observation.
Approach
Theories are treated as fixed points of idempotent operators on descriptions. Order-theoretic closure operators are unified with dynamics-induced endomaps built from Markov kernels, coarse-graining lenses and time scales. An arrow-of-time functional is defined as the path-space KL divergence between forward and reversed trajectories, and a finite forcing-style counting lemma is proved. The order-theoretic parts (closures, ladders, reflections via Galois insertions, idempotent endomaps) are mechanized in Lean; probabilistic results are checked with Python instead.
Results
Six closure-changing primitives (P1–P6) are shown to be unavoidable once processes are composable but interface-limited. Path reversal asymmetry is monotone under coarse-graining, and protocol holonomy alone cannot sustain asymmetry. Definable predicate extensions are exponentially rare relative to a partition-based theory.
