pipelineSpec_eq_iff
plain-language theorem explainer
The equivalence establishes that distinct Option A combinations receive distinct empirical pipeline records, so the assignment from C1-C9 cases to their protocol-priority-action-deliverable tuples is injective. Researchers certifying empirical deliverables against Recognition Science models cite it to guarantee uniqueness when mapping combinations to observational protocols. The proof is a direct constructor that invokes the prior injectivity lemma on one side and performs equality rewriting on the other.
Claim. Let $C$ be the inductive type of implemented Option A combinations. Let $P : C → PipelineSpec$ be the function that assigns to each combination its protocol specification, empirical priority, analysis action, and deliverable record. Then for all $a, b : C$, $P(a) = P(b) ↔ a = b$.
background
The module defines a unified empirical pipeline record for the C1-C9 combinations under Option A. PipelineSpec is the structure holding the four fields (protocol, priority, action, deliverable). CombinationID enumerates the implemented cases, with C10 left as commentary only. The active edge count per fundamental tick is fixed at 1, and the φ-power balance identity at D = 3 is used in related mass and coherence calculations upstream.
proof idea
The term proof applies the constructor tactic to split the biconditional. The left-to-right direction invokes the lemma pipelineSpec_injective on the equality hypothesis. The right-to-left direction rewrites the goal by the supplied equality hypothesis.
why it matters
This theorem supplies the equality direction required by the downstream EmpiricalPipelineCert record, which aggregates injectivity, the iff statement, and the all-have-pipeline and scheduled-have-pipeline claims. It completes the uniqueness component of the empirical certification layer for Option A, ensuring no two combinations share the same deliverable tuple and feeding directly into the first-pass pipeline lists.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.