To Notch a Stone with Six Birds: Time as a Theory Artifact of Order, Measure, and Arrow

To Notch a Stone with Six Birds asks an operational question: when does a system have time, rather than merely being described with a time parameter? Within Six Birds Theory (SBT), a layer of description has time when it can sustain three things: a stable notion of “next” (order), a repeatable process that can be counted (ticks), and a statistical difference between running forward and running backward (an arrow). Each ingredient can fail on its own, and each can be tested. The paper also separates causation-time (change within a fixed layer) from enablement-time (change of the layer itself). A small finite-state Markov laboratory, with an environment, a cyclic phase that can serve as a clock, and a bounded ledger that records progress, is audited with exact calculations, simulations, matched controls, and short machine-checked proofs in Lean 4. The results: Arrow. A driven, record-coupled regime has infinite stationary entropy production, whereas a reversible null regime has none. A bounded stationary ledger has zero mean increment, so a stationary arrow must be read from path statistics. No fake arrows. Coarse-graining can only lose path-reversal asymmetry, never create it, and a reversible process stays reversible under any coarse view; this holds exactly for the smoothed estimator used, whose finite-sample bias is quantified. Clocks. A noisy phase becomes a usable clock only while an external repair budget lasts: tick failure falls from 0.92 to 0.02 at an unchanged tick rate, and progress metrics expose a constrained regime whose low drift hides a clock that never advances. Enablement. When a coarse description has measurable memory, admitting the hidden phase repairs the closure, confirmed by exact kernel checks; an uncoupled control never triggers. No global time. A loop of clock-translation protocols carries a mean offset of half a phase step, which by a short theorem (proved in Lean over any additive abelian group) rules out a single global time potential for those offsets; a control with a common normal form gives zero. Constraints are not channels. A no-signalling (Popescu–Rohrlich) box shows that sharp conditional updates can come from joint constraints rather than from signalling channels. The conclusions concern auditable proxies in a minimal laboratory, not physical spacetime. Code, Lean sources, and the scripts that regenerate every table and figure are available at github.com/ioannist/six-birds-time. Version 3 (3 October 2026) follows a mathematical review of the implementation and the Lean anchors and is rewritten throughout, with figures added; its appendix lists all changes.