module module high

`IndisputableMonolith.Foundation.OptionAEmpiricalQueue`

This module assigns empirical priorities to the implemented Option A combinations C1-C9. It defines a Priority type along with the empiricalPriority function and predicates that mark items as immediate or high. Researchers formalizing falsification schedules for Recognition Science predictions would cite it to rank testable combinations. The module consists of definitions and direct coverage checks that extend the upstream protocol without new theorems.

claimThe map empiricalPriority assigns each implemented Option A combination $C_i$ ($i=1..9$) a value in the set {immediate, high}, together with the predicates isImmediate and isHighOrImmediate that select the subset of protocol-covered items ready for scheduling.

background

The upstream Option A Empirical Protocol module converts the falsifier registry into Lean propositions, guaranteeing that every implemented C1-C9 combination carries a dataset class, predicted observable, and failure mode. This queue module introduces the Priority type and the empiricalPriority function to rank those combinations for testing order. It also supplies the predicates isImmediate, isHighOrImmediate, and the coverage lemmas c3_immediate through c9_high that filter high-value tests while confirming protocol coverage.

proof idea

This is a definition module. It declares the Priority inductive type, the empiricalPriority function, and a collection of one-line lemmas that apply the protocol coverage results from the imported module to verify each priority classification.

why it matters in Recognition Science

This module supplies the priority assignments consumed by the downstream Option A Empirical Schedule module, which fixes an explicit execution order for the first five high-value tests and proves that every scheduled item is high-or-immediate and protocol-covered. It therefore bridges the protocol registry to the ordered falsification queue in the Option A chain.

scope and limits

Does not specify concrete datasets or observables attached to each C combination.
Does not derive physical constants or predictions.
Does not address non-implemented Option A variants.
Does not contain test execution or data-analysis logic.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.OptionAEmpiricalSchedule module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.OptionAEmpiricalProtocol module_import

declarations in this module (34)

inductive Priority L22
theorem priority_count L29
def empiricalPriority L33
def isImmediate L44
def isHighOrImmediate L47
theorem c3_immediate L50
theorem c8_immediate L52
theorem c5_high L54
theorem c2_high L56
theorem c9_high L58
theorem c3_protocol_covered L60
theorem c8_protocol_covered L64
theorem every_priority_has_protocol L68
theorem immediate_iff L73
theorem high_or_immediate_iff L78
def immediateTests L88
def highPriorityTests L92
def mediumPriorityTests L96
def deferredTests L100
theorem immediateTests_length L103
theorem highPriorityTests_length L106
theorem mediumPriorityTests_length L109
theorem deferredTests_length L112
theorem immediateTests_nodup L115
theorem highPriorityTests_nodup L118
theorem mediumPriorityTests_nodup L121
theorem deferredTests_nodup L124
theorem immediateTests_exact L127
theorem highPriorityTests_exact L131
theorem mediumPriorityTests_exact L135
theorem deferredTests_exact L139
theorem priorityBucketTotal L143
structure EmpiricalQueueCert L149
def empiricalQueueCert L182