deliverableFor_injective
plain-language theorem explainer
The function mapping each of the five Option A combinations to its assigned deliverable is injective. Researchers auditing the empirical validation schedule in Recognition Science would cite this to confirm the nine outputs remain distinct. The result supports construction of the deliverables certificate. The proof proceeds by exhaustive case analysis on the two input combinations followed by simplification using the definition of the assignment function.
Claim. The function that assigns to each Option A combination identifier one of the five concrete deliverables (oncology notebook, memory collapse notebook, attention plateau plot, regulatory table, or planet ratio table) is injective.
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 assignment function is defined by case distinction on the five CombinationID constructors, sending each to a distinct Deliverable such as oncologyFactorModelNotebook or planetPhiRatioTable. This injectivity theorem is the only upstream dependency and is invoked directly when the certificate is assembled.
proof idea
The term proof introduces two arbitrary combinations a and b together with the assumption that their images are equal, performs exhaustive case analysis on both, and simplifies using the definition of the assignment function to obtain a equals b.
why it matters
The theorem populates the deliverable_injective field inside the empiricalDeliverablesCert definition, which also records the count, the first-pass equality, length, and noduplicate properties. It thereby completes the auditable-outputs component of the Option A empirical action plan within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.