deliverableFor
plain-language theorem explainer
deliverableFor assigns each Option A combination identifier to one of nine concrete empirical artifacts. Researchers auditing the empirical validation schedule cite it to fix the required outputs for each test case in the first-pass plan. The definition is a direct exhaustive pattern match on the CombinationID constructors with no auxiliary lemmas.
Claim. The function $deliverableFor : CombinationID → Deliverable$ is defined by cases on the nine constructors of CombinationID, sending c3OncologyTensor to oncologyFactorModelNotebook, c8MillerSpan to memoryCollapseNotebook, c5AttentionTensor to attentionPlateauPlot, and likewise for the remaining six combinations.
background
The Option A Empirical Deliverables module converts the first-pass schedule into an auditable collection of outputs. CombinationID is the inductive enumeration of implemented test cases drawn from the falsifier registry (C1–C9; C10 remains commentary). Deliverable is the inductive type whose nine constructors name the expected artifacts: oncologyFactorModelNotebook, memoryCollapseNotebook, attentionPlateauPlot, regulatoryCeilingTable, planetPhiRatioTable, cognitiveDecoderBenchmark, responseCoefficientPanel, quantumAddressingBenchmark, and eriksonReverseCohortTable.
proof idea
The definition proceeds by exhaustive pattern matching on each constructor of CombinationID, returning the matching Deliverable constructor in every branch. No lemmas or tactics are applied; the assignment is purely definitional.
why it matters
deliverableFor supplies the concrete mapping required by EmpiricalDeliverablesCert, firstPassDeliverables, and the family of equality theorems (c3_deliverable, c5_deliverable, c8_deliverable). It thereby anchors the empirical action plan inside the Recognition Science foundation, linking abstract combination identifiers to the specific notebooks, plots, and tables that must be produced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.