firstPassDeliverables_eq
plain-language theorem explainer
The equality fixes the first-pass deliverables list to an explicit enumeration of five artifacts drawn from the Option A empirical plan. Downstream certification and length theorems in the same module cite it to anchor the initial output set. The proof reduces to a single decide tactic that evaluates the list equality by direct computation.
Claim. The list of first-pass deliverables equals the explicit list consisting of the oncology factor model notebook, the memory collapse notebook, the attention plateau plot, the regulatory ceiling table, and the planet phi ratio table.
background
The module supplies concrete artifacts expected from the Option A empirical action plan and converts the first-pass schedule into an auditable collection of outputs. The upstream definition firstPassDeliverables is obtained by mapping the first-pass schedule through the deliverableFor function, which produces the concrete list of five items. This establishes the initial empirical deliverables within the Recognition Science framework.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic succeeds because the right-hand side is an explicit list and the left-hand side is defined by a direct map, rendering the equality decidable by computation.
why it matters
This equality is referenced by the empiricalDeliverablesCert definition and by the firstPassDeliverables_length and firstPassDeliverables_nodup theorems. It supplies the concrete content for the first-pass schedule, completing the auditable output specification in the Option A deliverables module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.