Commitment Depth Telescoping

Abstract

Commitment depth is the finite telescoping loss of compatible future-plan capacity.

Proposition 1.1 (Commitment depth telescopes along a finite history).

$$\begin{array}{r}\forall Plan:\mathrm{Type},n:Nat,\\ Omega:Nat\to \mathrm{Finset}(Plan),\\ \sum _{t\in \mathrm{range}(n)}log2(\mathrm{card}(Omega(t)))-log2(\mathrm{card}(Omega(t+1)))=\\ log2(\mathrm{card}(Omega(0)))-log2(\mathrm{card}(Omega(n))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Agency/CommitmentDepthTelescoping.finite_plan_commitment_depth_telescopes (✓ std3). ∎

Source. Repository-derived.

Commentary.

The source object is a finite sequence of compatible future-plan spaces. At each step, commitment depth is constructed as the decrease in its base-two log-cardinality.

The finite sum cancels every intermediate plan-space capacity, leaving only the initial capacity minus the terminal capacity. The result also holds for an empty plan space under Lean’s total real logarithm.

References

• Truth anchor: D5/S3/ConceptDynamics/Agency/CommitmentDepthTelescoping.finite_plan_commitment_depth_telescopes