CombinatoricsFamily
plain-language theorem explainer
Recognition Science enumerates five combinatorial families to match the configuration dimension at D=3. A researcher deriving binomial identities from the eight-tick octave cites this enumeration when establishing C(8,4)=70. The declaration is given directly as an inductive type that derives Fintype for immediate cardinality access.
Claim. Let $F$ be the inductive enumeration of combinatorial families in Recognition Science consisting of permutations, combinations, partitions, paths, and Young tableaux. Then $F$ carries decidable equality and finite cardinality 5.
background
The module extracts combinatorial identities from the Recognition Science framework, including binomial coefficients C(8,k) for the eight-tick octave at D=3 and the central identity C(8,4)=70 exceeding gap-45 by D^{D-1}. Five families are introduced to align with configDim D=5, supplying the substrate for Catalan number C_5=42 and Bell number B_5=52 near the same gap. The local setting is the derivation of all physics from the functional equation via the forcing chain T0-T8, with T7 fixing the eight-tick period and T8 fixing D=3.
proof idea
The declaration is an inductive definition with five constructors, automatically deriving DecidableEq, Repr, BEq, and Fintype. No tactics or lemmas are applied; the structure itself enables the cardinality theorem combinatoricsFamilyCount.
why it matters
This definition supplies the five families required by the certificate structure CombinatoricsCert, which asserts Fintype.card CombinatoricsFamily =5 together with choose84=70. It implements the module claim that five families equal configDim D=5, linking directly to the eight-tick octave (T7) and spatial dimension D=3 (T8) in the forcing chain. No open questions are addressed; it closes the enumeration step for subsequent combinatorial proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.