firstPassDeliverables
plain-language theorem explainer
The first-pass deliverables list is obtained by mapping the deliverable assignment function over the ordered list of five CombinationIDs in the initial empirical schedule. An auditor of the Option A empirical program would cite this list to confirm that each scheduled test produces a concrete, distinct artifact. The definition is a direct functional composition via list map.
Claim. Let $S$ be the ordered list of five CombinationIDs given by firstPassSchedule and let $f$ be the function deliverableFor that assigns a unique Deliverable artifact to each ID. Then firstPassDeliverables is the list $[f(c) : c ∈ S]$.
background
In this module Deliverable is an inductive type whose constructors name nine concrete artifacts expected from empirical analysis: oncologyFactorModelNotebook, memoryCollapseNotebook, attentionPlateauPlot, regulatoryCeilingTable, planetPhiRatioTable, and four others. The upstream firstPassSchedule supplies the fixed initial ordering of five CombinationIDs, while deliverableFor supplies the deterministic mapping from each ID to its assigned artifact. The module documentation states that the module turns the first-pass schedule into an auditable set of outputs.
proof idea
The definition is a one-line wrapper that applies the map operation from RSNative.Core to firstPassSchedule with deliverableFor as the element-wise transformation.
why it matters
This definition supplies the concrete list required by EmpiricalDeliverablesCert and by the FirstPassProgramComplete gate in the empirical program module. It thereby closes the link between the scheduled tests and their required output artifacts, ensuring the first-pass program remains collision-free and ready for certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.