maxPhonemes_eq_gap45
plain-language theorem explainer
Recognition Science forces a maximum phoneme inventory of 45 from the orbit count tied to gap-45 in the Q₃ structure. Quantitative linguists comparing theoretical bounds to observed inventories would cite this equality when validating the upper limit. The proof is a direct reflexivity step that follows from the definition of maxPhonemes as exactly that orbit count.
Claim. The maximum phoneme inventory size equals 45, where this value is the orbit count associated with the gap-45 construction.
background
The module derives phoneme inventory bounds from Recognition Science applied to the Q₃ structure, which imposes a vertex count of 8, edge count of 12, and orbit count of 45. maxPhonemes is defined as 45 to represent the gap-45 orbit count. The band operation from PreLogicalCost supplies arithmetic conjunction on stable states via 0/1 multiplication.
proof idea
The proof is a one-line reflexivity step that matches the definition of maxPhonemes directly to the numerical value 45.
why it matters
This equality supplies the max_gap45 component inside PhonemeInventoryCert, which bundles the overall min-max bound, the minimum from the F₂³ cube, and the maximum from gap-45. It completes the bounding relation stated in the module documentation for phoneme inventories derived from the Q₃ structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.