Naive Refinement Complexity

Abstract

Finite signature refinement has linear rounds and the stated sorting and hashing costs.

Theorem 1.1 (Canonical refinement has the finite-system complexity bounds).

$$\begin{array}{c}\forall i,\mathrm{FiniteNonempty}(Y_i),\mathrm{FiniteNonempty}(O_i),\\ n_i=|Y_i|,\\ ta{u}_i:Y_i\to Y_i,q_i:Y_i\to O_i,\mathrm{Surjective}(q_i),\\ s_i\in \mathrm{BigO}(n_i\log n_i),h_i\in \mathrm{BigO}(n_i),w_i\in \mathrm{BigO}(1)⟶\\ (\mathrm{refinementRounds}(ta{u}_i,q_i)\le n_i-|O_i|)\wedge \\ (\mathrm{sortingRefinementWork}(\mathrm{refinementRounds}(ta{u}_i,q_i),s_i)\in \mathrm{BigO}(n_i\times (n_i-|O_i|+1)\times \log n_i))\wedge \\ (\mathrm{refinementWorkspace}(n_i,w_i)\in \mathrm{BigO}(n_i))\wedge \\ (\mathrm{expectedHashRefinementWork}(\mathrm{refinementRounds}(ta{u}_i,q_i),h_i)\in \mathrm{BigO}(n_i\times (n_i-|O_i|+1))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/NaiveRefinementComplexity.naive_refinement_complexity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Consider a filter-indexed family of finite nonempty deterministic state systems. Each readout is surjective onto its realized output carrier. The algorithm recursively labels a state by its current readout and the preceding label of its successor, and stops at the first unchanged partition.

The sorting, hashing, and workspace assumptions concern independent one-round or one-state cost functions. Total sorting and expected hashing work are constructed by multiplying the corresponding round cost by the canonical number of rounds plus the initial labeling pass. Total workspace is constructed from one record per state.

The imported finite-stability theorem bounds the first unchanged partition by the state count minus the realized-output count. Mathlib’s IsBigO.mul then composes that pointwise round bound with the primitive cost assumptions, producing the three displayed resource bounds.

Repository search directly found and applies controlled_finite_stability and its canonical stopping depth. Pinned Mathlib directly supplies IsBigO.mul, IsBigO.of_bound, and isBigO_refl. Loogle and LeanSearch executables were unavailable, and no single packaged theorem with all four clauses was found.

References

• Truth anchor: D5/S3/ObserverMemory/Algorithms/NaiveRefinementComplexity.naive_refinement_complexity
• Dependency: D5/S3/ObserverMemory/Algorithms/ControlledFiniteStability