hasDeliverable_all
plain-language theorem explainer
Every Option A combination identifier possesses an assigned deliverable artifact. Researchers validating the empirical action plan in Recognition Science would cite this to confirm that scheduled tests yield concrete outputs. The proof is a one-line wrapper that directly constructs the existential witness from the deliverable assignment function and reflexivity.
Claim. For every combination identifier $c$, there exists a deliverable $d$ such that the deliverable assigned to $c$ equals $d$.
background
This module converts the first-pass schedule into an auditable set of outputs for the Option A empirical action plan. HasDeliverable $c$ is the proposition asserting existence of a Deliverable $d$ with deliverableFor $c = d$. The function deliverableFor is defined by cases on CombinationID, sending c3OncologyTensor to oncologyFactorModelNotebook, c8MillerSpan to memoryCollapseNotebook, c5AttentionTensor to attentionPlateauPlot, c9RegulatoryCeiling to regulatoryCeilingTable, and c2PlanetStrata to planetPhiRatioTable. CombinationID is the inductive type enumerating the implemented combinations.
proof idea
The proof is a one-line wrapper that applies exact to the term ⟨deliverableFor c, rfl⟩, directly supplying the witness required by the existential definition of HasDeliverable.
why it matters
This result supplies the deliverable component used by scheduled_has_deliverable for members of firstPassSchedule and by empiricallyReady_all, which bundles it with protocol falsifiability, analysis actions, and pipeline checks. It ensures the Option A plan produces verifiable artifacts inside the Recognition Science framework, closing one link in the empirical deliverables chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.