EmpiricalProgramCert
plain-language theorem explainer
EmpiricalProgramCert is a record type that packages injectivity of programSpec, length-5 and duplicate-free firstPassProgram, FirstPassReady, FirstPassProgramComplete, schedule matching for ready and pipeline fields, plus nodup conditions on actions, deliverables and pipelines, together with the exact top-priority equivalence. Option A empirical pipeline authors cite it as the single metadata certificate confirming the assembled first-pass program is collision-free and complete. The definition is a direct bundling of lemmas already proved in先行
Claim. A structure $EmpiricalProgramCert$ whose fields assert: $programSpec$ is injective; $firstPassProgram$ has length 5 and is duplicate-free; $FirstPassReady$ and $FirstPassProgramComplete$ hold; for every $c$ in $firstPassSchedule$, $(programSpec c).ready = empiricallyReady_all c$ and $(programSpec c).pipeline = pipelineSpec c$; the lists $firstPassActions$, $firstPassDeliverables$ and $firstPassPipelines$ are duplicate-free; and $c$ belongs to $firstPassSchedule$ if and only if $isHighOrImmediate c$.
background
The module assembles a single certificate for the first-pass empirical program of Option A. Earlier files establish the queue, schedule, actions, deliverables, pipelines and readiness predicates separately; this structure simply records that the assembled program satisfies all metadata constraints at once. FirstPassProgramComplete is the conjunction FirstPassReady ∧ firstPassProgram.length = 5 ∧ firstPassProgram.Nodup ∧ firstPassActions.Nodup ∧ firstPassDeliverables.Nodup ∧ firstPassPipelines.Nodup ∧ (∀ c, c ∈ firstPassSchedule ↔ isHighOrImmediate c). Upstream lemmas supply firstPassProgram, firstPassActions, firstPassDeliverables, firstPassPipelines and pipelineSpec, each defined by mapping the schedule through the corresponding specification function.
proof idea
The declaration is a structure definition with no proof body. Its fields are populated by direct reference to the already-proved lemmas firstPassProgram_length, firstPassProgram_nodup, FirstPassReady, FirstPassProgramComplete, programSpec_injective, firstPassProgram_actions_nodup, firstPassProgram_deliverables_nodup, firstPassProgram_pipelines_nodup and the exact_top_priority equivalence.
why it matters
EmpiricalProgramCert supplies the single record consumed by the downstream definition empiricalProgramCert, which closes the first-pass verification inside OptionAEmpiricalProgram. It therefore completes the metadata layer of the Option A empirical pipeline before any runtime or measurement steps are considered. The certificate directly supports the Recognition Science foundation claim that the first-pass program is ready and collision-free, feeding the larger empirical-readiness gate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.