phoneme_bound
plain-language theorem explainer
The inequality between the lower and upper bounds on phoneme inventory size follows directly from the Recognition Science derivation of the Q3 hypercube structure. Researchers modeling linguistic universals or testing Zipf-law predictions in phoneme distributions would cite this result to anchor the allowed range. The proof consists of a single decide tactic that evaluates the concrete constants 8 and 45.
Claim. $8 < 45$, where 8 is the vertex count of the three-dimensional hypercube $Q_3$ and 45 is the orbit count under the gap-45 constraint.
background
In the Phoneme Inventory Band from RS module, the Recognition Science framework derives language structure from the forcing chain applied to the 3-cube. The minimum phoneme inventory equals the vertex count of $Q_3$, fixed at 8. The maximum equals the orbit count under the gap-45 constraint, fixed at 45. This module proves the bounding relation required for the phoneme inventory certificate.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the inequality between the two natural-number constants.
why it matters
This theorem supplies the min_max field of the PhonemeInventoryCert definition, which certifies that human languages lie within the RS-derived band. It closes the bounding step in the linguistics depth of the framework, linking the Q3 vertex count to the gap-45 orbit count. The module documentation notes that the resulting Zipf exponent falls inside the empirical interval (0.45, 0.52).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.