scheduled_has_pipeline
plain-language theorem explainer
Any Option A combination appearing in the first-pass empirical test order has a complete pipeline record. Researchers validating the C1-C9 empirical suite cite this to confirm that scheduled tests carry full instrumentation. The proof is a direct one-line application of the universal pipeline existence result to the scheduled element.
Claim. For every implemented Option A combination identifier that belongs to the initial empirical test ordering, there exists a pipeline specification record such that the specification for that combination equals the record.
background
The module records a unified empirical pipeline for each implemented Option A combination (C1-C9), linking protocol, priority, analysis action, and deliverable. HasPipeline for a given combination holds precisely when a PipelineSpec record exists for it. The first-pass schedule is the concrete list of five combinations chosen for initial empirical testing; the universal result states that every combination identifier possesses such a record.
proof idea
One-line term wrapper that applies the universal pipeline existence theorem directly to the supplied combination identifier.
why it matters
The result supplies the scheduled_have_pipeline field inside the empiricalPipelineCert definition, which assembles injectivity, equivalence, universal coverage, and first-pass length into a single certificate. It thereby closes the scheduled portion of the Option A empirical pipeline record described in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.