combinatoricsFamilyCount
plain-language theorem explainer
The theorem establishes that Recognition Science produces exactly five combinatorial families at spatial dimension three. Researchers classifying discrete objects from the eight-tick octave would cite the count when listing permutations, combinations, partitions, paths, and Young tableaux. The proof is a one-line decision procedure that exhausts the constructors of the finite inductive type.
Claim. The finite type whose elements are the five combinatorial families (permutations, combinations, partitions, paths, and Young tableaux) has cardinality five: $|S| = 5$.
background
The module extracts combinatorial identities tied to the eight-tick octave at D=3, including the binomial coefficients C(8,k) and the statement that five families equal configDim D=5. CombinatoricsFamily is the inductive type with exactly those five constructors, each deriving DecidableEq, Repr, BEq, and Fintype. The module documentation lists the families as the canonical objects arising from Recognition Science and notes that C(8,4)=70 equals gap45 plus D to the power D-1.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the equality Fintype.card CombinatoricsFamily = 5. Because the inductive type derives Fintype and contains precisely five constructors, the decision procedure computes the cardinality by exhaustive enumeration with no additional lemmas required.
why it matters
The result supplies the five_families field of combinatoricsCert, which bundles the family count with the binomial identity C(8,4)=70 and the inequality C(8,4) greater than gap45. It realizes the framework claim that configDim equals five for D=3, linking the eight-tick octave (T7) to the enumeration of combinatorial objects. The declaration closes the enumeration step with no attached open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.