configDim5_equicardinal
plain-language theorem explainer
Any two finite types A and B each satisfying HasConfigDim5 have identical cardinality. Cross-domain researchers cite this to confirm all D=5 structures are equinumerous. The proof is a one-line rewrite that substitutes the two cardinality hypotheses.
Claim. Let $A$ and $B$ be finite types. If $|A|=5$ and $|B|=5$, then $|A|=|B|$.
background
HasConfigDim5 is the predicate asserting that a type T equipped with a Fintype instance has cardinality exactly 5. The module formalizes configDim universality for D=5 across domains, listing instances in sensory, emotional, biological, economic and linguistic structures plus the product theorem yielding cardinality 125. The definition of HasConfigDim5 supplies the direct equality used in the statement.
proof idea
One-line term proof that rewrites the two hypotheses hA and hB, each stating Fintype.card equals 5, to obtain the trivial equality 5=5.
why it matters
The result closes the equicardinality half of the C13 universality claim, ensuring every D=5 type is interchangeable by size with every other. It supports the sibling triple-product theorem of cardinality 125 and aligns with the framework's emphasis on D=5 as a repeated structural motif alongside the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.