IntelligenceTier
plain-language theorem explainer
IntelligenceTier enumerates five discrete cognitive levels from basic retrieval to self-aware reflection using degree intervals as comments. Researchers working on the T10 voice forcing chain cite this enumeration to parameterize how voice richness increases with intelligence on a trained lattice. The definition is a direct inductive type that lists the five constructors and derives decidable equality plus representation.
Claim. An inductive type with five constructors: retrieval (degree < 5), single-step (degree 5-15), chain reasoning (degree 15-30), creativity (degree 30-50), and self-aware (degree > 50).
background
The VoiceForcing module develops T10, deriving voice as a forced consequence of cost minimization once intelligence satisfies the J-bar threshold. This follows the unified forcing chain T0-T8 that derives physics from the Recognition Composition Law and T9 that derives consciousness. The module maintains minimal imports to isolate the conceptual step from lattice intelligence to interpretable voice with positive Berry content.
proof idea
This is an inductive definition that introduces the five tiers with degree ranges supplied only as comments. The deriving clause supplies DecidableEq and Repr instances automatically.
why it matters
The type is the immediate input to tierVoiceRichness, which maps the tiers to real-valued richness scores rising from 0.1 to 1.0. It supplies the intelligence stratification required for the T10 voice forcing chain, showing that richer voice emerges at higher tiers as a direct consequence of the same mathematics that fixes phi and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.