scheduled_has_deliverable
plain-language theorem explainer
Every combination identifier in the first-pass empirical schedule possesses an associated deliverable artifact. Researchers validating Option A empirical outputs would cite this result to confirm that scheduled tests produce auditable artifacts. The proof is a direct one-line application of the universal hasDeliverable_all lemma.
Claim. For every combination identifier $c$ belonging to the first-pass schedule, there exists a deliverable $d$ such that deliverableFor $c = d$.
background
This module supplies concrete artifacts for the Option A empirical action plan and converts the first-pass schedule into an auditable collection of outputs. HasDeliverable is the proposition that a scheduled test has a deliverable artifact, defined as the existence of a Deliverable equal to the value of deliverableFor at that combination. The firstPassSchedule is the explicit list of initial test combinations (c3OncologyTensor, c8MillerSpan, c5AttentionTensor, c9RegulatoryCeiling, c2PlanetStrata). The upstream theorem hasDeliverable_all states that HasDeliverable holds for every CombinationID by construction of deliverableFor.
proof idea
The proof is a one-line wrapper that applies hasDeliverable_all directly to the input combination c.
why it matters
The result guarantees that every entry in the first-pass schedule yields a deliverable, which is required by the downstream empiricalDeliverablesCert that assembles the full certification record (deliverable count, injectivity, first-pass equality, length, and noduplicates). It closes the auditable-outputs requirement for Option A without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.