Impossibility Theorems for Fixed-Axis Classification Systems: With Application to Type Theory

The typing discipline debate (duck vs structural vs nominal) rests on a false premise. We prove: Duck typing is not a coherent discipline. It uses axis S (namespace/shape) without declared interfaces, violating basic consistency requirements. Structural typing is Pareto-dominated by nominal typing. Nominal uses axes B (bases/inheritance) and S. Structural uses only S. Nominal provides all capabilities of structural plus four additional capabilities (provenance, identity, enumeration, conflict resolution). The dominance is strict when B ≠ ∅. All fixed-axis systems are incomplete. This includes nominal typing. For any fixed axis set A, there exists a domain D that A cannot serve. The solution is not choosing the "best" fixed discipline. It is deriving axes from domain requirements. The Core Theorems (All proofs in Lean 4, 6300+ lines, 190+ theorems, 0 sorry): Fixed Axis Incompleteness (Universal): For any axis set A, there exists a domain D that A cannot serve. Every fixed-axis system fails for some domain. 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. Semantic Non-Embeddability: Disciplines with fewer axes cannot embed disciplines with more axes. Structural typing cannot simulate nominal typing. The gap is information-theoretic. No encoding or workaround bridges it. Minimality ⇒ Orthogonality: Every minimal complete axis set is orthogonal. Orthogonality is not imposed. It is derived from minimality. Matroid Structure: Orthogonal axis sets satisfy the matroid exchange property. All minimal complete sets have equal cardinality. Dimension is well-defined. 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: (B, S) is the unique minimal complete axis set for the domain of standard class semantics. It is still incomplete for domains requiring additional axes. (B, S, H) extends this for hierarchical configuration systems. H (hierarchy) was derived when OpenHCS required scope-chain queries that (B, S) could not answer. {B, S} strictly dominates {S} when B ≠ ∅. Nominal typing dominates structural typing. Structural typing cannot provide provenance, identity, enumeration, or conflict resolution. These require B. 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. Biological taxonomies, library classification schemes, database schemas, knowledge graphs: all are subject to the same constraints. Every fixed axis set guarantees domains that cannot be served. Corollary (Incoherence of Preference). Claiming classification system design is a matter of preference while accepting the uniqueness theorem is a contradiction. Uniqueness entails no alternatives exist. Preference presupposes alternatives exist. The mathematics admits no choice.