firstPassDeliverables_nodup
plain-language theorem explainer
The theorem asserts that the explicit list of four first-pass deliverables contains no repeated entries. Researchers certifying the Option A empirical program would cite it to confirm the schedule produces distinct artifacts. The proof reduces the abstract list to its concrete four-element form via the equality lemma and then decides the no-duplicates property by direct computation.
Claim. Let $D$ be the list consisting of the oncology factor model notebook, the memory collapse notebook, the attention plateau plot, and the regulatory ceiling table. Then $D$ contains no duplicate elements.
background
The module defines concrete artifacts expected from the Option A empirical action plan and converts the first-pass schedule into an auditable set of outputs. The list in question is obtained by applying the deliverableFor map to the first-pass schedule, which the equality theorem expands to the four-item sequence above. Upstream results include the definition of active edges per tick (A = 1) in the Masses and Modal modules together with the spectral-peak class from AsteroidOreSpectroscopy, all of which supply the integration context for the deliverables.
proof idea
The proof is a one-line wrapper that applies the equality theorem firstPassDeliverables_eq to replace the abstract list with its explicit four-element form, after which the decide tactic confirms the no-duplicates property by direct computation.
why it matters
The result is invoked inside empiricalDeliverablesCert and inside the proof of firstPassProgramComplete, which together certify that the first-pass program is complete and auditable. It supplies the required uniqueness property for the deliverables list in the Option A empirical module, closing one concrete step in the foundation layer that supports empirical validation within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.