empiricalQueueCert
plain-language theorem explainer
The empirical queue certificate bundles priority assignments and protocol coverage for the C1-C9 cross-domain theorems into one structure. It specifies that four priorities exist, designates immediate and high-priority items for oncology tensor, Miller span, attention tensor, planet strata, and regulatory ceiling combinations, and asserts every combination admits a falsifiable protocol. Physicists validating the empirical side of Recognition Science would cite this to fix the testing order. The definition is a direct record construction that re
Claim. The empirical queue certificate is the structure satisfying: the priority type has cardinality 4; c3OncologyTensor and c8MillerSpan are immediate; c5AttentionTensor, c2PlanetStrata, and c9RegulatoryCeiling have high priority; every CombinationID admits a falsifiable protocol; and the counts of immediate, high, medium, and deferred tests match the exact sets defined by the priority function.
background
The module defines a priority queue for empirical tests attached to the C1-C9 cross-domain theorems. It records which protocols should be tested first and proves every queued item is already covered by the formal empirical protocol. The EmpiricalQueueCert structure requires four_priorities to be the cardinality of Priority, immediate and high classifications via isImmediate and empiricalPriority, all_have_protocol via ProtocolFalsifiable, and exact bucket counts via deferredTests_exact and similar lemmas. Upstream results supply the concrete assignments: c3_immediate states isImmediate .c3OncologyTensor := rfl; c2_high states empiricalPriority .c2PlanetStrata = .high := rfl; and deferredTests_exact proves membership in the deferred set by case analysis on CombinationID.
proof idea
The definition constructs the EmpiricalQueueCert record by direct field assignment. Each field receives the value of a prior sibling definition or theorem: four_priorities from priority_count, c3_now from c3_immediate, c5_next from c5_high, immediate_count from immediateTests_length, defer_exact from deferredTests_exact, and all_have_protocol from every_priority_has_protocol. No tactics or reductions are applied beyond the record syntax.
why it matters
This definition supplies the concrete certificate that every empirical test item for the C1-C9 theorems is already covered by a formal protocol and ordered by the four-priority scheme. It closes the empirical-queue interface in the foundation layer, preparing downstream claims that would invoke the certificate to assert testing readiness. The module doc-comment states the Lean status is zero sorry and zero axiom, confirming the coverage claim is fully formalised within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.