EmpiricalScheduleCert
plain-language theorem explainer
EmpiricalScheduleCert bundles the verification that the first-pass empirical test schedule has exactly five entries, begins with the oncology tensor test, continues with the Miller span and attention tensor tests, contains no duplicates, and includes precisely the high-or-immediate priority combinations that are protocol-falsifiable. Researchers validating Option A falsification protocols would cite this certificate to confirm the initial test sequence is well-defined and complete. The structure is defined by its fields, each satisfied by a set
Claim. Let $S$ be the ordered list of the first five empirical test combinations: oncology tensor, Miller span, attention tensor, regulatory ceiling, and planet strata. The certificate structure asserts that this list has length five, begins with the oncology tensor combination, has the Miller span combination in position one, the attention tensor in position two, contains no duplicate entries, includes a combination if and only if it has high or immediate priority, and every scheduled combination is protocol-falsifiable.
background
The Option A empirical schedule module fixes an explicit order for the first five high-value tests attached to the forcing chain. The list firstPassSchedule is defined as the concrete sequence oncology tensor, Miller span, attention tensor, regulatory ceiling, planet strata. A combination is high-or-immediate when its empirical priority equals immediate or high. ProtocolFalsifiable holds when the combination has an associated dataset class, predicted observable, and failure mode in the registry.
proof idea
This is a structure definition whose fields collect the required properties of the schedule list. Each field is discharged by a dedicated lemma on firstPassSchedule, such as the length lemma for the size assertion and the membership equivalence lemma for the exact high-or-immediate coverage condition. The concrete instance is assembled downstream by supplying those lemmas to the structure constructor.
why it matters
This definition locks the initial test order for Option A empirical validation, ensuring the sequence is fixed, complete for high-priority items, and covered by falsifiable protocols. It is instantiated by the downstream empiricalScheduleCert definition. In the Recognition Science framework it supports the empirical queue step that tests predictions from the eight-tick octave and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.