empiricalPipelineCert
plain-language theorem explainer
This definition assembles a concrete record instance of EmpiricalPipelineCert that bundles injectivity of pipelineSpec, equivalence of specifications, universal coverage for CombinationID, first-pass schedule properties, and concrete priority-action-deliverable assignments for C3 and C8. Researchers validating the Option A empirical protocol in Recognition Science would reference it to confirm the pipeline meets its structural invariants. The construction is a direct record literal delegating each field to a prior sibling definition or rfl-equa
Claim. Let $E$ be the structure requiring: pipelineSpec to be injective, pipelineSpec $a$ = pipelineSpec $b$ iff $a=b$ for CombinationID $a,b$, every CombinationID has a pipeline, every scheduled combination has a pipeline, firstPassPipelines has length 5 and is nodup, (pipelineSpec .c3OncologyTensor).priority = immediate and its action = fitFactorModel with deliverable = oncologyFactorModelNotebook, and likewise for .c8MillerSpan with priority immediate, action fitDiscreteCollapse and deliverable memoryCollapseNotebook. Then empiricalPipelineCert is the record satisfying all these properties.
background
The module defines a unified empirical pipeline record for C1-C9 that ties protocol, priority, analysis action, and deliverable together for every implemented Option A combination. EmpiricalPipelineCert is the structure whose fields encode these requirements: pipeline_injective asserts Function.Injective pipelineSpec, pipeline_eq_iff gives the biconditional equivalence, all_have_pipeline and scheduled_have_pipeline assert coverage, first_pass_length and first_pass_nodup fix the schedule size and uniqueness, while c3_priority, c3_action, c3_deliverable and their C8 counterparts fix the concrete assignments. Upstream results supply the concrete values via rfl: c3_action states analysisAction .c3OncologyTensor = .fitFactorModel, c8_action states analysisAction .c8MillerSpan = .fitDiscreteCollapse, and the corresponding deliverable theorems fix the notebook outputs.
proof idea
The definition constructs the record by direct field assignment. Each field of EmpiricalPipelineCert receives the value of a sibling definition or theorem already proved in the module: pipeline_injective receives pipelineSpec_injective, pipeline_eq_iff receives pipelineSpec_eq_iff, all_have_pipeline receives hasPipeline_all, scheduled_have_pipeline receives scheduled_has_pipeline, first_pass_length receives firstPassPipelines_length, first_pass_nodup receives firstPassPipelines_nodup, and the C3/C8 priority-action-deliverable fields receive the corresponding c3_pipeline_* and c8_pipeline_* theorems.
why it matters
This declaration supplies the single certificate that unifies the Option A empirical pipeline, closing the structural requirements stated in the module documentation for C1-C9. It sits at the end of the foundation layer that assembles actions from OptionAEmpiricalActionPlan and deliverables from OptionAEmpiricalDeliverables. Within the Recognition Science framework it supports the empirical validation step that follows the forcing chain (T0-T8) and the Recognition Composition Law by giving a concrete, checkable record for the phi-ladder mass and Berry-threshold predictions. No downstream uses are recorded yet; the declaration therefore functions as the canonical reference point for any later empirical certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.