phonemeInventoryCert
plain-language theorem explainer
The phonemeInventoryCert definition assembles a certified interval for natural-language phoneme counts under Recognition Science constraints. Linguists modeling inventory size from the phi-ladder or eight-tick octave would cite the resulting 8-to-45 band when deriving Zipf exponents. The definition is a direct record construction that supplies three fields from already-proved sibling facts.
Claim. Let $m$ be the minimum phoneme inventory size and $M$ the maximum. Then $m = 2^3$, $M = 45$, and $m < M$.
background
The module treats phoneme inventories as bounded by the Recognition Science forcing chain. The lower bound equals the order of the vector space $F_2^3$, which supplies eight vertices under the eight-tick octave. The upper bound equals the gap-45 orbit count. The PhonemeInventoryCert structure packages the strict inequality together with these two explicit values.
proof idea
The definition constructs the PhonemeInventoryCert record by direct field assignment: the inequality from phoneme_bound, the equality to eight from minPhonemes_eq_F2cube, and the equality to forty-five from maxPhonemes_eq_gap45. No further tactics or reductions are applied.
why it matters
This definition closes the phoneme-inventory band in the linguistics extension of Recognition Science, linking the T7 eight-tick octave and T8 three-dimensional forcing to observable language statistics. It supplies the concrete interval used to predict Zipf exponents near 0.48. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.