FailureMode
plain-language theorem explainer
The FailureMode inductive type enumerates nine empirical patterns that would falsify the C1-C9 cross-domain theorems in the Recognition Science framework. Researchers maintaining empirical protocols cite this registry to attach concrete falsifiers to each theorem bundle. The definition proceeds by direct inductive enumeration deriving DecidableEq, Repr, and Fintype instances.
Claim. An inductive type whose elements are the empirical failure patterns attached to the Option A claims, consisting of sufficiency of a single-axis decoder, absence of a small phi-power ratio, additive therapy response, depth exceeding five bits, non-forty plateau spectrum, non-reverse dementia order, non-unit shared coefficient, non-Q-space span collapse, and module exceeding ceiling 70.
background
The module defines a finite registry that pairs each C1-C9 cross-domain theorem with a dataset class, predicted observable, and failure mode. This keeps the claims attached to concrete tests so the cross-domain work cannot drift into unfalsifiable numerology. Upstream modules supply analogous inductive FailureMode types for engineering (yielding, buckling, fatigue, fracture, creep), governance (authoritarianism, oligarchy, ruleOfMen, coupRisk, informationCollapse), and materials (ductileFracture, brittleFracture, fatigue, creep, stressCorrosion).
proof idea
This is a direct inductive definition of the nine constructors with automatic derivation of DecidableEq, Repr, and Fintype.
why it matters
It supplies the failure modes used by the failureMode mapping and the ProtocolFalsifiable predicate, which require a dataset class, predicted observable, and failure mode for each CombinationID. The definition supports the module goal of keeping cross-domain theorems empirically testable. It aligns with the framework requirement that claims remain falsifiable rather than drifting into numerology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.