seventy_is_choose_8_4
plain-language theorem explainer
70 equals the binomial coefficient C(8,4), the largest central binomial for n=8. This supplies a concrete witness inside the Recognition Science cardinality spectrum, confirming that 70 arises from combinations of the cube generators {2,3} and config dimension 5. The proof is a direct decision procedure that evaluates the numerical identity in one step.
Claim. $70 = {8} choose {4}$ holds in the natural numbers, where the right-hand side is the central binomial coefficient.
background
The module collects witnesses for cardinalities of canonical RS domain types. The spectrum comprises values reachable by multiplying, summing, or powering the cube-generators {2,3}, the configDim 5, and gap45. The local setting is the structural claim that RS produces a structured numerical spectrum rather than an arbitrary collection, with every listed cardinality admitting a decomposition into these primitives.
proof idea
The proof is a term-mode decision that directly evaluates the equality 70 = Nat.choose 8 4. The decide procedure computes the binomial coefficient and confirms the match without invoking any lemmas.
why it matters
This witness populates the cardinalitySpectrumCert definition, which aggregates Dspatial=3, Dconfig=5, gap45, eight-tick, and cube-face relations. It supports the claim that the spectrum is generated from RS primitives and aligns with the eight-tick octave and D=3 spatial dimensions in the forcing chain. No open scaffolding questions are closed by this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.