module module high

`IndisputableMonolith.Foundation.OptionAEmpiricalQueue`

Module defines empirical priorities for implemented Option A combinations, extending the protocol's coverage claims. Test schedulers validating Recognition Science against data cite these assignments to rank falsification attempts. Content consists of type definitions and mappings with no theorems proved.

claimEmpirical priority function $empiricalPriority$ mapping implemented C1-C9 combinations to levels in type $Priority$, together with predicates $isImmediate$ and $isHighOrImmediate$.

background

The upstream Option A Empirical Protocol module converts the falsifier registry into Lean propositions, guaranteeing every implemented C1-C9 combination carries a dataset class, predicted observable, and failure mode. Data mappings remain empirical metadata while the formal content enforces total coverage with no gaps. This queue module sits in the foundation layer and introduces the Priority type plus the empiricalPriority assignment to classify tests for later scheduling.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

Supplies the priority queue to the downstream Option A Empirical Schedule module. That module fixes an explicit execution order for the first five high-value tests and proves every scheduled item is high-or-immediate and protocol-covered. It completes the priority assignment step in the empirical validation pipeline for Option A.

scope and limits

Does not contain experimental datasets or observables.
Does not prove theorems about the assigned priorities.
Does not address non-implemented Option A combinations.
Does not define test execution order or scheduling properties.

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