module module high

`IndisputableMonolith.Foundation.OptionAFalsifierRegistry`

This module registers the implemented Option A combinations C1-C9 with their test classes, dataset classes, predicted observables, and failure modes. Researchers auditing empirical coverage of Recognition Science predictions would cite it to verify that no formal Option A result lacks a falsifier protocol. It is a definition module consisting of enumerations and counts with no theorems.

claimRegistry of falsifiers for Option A: $C_i$ ($i=1$ to $9$) each mapped to a DatasetClass, PredictedObservable, and FailureMode, with CombinationID, EmpiricalStatus, and TestClass as supporting enumerations (C10 remains commentary).

background

The module sits in the Foundation layer and introduces the core enumerations needed to attach empirical protocols to Option A results. CombinationID labels each implemented combination; TestClass and DatasetClass categorize the required observations; EmpiricalStatus records implementation state; PredictedObservable names the measurable quantity; and FailureMode specifies the concrete disconfirmation condition. The module doc comment states that C10 was left as commentary. No upstream lemmas are imported.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The registry supplies the concrete mappings consumed by the OptionAEmpiricalProtocol module. That protocol converts the registry into a Lean proposition asserting total coverage: every implemented C1-C9 combination possesses a dataset class, predicted observable, and failure mode. It thereby closes the empirical-metadata requirement for the Option A branch of the Recognition framework.

scope and limits

Does not include C10 as an implemented formal combination.
Does not contain actual numerical datasets or measurement protocols.
Does not prove that the listed observables are experimentally accessible.
Does not address Option B or later branches of the framework.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.OptionAEmpiricalProtocol module_import

declarations in this module (35)

inductive CombinationID L19
theorem combinationID_count L31
inductive TestClass L35
theorem testClass_count L47
inductive EmpiricalStatus L51
theorem empiricalStatus_count L57
inductive DatasetClass L61
theorem datasetClass_count L73
inductive PredictedObservable L77
theorem predictedObservable_count L89
inductive FailureMode L93
theorem failureMode_count L105
def falsifierClass L109
def empiricalStatus L122
def datasetClass L134
def predictedObservable L146
def failureMode L158
theorem c1_falsifier L169
theorem c2_falsifier L172
theorem c3_falsifier L175
theorem c4_falsifier L178
theorem c5_falsifier L181
theorem c6_falsifier L184
theorem c7_falsifier L187
theorem c8_falsifier L190
theorem c9_falsifier L193
theorem c3_observable L196
theorem c5_failure L199
theorem c8_dataset L202
theorem falsifierClass_injective L205
theorem datasetClass_injective L209
theorem predictedObservable_injective L213
theorem failureMode_injective L217
structure FalsifierRegistryCert L221
def falsifierRegistryCert L248