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 representation of class semantics. (B, S, H) extends this for hierarchical configuration systems. H (hierarchy) was added in production to enable a click-to-provenance UI feature in OpenHCS. The axis derivation procedure identified it as required. {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.