scheduled_program_ready
plain-language theorem explainer
The theorem states that for any combination identifier in the first-pass empirical schedule the readiness flag inside its program specification equals the comprehensive empirical readiness predicate. Researchers assembling the Option A test certificate cite this equality to confirm that scheduled rows carry the correct metadata flags before pipeline execution. The proof is a direct reflexivity reduction that follows from the aligned definitions of programSpec and empiricallyReady_all.
Claim. For every combination identifier $c$ belonging to the first-pass schedule, the readiness field of the program specification for $c$ equals the predicate asserting that $c$ satisfies empirical readiness in all required respects.
background
The module supplies a single certificate for the first-pass empirical program attached to Option A. ProgramSpec is the record type that bundles a CombinationID with its protocol specification, empirical priority, analysis action, and deliverable. EmpiricallyReady_all is the theorem that a given combination meets the full readiness predicate by satisfying protocol falsifiability, presence of an analysis action, a deliverable, and a pipeline. FirstPassSchedule is the concrete list of five CombinationID values that constitute the initial test order.
proof idea
The proof is a one-line reflexivity step. It holds immediately because the ready field inside the programSpec record is constructed to coincide with the value returned by empiricallyReady_all for the same combination identifier.
why it matters
This equality supplies the first_pass_ready field of the empiricalProgramCert certificate that collects injectivity, length, absence of duplicates, readiness, and completeness for the assembled first-pass program. It closes the readiness link in the metadata certification chain for the Option A empirical program. The supplied documentation flags no open questions at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.