scheduled_program_ready
plain-language theorem explainer
For any CombinationID in the first-pass schedule the ready flag of its program specification equals the full empirical readiness conjunction. Option A empirical validation work cites this to confirm the metadata layer is closed. The proof is a one-line reflexivity step.
Claim. For every combination identifier $c$ in the first-pass schedule, the readiness component of the program row assigned to $c$ equals the conjunction of protocol falsifiability, analysis action presence, deliverable presence, and pipeline presence for $c$.
background
The module supplies a single certificate for the first-pass empirical program of Option A. programSpec builds each row from combination, protocolSpec, empiricalPriority, analysisAction, and deliverableFor. empiricallyReady_all proves EmpiricallyReady $c$ by the four conjuncts protocolFalsifiable_all $c$, hasAnalysisAction_all $c$, hasDeliverable_all $c$, and hasPipeline_all $c$. firstPassSchedule enumerates the five implemented CombinationIDs; CombinationID is the inductive type of those combinations.
proof idea
One-line wrapper that applies rfl. The equality is definitionally true once programSpec and empiricallyReady_all are unfolded.
why it matters
The result supplies the readiness datum required by empiricalProgramCert, the top-level certificate that assembles injectivity, length, nodup, readiness, and completeness for the Option A program. It closes the metadata check inside the foundation layer before any physical interpretation. The module states zero sorrys and zero axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.