firstPassPipelines_length
plain-language theorem explainer
The declaration establishes that the list of first-pass pipeline records contains exactly five entries. Researchers certifying the empirical structure of Option A combinations in the Recognition Science framework would cite it to confirm schedule completeness. The argument reduces the length claim by expanding the map definition over the schedule and substituting the upstream schedule length result.
Claim. Let $L$ be the list obtained by applying the pipeline specification constructor to each entry of the first-pass schedule $S$. Then $|L| = 5$.
background
The module constructs unified empirical pipeline records for C1-C9. This ties together protocol, priority, analysis action, and deliverable for every implemented Option A combination. The first-pass pipelines list consists of the records in schedule order. An upstream result shows that the first-pass schedule itself has length five via direct decision.
proof idea
Unfold the definition of the first-pass pipelines list to expose the map over the schedule. Rewrite using the length of a mapped list, then substitute the value five supplied by the schedule length theorem.
why it matters
This length fact populates the first-pass length field inside the empirical pipeline certificate. The certificate aggregates injectivity, equivalence conditions, and scheduling invariants to validate the Option A deliverables. It supports the framework's claim of complete coverage for the initial pipeline pass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.