failureMode_count
plain-language theorem explainer
The theorem establishes that the FailureMode inductive type enumerates exactly nine distinct empirical failure patterns attached to the Option A cross-domain claims. Researchers maintaining the falsifier registry in Recognition Science cite this cardinality to confirm balance between theorems and testable refutations. The proof is a one-line decision procedure that evaluates the finite type cardinality from the nine constructors.
Claim. The cardinality of the set of failure modes is nine: $|FailureMode| = 9$, where each constructor names an empirical pattern that would refute one of the nine cross-domain claims in the Option A registry.
background
The Option A Falsifier Registry module maintains a finite collection that pairs each of the nine C1-C9 cross-domain theorems with an empirical test class. FailureMode is the inductive type whose nine constructors list the observable patterns that would count as failures of the associated claims. The module documentation states that this attachment keeps the cross-domain work from drifting into unfalsifiable numerology while recording zero sorry or axiom. Upstream FailureMode definitions appear in engineering and governance modules derived from J-cost analysis, supplying the structural pattern reused here.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable Fintype instance on the FailureMode inductive type, directly computing its cardinality as nine.
why it matters
This result feeds the falsifierRegistryCert definition, which certifies nine combinations, nine test classes, three statuses, nine dataset classes, and nine observables to keep the registry balanced. It fills the module requirement to attach concrete falsifiers to the theorem bundle, as described in the Option A Falsifier Registry documentation. In the Recognition Science framework it supports empirical testability for the forcing chain and cross-domain integrations without proving the underlying claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.