EmpiricalDeliverablesCert
plain-language theorem explainer
The EmpiricalDeliverablesCert structure certifies an inventory of nine deliverable artifacts for Option A tests together with an injective assignment from combination identifiers. It fixes the first-pass list to five specific notebooks and tables, requires that list to be duplicate-free, and demands that every entry in the first-pass schedule possesses a deliverable. Researchers auditing the empirical action plan cite the certificate to confirm the mapping and schedule are internally consistent. The structure is assembled directly from sibling
Claim. A structure $C$ asserting: the set of deliverable artifacts has cardinality 9; the assignment from test combinations to artifacts is injective; the first-pass list equals [oncology factor model notebook, memory collapse notebook, attention plateau plot, regulatory ceiling table, planet phi ratio table]; that list has length 5 and contains no duplicates; every combination in the first-pass schedule has an associated artifact; and the oncology tensor, Miller span, and attention tensor combinations map to the oncology factor model notebook, memory collapse notebook, and attention plateau plot respectively.
background
The module supplies concrete artifacts expected from the Option A empirical action plan and converts the first-pass schedule into an auditable set of outputs. Deliverable is the inductive enumeration of nine artifact types (oncology factor model notebook through erikson reverse cohort table). The function deliverableFor maps each CombinationID to one of these artifacts; firstPassDeliverables is obtained by applying that map to firstPassSchedule. HasDeliverable c holds precisely when there exists an artifact d such that deliverableFor c equals d.
proof idea
The declaration is a structure definition whose fields directly embed the cardinality result deliverable_count, the injectivity lemma deliverableFor_injective, the equality firstPassDeliverables_eq, the length and nodup facts, and the explicit output mappings for three combinations. No tactics or reductions are required; the structure simply packages the already-proved sibling statements.
why it matters
The certificate is instantiated by the downstream definition empiricalDeliverablesCert, which assembles the fields from deliverable_count, deliverableFor_injective and firstPassDeliverables_eq. It supplies the auditable inventory required by the Option A empirical action plan inside the Recognition Science framework, closing the link between the first-pass schedule and concrete deliverables without addressing physical predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.