firstPassDeliverables_length
plain-language theorem explainer
The theorem states that the list of first-pass deliverables has length five. Researchers certifying empirical outputs for Option A in Recognition Science would cite this when confirming the initial artifact count. The proof is a term-mode wrapper that rewrites via the explicit list equality and then decides the resulting numerical claim.
Claim. Let $L$ be the list obtained by mapping the deliverable constructor over the first-pass schedule. Then the cardinality of $L$ equals 5.
background
The module turns the Option A empirical action plan into concrete, auditable artifacts. The list of first-pass deliverables is generated by applying the deliverable constructor to each element of the first-pass schedule. An upstream equality theorem enumerates this list explicitly as five items: the oncology factor model notebook, memory collapse notebook, attention plateau plot, regulatory ceiling table, and one additional deliverable required to reach length five. The module documentation states that these are the 'Concrete artifacts expected from the Option A empirical action plan.'
proof idea
The proof is a one-line term wrapper. It rewrites the length expression using the upstream equality theorem that unfolds the list to its explicit five-element form, then applies the decide tactic to confirm the cardinality.
why it matters
This supplies the first_pass_length component inside the empiricalDeliverablesCert structure, which also records the total deliverable count, injectivity of the constructor, the explicit first-pass list, and absence of duplicates. It closes the first-pass schedule into a verifiable set of outputs. Within the Recognition framework it supports the empirical deliverables track of Option A by providing a countable, axiom-free starting point before further analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.