Uniform all-time clock avalanche

Abstract

A clock for each ordered maximal face realizes every finite complex without ghost original vertices as the original slice of an actual parallel avalanche. The orbit is classified for every natural time, including its final facet and its empty firing tail.

Definition 1.1 (outdegree).

$$\forall W\in \mathrm{Type},[\mathrm{Fintype}\left(W\right)][\mathrm{DecidableEq}\left(W\right)]\forall G\in \mathrm{Digraph}\left(W\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\forall w\in W,\mathrm{outdegree}\left(G,w\right)=\mathrm{card}\left(\mathrm{filter}\left(\mathrm{Adj}\left(G,w\right),\mathrm{univ}\left(W\right)\right)\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.outdegree (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

Out-degree counts actual outgoing arcs.

Definition 1.2 (firing).

$$\forall W\in \mathrm{Type},[\mathrm{Fintype}\left(W\right)][\mathrm{DecidableEq}\left(W\right)]\forall G\in \mathrm{Digraph}\left(W\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\forall c\in W\to \mathbb{N},\forall w\in W,w\in \mathrm{firing}\left(G,c\right)\iff \left(0<\mathrm{outdegree}\left(G,w\right)\wedge \mathrm{outdegree}\left(G,w\right)\le c\left(w\right)\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.firing (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

Every unstable vertex with positive out-degree fires once. This excludes all sinks even when they have accumulated grains.

Definition 1.3 (step).

$$\forall W\in \mathrm{Type},[\mathrm{Fintype}\left(W\right)][\mathrm{DecidableEq}\left(W\right)]\forall G\in \mathrm{Digraph}\left(W\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\forall c\in W\to \mathbb{N},\forall w\in W,\mathrm{step}\left(G,c,w\right)=c\left(w\right)-\mathrm{ite}\left(w\in \mathrm{firing}\left(G,c\right),\mathrm{outdegree}\left(G,w\right),0\right)+\sum _{a\in W}\mathrm{ite}\left(a\in \mathrm{firing}\left(G,c\right)\wedge \mathrm{Adj}\left(G,a,w\right),1,0\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.step (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

Subtraction uses eligibility in the old configuration, followed by one arrival along each arc from the old complete firing set. Arrivals cannot authorize same-time firing; sink coordinates are retained.

Definition 1.4 (orbit).

$$\forall W\in \mathrm{Type},[\mathrm{Fintype}\left(W\right)][\mathrm{DecidableEq}\left(W\right)]\forall G\in \mathrm{Digraph}\left(W\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\forall c\in W\to \mathbb{N},\forall t\in \mathbb{N},\mathrm{orbit}\left(G,c,t\right)=\mathrm{iterate}\left(\mathrm{step}\left(G\right),t,c\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.orbit (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

The actual orbit iterates the synchronous transition; no firing schedule is an input.

Definition 1.5 (avalanche).

$$\forall W\in \mathrm{Type},[\mathrm{Fintype}\left(W\right)][\mathrm{DecidableEq}\left(W\right)]\forall G\in \mathrm{Digraph}\left(W\right),[\mathrm{DecidableRel}\left(\mathrm{Adj}\left(G\right)\right)]\forall c\in W\to \mathbb{N},\forall T\in \mathrm{Finset}\left(W\right),T\in \mathrm{avalanche}\left(G,c\right)\iff \left(\mathrm{Nonempty}\left(T\right)\wedge \left(\exists t\in \mathbb{N},T\subseteq \mathrm{firing}\left(G,\mathrm{orbit}\left(G,c,t\right)\right)\right)\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.avalanche (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

The native complex omits the empty face and takes the downward closure of actual firing sets at all natural times. Conventional augmentation adds only the empty face.

Definition 1.6 (original).

$$\forall V\in \mathrm{Type},\forall m\in \mathbb{N},\forall v\in V,\mathrm{original}\left(m,v\right)=\mathrm{inl}\left(\mathrm{inl}\left(v\right)\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.original (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

Originals embed into the first summand of W = (V + Fin m) + Unit. Clock i is inl(inr i); the sink is inr(unit).

Definition 1.7 (neighbours).

$$\forall V\in \mathrm{Type},[\mathrm{DecidableEq}\left(V\right)]\forall m\in \mathbb{N},\forall F\in \mathrm{Fin}\left(m\right)\to \mathrm{Finset}\left(V\right),\forall w\in \mathrm{Sum}\left(\mathrm{Sum}\left(V,\mathrm{Fin}\left(m\right)\right),\mathrm{Unit}\right),\mathrm{neighbours}\left(F,w\right)=N\left(F,w\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.neighbours (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

N(F,o(v)) is the sink singleton. N(F,p(i)) is o[F(i)] together with p(i+1) when i+1<m and the sink otherwise. N(F,s) is empty. Distinct summands exclude loops and separate the successor from the facet.

Definition 1.8 (clockGraph).

$$\forall V\in \mathrm{Type},[\mathrm{DecidableEq}\left(V\right)]\forall m\in \mathbb{N},\forall F\in \mathrm{Fin}\left(m\right)\to \mathrm{Finset}\left(V\right),\forall a\in \mathrm{Sum}\left(\mathrm{Sum}\left(V,\mathrm{Fin}\left(m\right)\right),\mathrm{Unit}\right),\forall w\in \mathrm{Sum}\left(\mathrm{Sum}\left(V,\mathrm{Fin}\left(m\right)\right),\mathrm{Unit}\right),\mathrm{Adj}\left(\mathrm{clockGraph}\left(F\right),a,w\right)\iff w\in \mathrm{neighbours}\left(F,a\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.clockGraph (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

Adjacency is membership in the actual outgoing neighbor set. Original out-degree is one; clock out-degree is the facet cardinality plus one; sink out-degree is zero.

Definition 1.9 (initial).

$$\forall V\in \mathrm{Type},[\mathrm{DecidableEq}\left(V\right)]\forall m\in \mathbb{N},\forall F\in \mathrm{Fin}\left(m\right)\to \mathrm{Finset}\left(V\right),\forall b\in V,\forall w\in \mathrm{Sum}\left(\mathrm{Sum}\left(V,\mathrm{Fin}\left(m\right)\right),\mathrm{Unit}\right),\mathrm{initial}\left(F,b,w\right)=C\left(F,b,w\right)$$

Formalization. D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.initial (✓ std3).

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

C(F,b,o(v)) is one exactly at b. C(F,b,p(i)) is |F(i)| + [i=0]. C(F,b,s)=0. No restriction on facet overlap, repetition, order, or the choice of b is imposed.

Theorem 1.10 (uniform clock all time).

$$\forall V\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{DecidableEq}\left(V\right)]\forall K\in \mathrm{AbstractSimplicialComplex}\left(V\right),\forall m\in \mathbb{N},1\le m\Rightarrow \left(\forall f\in \mathrm{Fin}\left(m\right)\to \mathrm{facets}\left(K\right),\mathrm{Surjective}\left(f\right)\Rightarrow \left(\forall b\in V,\left(\left(\forall t\in \mathbb{N},\forall v\in V,\mathrm{orbit}\left(\mathrm{clockGraph}\left(\mathrm{values}\left(f\right)\right),\mathrm{initial}\left(\mathrm{values}\left(f\right),b\right),t\right)\left(\mathrm{original}\left(m,v\right)\right)=O\left(\mathrm{values}\left(f\right),b,t,v\right)\right)\wedge \left(\forall t\in \mathbb{N},\forall i\in \mathrm{Fin}\left(m\right),\mathrm{orbit}\left(\mathrm{clockGraph}\left(\mathrm{values}\left(f\right)\right),\mathrm{initial}\left(\mathrm{values}\left(f\right),b\right),t\right)\left(\mathrm{clock}\left(i\right)\right)=P\left(\mathrm{values}\left(f\right),t,i\right)\right)\right)\wedge \left(\left(\forall t\in \mathbb{N},\mathrm{firing}\left(\mathrm{clockGraph}\left(\mathrm{values}\left(f\right)\right),\mathrm{orbit}\left(\mathrm{clockGraph}\left(\mathrm{values}\left(f\right)\right),\mathrm{initial}\left(\mathrm{values}\left(f\right),b\right),t\right)\right)=S\left(\mathrm{values}\left(f\right),b,t\right)\right)\wedge \left(\forall T\in \mathrm{Finset}\left(\mathrm{Sum}\left(\mathrm{Sum}\left(V,\mathrm{Fin}\left(m\right)\right),\mathrm{Unit}\right)\right),T\in \mathrm{avalanche}\left(\mathrm{clockGraph}\left(\mathrm{values}\left(f\right)\right),\mathrm{initial}\left(\mathrm{values}\left(f\right),b\right)\right)\iff \left(\mathrm{Nonempty}\left(T\right)\wedge \left(\left(\exists A\in \mathrm{Finset}\left(V\right),A\in K\wedge T=\mathrm{map}\left(\mathrm{original}\left(m\right),A\right)\right)\vee \left(\exists i\in \mathrm{Fin}\left(m\right),T\subseteq \mathrm{insert}\left(\mathrm{clock}\left(i\right),\mathrm{map}\left(\mathrm{original}\left(m\right),B\left(\mathrm{values}\left(f\right),b,i\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.uniform_clock_all_time (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Henri Riihimäki, Jason P. Smith (2026). Avalanche homology of digraphs via sandpile dynamics. URL: https://arxiv.org/abs/2606.26786v1.

Commentary.

Here F(i) is the underlying maximal face of f(i), and f is an arbitrary surjective ordered enumeration, permitting repetitions. O(F,b,0,v)=[v=b]; O(F,b,t,v)=[v in F(t-1)] for 1<=t<=m and zero thereafter. P(F,t,i)=|F(i)| for t<i, |F(i)|+1 for t=i, and zero for t>i. S(F,b,0)={o(b),p(0)}; S(F,b,t)=o[F(t-1)] union {p(t)} for 1<=t<m; S(F,b,m)=o[F(m-1)]; S(F,b,t) is empty for t>m. B(F,b,0)={b}, and B(F,b,i)=F(i-1) for i>0. The induction removes the current original indicator, replaces it by the active clock’s facet indicator, and passes one grain only to the successor clock. At the last facet all clocks are zero; at every later time all nonsinks are zero, while the sink retains its accumulated grains. Maximal-face coverage identifies the original faces with K and the remaining generators with the clock attachment simplices. Every face containing the sink or two clocks is excluded. No topology, collapse, homology, or torsion conclusion is included.

References

• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.avalanche
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.clockGraph
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.firing
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.initial
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.neighbours
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.orbit
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.original
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.outdegree
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.step
• Truth anchor: D5/S3/StatisticalMechanics/Sandpiles/UniformClockAvalanche.uniform_clock_all_time