firstPassReady
plain-language theorem explainer
The declaration proves that every combination in the first-pass schedule satisfies the empirical readiness condition. Option A empirical pipeline certifiers would cite it to close the metadata readiness gate before data collection. The proof is a direct one-line application of the scheduled readiness lemma after introducing the combination and schedule membership.
Claim. $forall c in first-pass schedule, EmpiricallyReady(c)$, where a combination is empirically ready when it possesses a falsifier protocol, analysis action, deliverable artifact, and unified pipeline record.
background
The module sets a readiness gate for Option A empirical work. A combination meets the gate when it contains all four operational layers: falsifier protocol, analysis action, deliverable artifact, and unified pipeline record. The development reports zero sorrys and zero axioms. FirstPassReady is the proposition that the first-pass schedule is ready, i.e., every combination belonging to the schedule is empirically ready. This rests on the upstream scheduled_empiricallyReady theorem, which states that any combination in the first-pass schedule is empirically ready by direct appeal to the all-implemented readiness result.
proof idea
The proof introduces an arbitrary combination c together with the hypothesis that c belongs to the first-pass schedule, then applies the scheduled_empiricallyReady lemma directly to discharge the goal.
why it matters
The theorem supplies the first_pass_ready field inside empiricalProgramCert and is used to construct firstPassProgramComplete. It also appears inside empiricalReadinessCert together with allImplementedReady and the specific c3, c5, c8 readiness results. In the Recognition framework it certifies the foundational metadata layer for Option A empirical validation, confirming the protocol and pipeline records are in place before proceeding to actual measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.