failureMode_injective
plain-language theorem explainer
The function mapping each of the nine CombinationIDs to a FailureMode is injective. Registry maintainers cite this to guarantee that distinct cross-domain theorems receive distinguishable empirical attachments. The proof proceeds by introducing two arbitrary inputs, performing exhaustive case analysis on both, and simplifying with the definition of failureMode.
Claim. The map assigning a failure mode to each of the nine cross-domain theorems is injective: if two theorems receive the same assigned failure mode then they are the same theorem.
background
The Option A Falsifier Registry maintains a finite pairing of C1-C9 cross-domain theorems with empirical test classes. Its purpose is to attach concrete falsifiers to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology. The failureMode definition supplies the concrete assignment by cases on each CombinationID, sending c1CognitiveTensor to singleAxisDecoderSuffices, c2PlanetStrata to noSmallPhiPowerRatio, and similarly for the remaining seven entries.
proof idea
The proof introduces two arbitrary CombinationIDs a and b together with the hypothesis that their images under failureMode coincide. It then performs case analysis on a and on b. Simplification with the definition of failureMode immediately yields a equals b.
why it matters
This injectivity result is invoked by falsifierRegistryCert, which certifies the registry by recording nine combinations, nine test classes, three statuses, nine dataset classes, and nine observables. It supplies the bookkeeping step that keeps each C1-C9 theorem paired with a unique empirical falsifier, fulfilling the module's stated goal of preventing drift into numerology. The declaration touches no forcing-chain step or phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.