PipelineSpec
plain-language theorem explainer
PipelineSpec assembles a complete empirical execution record for each Option A C1-C9 combination by bundling a protocol specification, execution priority, analysis action, and expected deliverable. Researchers validating Recognition Science predictions through scheduled empirical tests would cite this record when constructing pipelines or program rows. The declaration is a plain structure definition that derives decidable equality and representation with no proof obligations.
Claim. A complete empirical execution record is a 4-tuple consisting of a complete empirical protocol record (dataset class, predicted observable, failure mode), an execution urgency level (immediate, high, medium or defer), a coarse computational action (fit factor model, fit discrete collapse, plateau detection, count regulatory states or estimate phi power ratio), and an expected deliverable artifact (oncology factor model notebook, memory collapse notebook, attention plateau plot, regulatory ceiling table or planet phi ratio table).
background
The Option A Empirical Pipeline module supplies unified records for testing Recognition Science predictions across C1-C9 combinations. It explicitly ties together protocol, priority, analysis action, and deliverable for every implemented combination, with Lean status of zero sorry and zero axiom. ProtocolSpec is the structure holding dataset class, predicted observable and failure mode for one combination. Priority is the inductive type with levels immediate, high, medium, defer. AnalysisAction enumerates the coarse computational actions needed to test a protocol. Deliverable enumerates the expected output artifacts.
proof idea
The declaration is a structure definition that simply declares the four fields and requests automatic derivation of DecidableEq and Repr; it contains no computational body or proof obligations.
why it matters
PipelineSpec is the core record type instantiated inside pipelineSpec for each CombinationID and used to populate firstPassPipelines and ProgramSpec rows. It directly supports HasPipeline and the injective property of the assignment map. In the Recognition framework this structure operationalizes the empirical validation pipeline for Option A tests, ensuring each combination carries a defined protocol, priority, action and deliverable while maintaining the module's zero-sorry status.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.