ProtocolFalsifiable
plain-language theorem explainer
ProtocolFalsifiable asserts that an Option A combination carries an assigned dataset class, predicted observable, and failure mode from the registry. Empirical physicists testing Recognition Science predictions would reference it to confirm each claim has a concrete falsification protocol. The definition is a direct existential unpacking of the three registry functions datasetClass, predictedObservable, and failureMode.
Claim. A combination $c$ is protocol-falsifiable when there exist a dataset class $d$, predicted observable $o$, and failure mode $f$ such that the registry satisfies datasetClass$(c)=d$, predictedObservable$(c)=o$, and failureMode$(c)=f$.
background
The Option A Empirical Protocol module converts the falsifier registry into Lean propositions that guarantee total coverage for implemented combinations. CombinationID is the inductive type listing active Option A claims (C1 cognitive tensor, C3 oncology tensor, C5 attention tensor, and C8 Miller span). DatasetClass enumerates the empirical data sources (EEG/MEG decoder corpus, seismic atmospheric catalog, TCGA clinical trials, quantum chemistry benchmarks, attention blink MEG). FailureMode records the empirical pattern that would refute the claim (single-axis decoder suffices, no small-phi power ratio, additive therapy response, depth exceeds five bits, non-forty plateau spectrum). PredictedObservable supplies the corresponding observable signature. This definition rests on the registry functions in OptionAFalsifierRegistry that perform the concrete assignments for each CombinationID.
proof idea
The definition is a direct existential statement over the three registry functions: datasetClass, predictedObservable, and failureMode applied to the input combination, conjoined by equality.
why it matters
ProtocolFalsifiable supplies the predicate used by EmpiricallyCovered, EmpiricalProtocolCert, and the concrete theorems c1_protocol, c3_protocol, c5_protocol, and c8_protocol. It records that every implemented Option A claim possesses an empirical falsifier, closing the coverage requirement stated in the module documentation. The construction aligns with the Recognition framework's demand for testable predictions without introducing new chain steps or open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.