minPhonemes_eq_F2cube
plain-language theorem explainer
The equality establishes that the minimum phoneme inventory size equals eight, matching the vertex count of the three-dimensional hypercube over the field with two elements. Linguists applying Recognition Science to language structure would cite this when fixing the lower bound on phoneme counts. The proof reduces to a direct computational verification that the definition of the minimum yields exactly two cubed.
Claim. Let $m$ denote the minimum phoneme inventory size, defined as the vertex count of the three-dimensional hypercube $Q_3$ over the field with two elements. Then $m = 2^3$.
background
The Phoneme Inventory Band from RS module derives phoneme bounds from the Recognition Science structure of $Q_3$, where vertex count equals eight, edge count equals twelve, and orbit count equals forty-five. The upstream definition sets the minimum phoneme count to the natural number eight as the vertex count of $Q_3$. This supplies the lower end of the bounding relation proved in the module, with the upper end tied to the gap-45 orbit count.
proof idea
The proof is a one-line wrapper that applies the decide tactic to confirm the numerical equality between the definition of the minimum phoneme count and two raised to the third power.
why it matters
This supplies the minimum value used inside the PhonemeInventoryCert definition that assembles the full certified bounds. It aligns with the eight-tick octave (period $2^3$) and the forcing of three spatial dimensions in the Recognition Science chain. The result closes the lower bound for the linguistics application with no remaining scaffolding in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.