mediumPriorityTests_length
The theorem establishes that the medium-priority empirical tests list contains exactly two entries. Researchers certifying the overall empirical queue coverage in Recognition Science cite this length when summing bucket sizes to confirm nine total tests. The proof evaluates the explicit list definition by direct decidable computation.
claimLet $M$ be the list of medium-priority empirical tests consisting of the cognitive tensor and universal response combinations. Then $|M| = 2$.
background
The module maintains a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. It records which protocols should be tested first and proves that every queued item is already covered by the formal empirical protocol. The upstream definition mediumPriorityTests constructs the list as [.c1CognitiveTensor, .c7UniversalResponse].
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate the length of the explicitly constructed list.
why it matters in Recognition Science
This length fact is invoked by priorityBucketTotal to obtain the total of nine tests across all priority buckets and by empiricalQueueCert to certify the queue structure. It fills the empirical validation layer for the C1-C9 theorems in the Recognition framework without supplying actual empirical data.
scope and limits
- Does not establish empirical validity of any listed test.
- Does not specify protocol details or measurement procedures.
- Does not address test ordering or execution sequence.
Lean usage
rw [mediumPriorityTests_length]formal statement (Lean)
109theorem mediumPriorityTests_length : mediumPriorityTests.length = 2 := by
proof body
Decided by rfl or decide.
110 decide
111