empiricalScheduleCert
plain-language theorem explainer
The empiricalScheduleCert assembles the certified first-pass schedule for Option A by populating the EmpiricalScheduleCert structure with properties of the firstPassSchedule list. Physicists validating the empirical test sequence in Recognition Science would reference this certificate to confirm compliance with length, ordering, and priority constraints. The proof is a straightforward record construction that delegates each field to a separate decision-procedure theorem.
Claim. The certificate is the structure with length five, head entry the oncology tensor test, second entry the Miller span test, third entry the attention tensor test, no duplicates, every member high or immediate priority, exactly the high-or-immediate combinations, and every member protocol falsifiable.
background
The Option A Empirical Schedule module defines an ordered execution sequence for the initial five empirical tests attached to Option A. Priorities are assigned in the companion OptionAEmpiricalQueue module via the empiricalPriority function on CombinationID values. The firstPassSchedule supplies the explicit list, while EmpiricalScheduleCert packages its verified properties into a single record.
proof idea
This is a direct record construction. Each field receives the matching theorem: length_five from firstPassSchedule_length, head_c3 from firstPassSchedule_head, second_c8 from firstPassSchedule_second, third_c5 from firstPassSchedule_third, no_duplicates from firstPassSchedule_nodup, scheduled_high_or_immediate from firstPassSchedule_mem_high_or_immediate, schedule_exactly_top_priority from firstPassSchedule_mem_iff_high_or_immediate, and scheduled_protocol from firstPassSchedule_mem_protocol. All supporting theorems are decided automatically after simplification.
why it matters
This definition supplies the concrete schedule certificate required by the Option A empirical validation path. It completes the first-pass schedule construction within the foundation layer, ensuring the schedule satisfies the high-priority and protocol conditions needed for subsequent empirical falsification steps. No open questions are addressed; it is a terminal definition in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.