empiricalProgramCert
plain-language theorem explainer
The declaration supplies a concrete certificate assembling all metadata properties of the first-pass empirical program for Option A. Researchers validating the Recognition Science empirical layer would cite it as the single reference object for program completeness and collision-freeness. The definition is a direct record construction that wires each field to a previously established lemma.
Claim. Let $EmpiricalProgramCert$ be the structure whose fields require that $programSpec$ is injective, the first-pass program has length 5 and contains no duplicates, satisfies readiness and completeness, the schedule meets readiness and pipeline conditions for every combination, action and deliverable classes are duplicate-free, pipeline records are duplicate-free, and the schedule selects precisely the high-or-immediate priorities. Then $empiricalProgramCert$ is the instance of this structure obtained by assigning each field the corresponding proved fact.
background
The module OptionAEmpiricalProgram constructs a single certificate for the first-pass empirical program attached to Option A. The structure $EmpiricalProgramCert$ collects the required properties: injectivity of $programSpec$, length of $firstPassProgram$ equal to 5, absence of duplicates in the program list, readiness via $FirstPassReady$, completeness via $FirstPassProgramComplete$, scheduled readiness and pipeline conditions, no duplicates among action classes, deliverable classes, and pipeline records, and exact selection of top-priority items.
proof idea
The definition is a record constructor that directly assigns each field of $EmpiricalProgramCert$ to the corresponding theorem: $program_injective$ to $programSpec_injective$, $first_pass_length$ to $firstPassProgram_length$, $first_pass_nodup$ to $firstPassProgram_nodup$, $first_pass_ready$ to $firstPassReady$, $first_pass_complete$ to $firstPassProgramComplete$, and the remaining nodup and priority fields to their respective lemmas.
why it matters
This declaration supplies the assembled certificate for the Option A empirical program, serving as the single reference point for the first-pass test suite. The module documentation states that the file proves the assembled first-pass program is complete and collision-free at the metadata layer. It closes the empirical readiness assembly step within the Recognition framework, though no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.