firstPassSchedule_third
plain-language theorem explainer
The declaration confirms that the third entry (0-indexed) in the first-pass empirical schedule list equals the c5 Attention Tensor. Researchers constructing certified test sequences for Option A would cite this to lock the execution order of high-priority combinations. The proof is a one-line wrapper that applies the decide tactic directly to the explicit list definition.
Claim. Let $S$ denote the first-pass empirical schedule, the list $[c_3, c_8, c_5, c_9, c_2]$ where each $c_i$ is a CombinationID. Then the element at position 2 satisfies $S[2] = c_5$, with $c_5$ the Attention Tensor.
background
The module supplies an ordered schedule for the first five empirical tests attached to Option A. The upstream queue module assigns priorities; this module fixes an explicit execution order and proves every scheduled item is high-or-immediate and protocol-covered. The key upstream definition is the concrete list first-pass schedule := [c3OncologyTensor, c8MillerSpan, c5AttentionTensor, c9RegulatoryCeiling, c2PlanetStrata].
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic evaluates the list indexing operation against the explicit definition of the schedule and reduces the equality to a decidable proposition that holds by reflexivity.
why it matters
This result supplies the third field of the EmpiricalScheduleCert structure, which certifies length five, head c3, second c8, third c5, and absence of duplicates. It thereby anchors the explicit ordering for the high-value tests in the Option A empirical validation sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.