module module high

`IndisputableMonolith.Foundation.OptionAFalsifierRegistry`

This module registers the implemented Option A combinations C1 through C9 as the core falsifier registry in the Recognition Science foundation. A researcher testing empirical coverage of Option A would cite it to confirm that each combination carries an associated dataset class, predicted observable, and failure mode. The structure leaves C10 as commentary only and supplies the metadata skeleton that downstream protocols consume. It is a pure definition module with no proofs.

claimRegistry of implemented Option A combinations $C_1$ to $C_9$, each equipped with a dataset class, predicted observable, and failure mode; $C_{10}$ retained solely as commentary.

background

Recognition Science derives physics from the forcing chain T0-T8, with Option A combinations arising as concrete instances of the J-cost and phi-ladder constructions. The module introduces the supporting types: CombinationID enumerates the nine implemented cases, TestClass and DatasetClass label the empirical probes, EmpiricalStatus tracks coverage, PredictedObservable names the measurable signature, and FailureMode specifies the falsifying observation. These definitions sit inside the Foundation layer and import only Mathlib, supplying the structural interface that converts theoretical combinations into falsifiable statements.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the registry consumed by the Option A Empirical Protocol, which asserts total coverage: every implemented C1-C9 combination possesses a dataset class, predicted observable, and failure mode. It closes the formal loop from the unified forcing chain to empirical falsification, ensuring no implemented Option A result lacks a corresponding test protocol. The construction directly supports the framework's claim that the phi-ladder and mass formulas remain empirically accessible.

scope and limits

Does not include C10 as an implemented formal combination.
Does not embed actual empirical datasets or numerical data.
Does not prove any theorems about the combinations themselves.
Does not extend the registry beyond the nine listed cases.

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