c8_dataset
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.