PhonemeInventoryCert
plain-language theorem explainer
The PhonemeInventoryCert structure certifies that the minimum phoneme inventory size is strictly below the maximum, with the minimum fixed at 8 and the maximum at 45. Quantitative linguists applying Recognition Science to universal grammar bounds would cite this when establishing numerical constraints on phoneme sets. It is a structure definition that directly bundles three relations drawn from the Q3 vertex count and gap-45 orbit count.
Claim. A structure certifying bounds on phoneme inventory size where the minimum count $m$ satisfies $m < M$, $m = 8$, and $M = 45$, with 8 the vertex count of the 3-cube graph $Q_3$ and 45 the orbit count associated to gap-45.
background
Recognition Science derives phoneme bounds from the cube graph $Q_3$, whose 8 vertices set the minimum inventory size while gap-45 supplies the 45-orbit maximum. The module states that $Q_3$ forces vertex count 8, edge count 12, and orbit count 45, then packages these as a certificate for human-language phoneme inventories. Upstream definitions fix minPhonemes as the vertex count of $Q_3$ and maxPhonemes as the gap-45 orbit count.
proof idea
The declaration is a structure definition whose three fields directly assert the strict inequality between the minimum and maximum counts together with the two equalities to 8 and 45. No lemmas or tactics are invoked beyond the upstream constant definitions of minPhonemes and maxPhonemes.
why it matters
This certificate is instantiated by the downstream phonemeInventoryCert definition, which supplies the concrete values via phoneme_bound, minPhonemes_eq_F2cube, and maxPhonemes_eq_gap45. It supplies the numerical bounds (8 to 45) required for the linguistics depth of the Recognition Science framework, linking the eight-tick octave and $D=3$ spatial dimensions to observable language constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.