programSpec
The programSpec definition constructs the executable row for a given Option A combination by assembling its protocol, priority, analysis action, deliverable, pipeline, and readiness fields from the respective component specifications. Researchers validating empirical predictions in the Recognition Science framework would cite this when building the first-pass program list. The definition proceeds by direct record initialization that delegates each field to a specialized component function.
claimFor a combination identifier $c$, the program specification is the record with combination field $c$, protocol given by the protocol specification for $c$, priority by the empirical priority for $c$, action by the analysis action for $c$, deliverable by the deliverable assigned to $c$, pipeline by the pipeline specification for $c$, and ready status by the empirical readiness for $c$.
background
The Option A empirical program module provides a single certificate for the first-pass empirical program attached to Option A. A ProgramSpec is one executable row in this program, consisting of a combination identifier together with its protocol, priority, analysis action, deliverable, pipeline, and readiness status. The module proves that the assembled first-pass program is complete and collision-free at the metadata layer, with zero sorry or axiom statements.
proof idea
This definition is a direct record construction. It initializes the ProgramSpec structure by applying the component functions protocolSpec, empiricalPriority, analysisAction, deliverableFor, pipelineSpec, and empiricallyReady_all to the input combination identifier.
why it matters in Recognition Science
This definition supplies the uniform constructor used by firstPassProgram to generate the execution list and by EmpiricalProgramCert to certify injectivity, length five, noduplication, readiness, and completeness of the first-pass program. It closes the assembly step in the Option A empirical validation pipeline, linking the individual component specifications to the overall program certificate in the Recognition Science foundation.
scope and limits
- Does not prove injectivity or absence of duplicates in the resulting program.
- Does not specify the concrete mappings inside component functions such as analysisAction.
- Does not address runtime execution or data collection details.
- Does not connect to the core Recognition Science forcing chain or constants.
Lean usage
def firstPassProgram : List ProgramSpec := firstPassSchedule.map programSpecformal statement (Lean)
39def programSpec (c : CombinationID) : ProgramSpec where
40 combination := c
proof body
Definition body.
41 protocol := protocolSpec c
42 priority := empiricalPriority c
43 action := analysisAction c
44 deliverable := deliverableFor c
45 pipeline := pipelineSpec c
46 ready := empiricallyReady_all c
47