CombinatoricsCert
plain-language theorem explainer
The CombinatoricsCert structure packages three decidable combinatorial facts that follow from the eight-tick octave in Recognition Science: the inductive type CombinatoricsFamily has cardinality 5, the binomial coefficient C(8,4) equals 70, and that value exceeds 45. A researcher checking the gap-45 relations or the combinatorial layer of the D=3 counting would cite this certificate when confirming the identities listed in the module. The definition is a plain record whose fields directly assert the statements with no internal computation.
Claim. Let $F$ be the inductive type whose constructors are permutations, combinations, partitions, paths, and Young tableaux. The structure asserts that the cardinality of $F$ is 5, that $C(8,4)=70$, and that $C(8,4)>45$.
background
Recognition Science obtains the eight-tick period from T7, yielding binomial coefficients over 8 elements when D=3. The module enumerates five canonical families (permutations, combinations, partitions, paths, Young tableaux) that equal configDim D=5 and records the identities C(8,4)=70 (maximum binomial at D=3) together with the relation 70=gap45+25. The upstream CombinatoricsFamily inductive supplies the Fintype instance used to state the cardinality claim.
proof idea
The structure is introduced as a record type whose three fields are direct propositional assertions. No lemmas or tactics are invoked inside the definition; the concrete values are supplied by sibling lemmas when an instance is constructed downstream.
why it matters
CombinatoricsCert supplies the type instantiated by combinatoricsCert, which records the numerical facts supporting C(8,4)=70=gap45+D^(D-1). It anchors the combinatorial layer between the eight-tick octave (T7) and the phi-ladder mass formula. The definition closes the module's claim that exactly five families arise at D=3; no open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.