combinationID_count
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove the empirical validity of any attached test class.
- Does not include or define C10, left as commentary.
- Does not derive the combinations from J-cost or the phi-ladder.
- Does not specify the internal structure of the test classes.
formal statement (Lean)
31theorem combinationID_count : Fintype.card CombinationID = 9 := by
proof body
Decided by rfl or decide.
32 decide
33
34/-- Coarse empirical test class attached to a combination. -/