c8_deliverable
plain-language theorem explainer
The deliverable assigned to the c8 Miller Span combination is fixed as the memory collapse notebook by the deliverableFor mapping. Researchers auditing the Option A empirical action plan would cite this assignment when confirming the first-pass schedule outputs. The proof reduces immediately by reflexivity to the case clause in the deliverableFor definition.
Claim. The deliverable assigned to the c8 Miller Span combination equals the memory collapse notebook: $deliverableFor(c8MillerSpan) = memoryCollapseNotebook$.
background
This 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 function deliverableFor maps each CombinationID to a Deliverable, with the explicit clause for c8MillerSpan returning the memory collapse notebook. The upstream deliverableFor definition enumerates the full list of assignments covering c3OncologyTensor, c8MillerSpan, c5AttentionTensor, c9RegulatoryCeiling, and c2PlanetStrata.
proof idea
One-line wrapper that applies reflexivity directly to the deliverableFor definition at the c8MillerSpan case.
why it matters
This result populates the empiricalDeliverablesCert structure that records nine deliverables, their injectivity, and the first-pass list properties. It thereby supports the auditable pipeline certification used in downstream empiricalPipelineCert. The assignment fits the Recognition Science empirical deliverables track for Option A without touching open questions on physical interpretation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.