HasDeliverable
plain-language theorem explainer
HasDeliverable states that every CombinationID maps to some Deliverable artifact under the deliverableFor assignment. Researchers certifying completeness of the Option A empirical schedule cite it when building readiness predicates. The definition is realized directly as an existential quantifier over the fixed mapping from CombinationID to Deliverable.
Claim. For every combination identifier $c$, there exists a deliverable artifact $d$ such that the assignment function maps $c$ to $d$.
background
The module supplies concrete artifacts expected from the Option A empirical action plan and converts the first-pass schedule into an auditable set of outputs. Deliverable is the inductive type whose constructors are oncologyFactorModelNotebook, memoryCollapseNotebook, attentionPlateauPlot, regulatoryCeilingTable and planetPhiRatioTable. deliverableFor is the total function that sends each implemented CombinationID to one of these five artifacts; CombinationID itself enumerates the tested combinations with C10 retained only as commentary.
proof idea
The definition is a one-line wrapper that asserts existence of a Deliverable equal to the value returned by deliverableFor on the input CombinationID.
why it matters
HasDeliverable is invoked inside the definition of EmpiricallyReady and inside the structure EmpiricalDeliverablesCert that records nine deliverables together with injectivity of deliverableFor. It therefore supplies the concrete-output half of the Option A empirical deliverables required by the Recognition Science empirical action plan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.