c8_dataset
The c8_dataset theorem records that the Miller-Span combination maps to the working memory perturbation dataset class inside the Option A falsifier registry. Cross-domain theorists cite this assignment when attaching an empirical test to the c8 result. The equality is immediate from the case definition of datasetClass.
claimThe dataset class assigned to the Miller-Span combination equals the working memory perturbation class: $datasetClass(c8MillerSpan) = workingMemoryPerturbation$.
background
The Option A Falsifier Registry pairs each of the nine C1-C9 cross-domain theorems with a concrete empirical test class. Its purpose is to keep the theoretical claims attached to falsifiable observables and prevent drift into unfalsifiable numerology. The datasetClass function is defined by exhaustive case analysis on CombinationID, with the c8 entry explicitly returning the working memory perturbation class.
proof idea
One-line wrapper that applies reflexivity to the datasetClass definition for the c8 case.
why it matters in Recognition Science
This entry populates the falsifier registry whose counts are certified by falsifierRegistryCert. It supplies the concrete empirical anchor for the c8 theorem, satisfying the module requirement that every cross-domain result remain linked to a testable dataset class.
scope and limits
- Does not prove the empirical validity of the working memory perturbation test.
- Does not specify the internal structure or size of the Miller-Span dataset.
- Does not derive any other combination's dataset class.
formal statement (Lean)
202theorem c8_dataset :
203 datasetClass .c8MillerSpan = .workingMemoryPerturbation := rfl
proof body
204