module module high

`IndisputableMonolith.Foundation.OptionAFalsifierRegistry`

This module enumerates the implemented Option A combinations C1-C9 as the falsifier registry in Recognition Science. Researchers testing empirical coverage of the framework cite it to confirm no theorem lacks a protocol. It is a definition module consisting of enumerations and type aliases only.

claimThe Option A falsifier registry consists of the implemented combinations \(C_1,\dots,C_9\) (with \(C_{10}\) retained only as commentary).

background

The Foundation layer of Recognition Science defines Option A as a class of theorems requiring empirical falsification protocols. This module introduces the supporting types: CombinationID for labeling the nine active cases, together with TestClass, EmpiricalStatus, DatasetClass, PredictedObservable and FailureMode. These types map each combination to the metadata needed for dataset, observable and failure-mode declarations. The module imports only Mathlib and contains no theorems.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The registry is consumed by OptionAEmpiricalProtocol, whose doc-comment states that it turns the registry into a Lean proposition asserting total coverage: every implemented C1-C9 combination has a dataset class, predicted observable, and failure mode. This step closes the empirical loop for Option A within the Recognition Science forcing chain.

scope and limits

Does not treat C10 as an implemented combination.
Does not embed actual numerical data or measurement protocols.
Does not prove any falsification result; only registers metadata.
Does not extend the registry beyond the nine listed combinations.

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