FirstPassReady
plain-language theorem explainer
The predicate holds precisely when every combination in the initial empirical test list meets the four-layer operational criteria of falsifier protocol, analysis action, deliverable artifact, and pipeline record. Option A empirical program certifiers reference this predicate inside the program certification structure to confirm the first batch is prepared. The definition consists of a direct universal quantification over the five-item schedule list.
Claim. Let $S$ denote the first-pass schedule. The predicate holds if and only if for every combination $c$ in $S$, $c$ has a falsifier protocol, an analysis action, a deliverable artifact, and a unified pipeline record.
background
The module supplies readiness gates for Option A empirical work. A combination satisfies the readiness criterion precisely when it possesses all four operational layers: falsifier protocol, analysis action, deliverable artifact, and unified pipeline record. The first-pass schedule is the concrete list of five combinations chosen for initial testing: oncology tensor, Miller span, attention tensor, regulatory ceiling, and planet strata.
proof idea
The definition is a direct universal quantification over the schedule list, requiring the four-layer conjunction for each entry.
why it matters
This definition supplies the first-pass readiness field required by the EmpiricalProgramCert structure, which also records program injectivity, length five, and absence of duplicates. It appears inside the FirstPassProgramComplete gate together with length and nodup conditions. The predicate closes the readiness check for the initial empirical batch, supporting overall program certification in the Option A pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.