firstPassSchedule_head
plain-language theorem explainer
The theorem asserts that the leading entry in the ordered list of first-pass empirical tests for Option A is the oncology tensor combination. Researchers validating the execution sequence of high-priority tests in the Recognition Science empirical protocol would cite this to anchor the schedule start. The proof is a one-line decision procedure that evaluates the concrete list head directly.
Claim. The head of the ordered list of first-pass empirical tests equals the oncology tensor combination: $head([oncology tensor, Miller span, attention tensor, regulatory ceiling, planet strata]) = oncology tensor$.
background
The module supplies an explicit ordered schedule for the first five empirical tests attached to Option A. The schedule is the concrete list beginning with the oncology tensor, followed by the Miller span, attention tensor, regulatory ceiling, and planet strata combinations. This ordering is fixed after the queue module assigns priorities, and the module proves that every entry is high-or-immediate and protocol-covered.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the equality between the list head accessor and the explicit first element of the schedule definition.
why it matters
The result is used directly to build the EmpiricalScheduleCert, which bundles length-five, head position, second and third positions, and no-duplicates properties. It supplies the concrete starting point for the Option A empirical sequence in the foundation layer and supports grounding of the forcing chain by fixing a testable test order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.