Finite Future Split Budget

Abstract

Finite future refinements obey pair and class-count split budgets.

Theorem 1.1 (Finite refinements consume a bounded split budget).

$$\forall X\in Type,B\in Type,finiteX\in \mathrm{Finite}\left(X\right),s\in \mathbb{N},C\in \mathrm{Fin}\left(s+1\right)\to \mathrm{Concept}\left(X,B\right),strict\in \left(\forall i\in \mathrm{Fin}\left(s\right),\mathrm{StrictlyRefines}\left(C\left(\mathrm{castSucc}\left(i\right)\right),C\left(\mathrm{succ}\left(i\right)\right)\right)\right),s\le \mathrm{choose}\left(|X|,2\right)\wedge s\le |X|-|\mathrm{range}\left(C\left(0\right)\right)|$$

Proof. Machine-checked in Lean as D5/S3/Observer/Budget/FiniteFutureSplitBudget.finite_future_split_budget (✓ std3). ∎

Source. Repository-derived.

Commentary.

The readouts form a finite chain on the same state carrier. Each strict step preserves existing distinctions and splits at least one old observation class.

The frozen strict-refinement theorem gives the sharp class-count deficit. A nonempty initial image removes one state from that deficit, and the binomial recurrence bounds the remainder by the number of unordered distinct state pairs; the empty carrier is handled separately.

References

• Truth anchor: D5/S3/Observer/Budget/FiniteFutureSplitBudget.finite_future_split_budget
• Dependency: D5/S3/ConceptDynamics/Refinement/StrictRefinementBound