Finite Discussion Stability

Abstract

A finite discussion admits at most the initially unresolved number of strict refinements.

Theorem 1.1 (Finite discussions have a sharp strict-refinement budget).

$$\begin{array}{r}\forall X:\mathrm{Type},[\mathrm{Fintype}(X)],steps:\mathbb{N},\\ \forall Coordinate:\mathrm{Fin}(steps+1)\to \mathrm{Type},\\ \forall concept:\forall i:\mathrm{Fin}(steps+1),\mathrm{Concept}(X,Coordinate(i)),\\ \forall effective:\forall i:\mathrm{Fin}(steps+1),\mathrm{Surjective}(concept(i)),\\ \forall strict:\forall i:\mathrm{Fin}(steps),\mathrm{StrictRefinement}(concept(\mathrm{castSucc}(i)),concept(\mathrm{succ}(i))),\\ steps\le |X|-|\mathrm{Im}(concept(0))|.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Discussion/FiniteDiscussionStability.finite_discussion_stability (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let X be a finite state space and let q_i : X -> C_i be the concept readout after i strict information-growth steps. Each readout is surjective, so its coordinate type records exactly its attained concept classes rather than unused labels.

Every nonredundant message is represented by the repository’s canonical StrictRefinement relation from q_i to q_(i+1). A refinement factor is surjective on effective coordinate types. If their finite cardinalities were equal, Mathlib’s finite surjection criterion would make the factor bijective and its inverse would give the forbidden reverse refinement.

Consequently every message increases the number of attained concept classes by at least one. The final class count is at most |X|, while surjectivity identifies the initial coordinate count with |Im(q_0)|. Therefore n <= |X| - |Im(q_0)|, exactly the finite discussion bound.

Repository search supplied ConceptJoinUniversal.Refines and StrictRefinementCapability.StrictRefinement. Pinned Mathlib supplied Nat.bijective_iff_surjective_and_card, Nat.card_le_card_of_surjective, and Nat.card_congr; no existing declaration packages the arbitrary-discussion bound.

References

• Truth anchor: D5/S3/ConceptDynamics/Discussion/FiniteDiscussionStability.finite_discussion_stability
• Dependency: D5/S3/ConceptDynamics/StrictRefinementCapability