
Classification systems (type systems, ontologies, taxonomies, schemas) operate over fixed sets of classification axes. We prove this architectural choice has unavoidable consequences: any fixed-axis system is incomplete for some domain. This is not a limitation of specific implementations; it is an information-theoretic impossibility. The Core Theorems All proofs in Lean 4 (2700+ lines, 142+ theorems, 0 sorry): Fixed Axis Incompleteness: For any axis set A and any axis a ∉ A, there exists a domain D that A cannot serve. The information required to answer D's queries does not exist in A. Parameterized Immunity: For any domain D, there exists an axis set A_D that is complete for D. This set is computable: A_D = ⋃_{q ∈ D} requires(q). The Asymmetry: Fixed systems guarantee failure for some domain. Parameterized systems guarantee success for all domains. One dominates the other absolutely. Uniqueness: For any domain D, all minimal complete axis sets have equal cardinality. "Dimension" is well-defined for classification problems. Minimality ⇒ Orthogonality: Every minimal complete axis set is orthogonal. Orthogonality is not imposed; it is derived from minimality. The Prescriptive Force. These are not design recommendations. They are mathematical necessities: Given any domain D, the required axes are computable, not chosen.Missing axes cause impossibility, not difficulty. No implementation overcomes a missing axis.The choice of axis-parameterization is forced by the requirement of domain-agnosticism.Application to Type Systems. We instantiate the framework to programming language type systems, proving: (B, S) (Bases and Namespace) is the unique minimal complete representation of class semantics(B, S, H) extends this for hierarchical configuration systems (adding a Scope axis)B-inclusive systems strictly dominate B-exclusive systems when B ≠ ∅ (in type system terminology: nominal typing dominates structural typing)Systems using only {S} require Ω(n) error localization; systems using {B, S} achieve O(1)The Broader Claim. The impossibility theorems apply to any classification system with fixed dimensions, not only type systems. Biological taxonomies, library classification schemes, database schemas, knowledge graphs: all are subject to the same constraints. A fixed set of axes guarantees domains that cannot be served. Corollary (Incoherence of Preference). Claiming "classification system design is a matter of preference" while accepting the uniqueness theorem instantiates P ∧ ¬P. Uniqueness entails ¬∃ alternatives; preference presupposes ∃ alternatives. The mathematics admits no choice.
structural typing, lower bounds, class systems, impossibility theorems, nominal typing, typing disciplines, information theory
structural typing, lower bounds, class systems, impossibility theorems, nominal typing, typing disciplines, information theory
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
