Finite-Branching Path Clock Criterion

Abstract

Nonnegative clocks on finite words have equivalent path, depth, and sublevel criteria.

Definition 1.1 (Path clock).

$$\begin{gathered} \forall A:Type,c:(\mathrm{List}(A))\to (A)\to \mathbb{R},h:\mathrm{List}(A), \\ {T}_c(h)=\sum _{i:\mathrm{Fin}(\mathrm{length}(h))}c(\mathrm{take}(h,i),\mathrm{get}(h,i)). \end{gathered}$$

Formalization. D5/S3/Estimation/ExperimentCost/FiniteBranchingPathClockCriterion.pathClock (✓ std3).

Source. Repository-derived.

Commentary.

The clock of a finite word is the sum of the calibrated costs of its successive edges. The cost of a letter is evaluated on the complete prefix preceding that letter.

Definition 1.2 (Minimum path clock at a depth).

$$\begin{gathered} \forall A:Type,[\mathrm{Fintype}(A)],[\mathrm{Nonempty}(A)], \\ c:(\mathrm{List}(A))\to (A)\to \mathbb{R},n:\mathbb{N}, \\ {g}_c(n)=\underset{w:(\mathrm{Fin}(n))\to A}{\min }{T}_c(\mathrm{ofFn}(w)). \end{gathered}$$

Formalization. D5/S3/Estimation/ExperimentCost/FiniteBranchingPathClockCriterion.minimumPathClock (✓ std3).

Source. Repository-derived.

Commentary.

At each depth, the minimum is taken over every word on the finite nonempty alphabet. Thus the minimum is attained.

Theorem 1.3 (Path divergence, depth control, and finite sublevels).

$$\begin{gathered} \forall A:Type,[\mathrm{Fintype}(A)],[\mathrm{Nonempty}(A)], \\ c:(\mathrm{List}(A))\to (A)\to \mathbb{R},(\forall h:\mathrm{List}(A),x:A,0\le c(h,x))\Rightarrow \\ List.TFAE(\forall omega:(\mathbb{N})\to A,\mathrm{Tendsto}(\Lambda n:\mathbb{N},T_c(\mathrm{ofFn}(\Lambda i:\mathrm{Fin}(n),\mathrm{omega}(i))),atTop,atTop), \\ \mathrm{Tendsto}(\Lambda n:\mathbb{N},g_c(n),atTop,atTop), \\ \forall b:\mathbb{R},\mathrm{Finite}(\{h:\mathrm{List}(A)\mid T_c(h)\le b\})). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/FiniteBranchingPathClockCriterion.finite_branching_path_clock_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Nonnegative increments make clocks monotone under extension. Hence the minimum clock is monotone in depth, and divergence of these minima bounds every clock sublevel by a finite set of short words.

A finite sublevel cannot contain all distinct prefixes of an infinite word. Conversely, bounded depth minima give nonempty finite level sets closed under restriction. Konig’s infinity lemma selects a compatible sequence, producing an infinite word with bounded clock.

References

• Truth anchor: D5/S3/Estimation/ExperimentCost/FiniteBranchingPathClockCriterion.finite_branching_path_clock_criterion
• Truth anchor: D5/S3/Estimation/ExperimentCost/FiniteBranchingPathClockCriterion.minimumPathClock
• Truth anchor: D5/S3/Estimation/ExperimentCost/FiniteBranchingPathClockCriterion.pathClock