combinationID_count
plain-language theorem explainer
combinationID_count establishes that the inductive type of implemented Option A cross-domain combinations has cardinality exactly nine. Researchers maintaining the Recognition Science falsifier registry cite this to certify completeness of the C1-C9 list before attaching empirical observables. The proof is a one-line decide tactic that evaluates the finite cardinality directly from the nine constructors.
Claim. The finite set of implemented Option A cross-domain combinations has cardinality nine: $|C| = 9$.
background
The Option A Falsifier Registry module maintains a finite list pairing each C1-C9 cross-domain theorem with an empirical test class. This keeps the theorems attached to concrete observables so the cross-domain work cannot drift into unfalsifiable numerology, per the module documentation. The upstream definition is CombinationID, an inductive type whose nine constructors are c1CognitiveTensor, c2PlanetStrata, c3OncologyTensor, c4QuantumMolecularDepth, c5AttentionTensor, c6EriksonReverse, c7UniversalResponse, c8MillerSpan, and c9RegulatoryCeiling.
proof idea
The proof is a one-line wrapper that applies the decide tactic to reduce Fintype.card of the inductive type to a decidable computation over its nine constructors.
why it matters
This cardinality result is referenced by the falsifierRegistryCert definition to populate the nine_combinations field alongside counts for test classes, statuses, and observables. It fills the registry requirement that the nine combinations remain explicitly enumerated and linked to empirical tests. In the Recognition framework this supports the cross-domain forcing chain by ensuring each combination carries a concrete falsifier rather than remaining open-ended.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.