IndisputableMonolith.Foundation.OptionAEmpiricalProtocol
This module supplies the complete empirical protocol record attached to each C1-C9 cross-domain theorem combination. Cross-domain workers in Recognition Science cite it to keep every theorem paired with a concrete test class. The module is a pure definition bundle that imports the falsifier registry and exports the protocol objects used by the downstream queue.
claimThe module defines ProtocolSpec as the finite record pairing a C1-C9 theorem with its empirical test class, together with the canonical instance protocolSpec and the predicates ProtocolFalsifiable and ProtocolMatches that certify coverage.
background
The upstream Option A Falsifier Registry supplies the finite pairing of each C1-C9 cross-domain theorem with an empirical test class; its doc-comment states that the registry 'keeps the falsifiers attached to the Lean theorem bundle so the cross-domain work cannot drift into unfalsifiable numerology.' This module records the protocol for one such combination, introducing ProtocolSpec, protocolSpec, ProtocolFalsifiable, ProtocolMatches and the supporting lemmas protocolSpec_matches, uniqueProtocolSpec, protocolSpec_injective. The local setting is therefore the attachment of falsifiable empirical protocols to the formal theorem statements before any queuing or testing occurs.
proof idea
This is a definition module, no proofs. It consists of inductive definitions for ProtocolSpec and the associated predicates, plus straightforward lemmas establishing injectivity, distinctness of C1-C3 and C3-C5 instances, and matching.
why it matters in Recognition Science
The module feeds the Option A Empirical Queue, whose doc-comment states it 'records which protocols should be tested first and proves that every queued item is already covered by the formal empirical protocol.' It therefore supplies the concrete protocol objects required by the queue while preserving the falsifiability discipline established in the upstream registry.
scope and limits
- Does not prove any empirical claims or supply test data.
- Does not enumerate all possible combinations outside the C1-C9 set.
- Does not discharge the actual experimental verification steps.
- Does not replace the priority queue logic in the downstream module.
used by (1)
depends on (1)
declarations in this module (22)
-
structure
ProtocolSpec -
def
protocolSpec -
def
ProtocolFalsifiable -
theorem
protocolFalsifiable_all -
def
ProtocolMatches -
theorem
protocolSpec_matches -
theorem
uniqueProtocolSpec -
theorem
protocolSpec_injective -
theorem
protocolSpec_eq_iff -
theorem
protocolSpec_ne_of_ne -
theorem
c1_c3_protocol_distinct -
theorem
c3_c5_protocol_distinct -
theorem
c5_c8_protocol_distinct -
def
EmpiricallyCovered -
theorem
empiricallyCovered -
theorem
c1_protocol -
theorem
c3_protocol -
theorem
c5_protocol -
theorem
c8_protocol -
theorem
c3_uniqueProtocol -
structure
EmpiricalProtocolCert -
def
empiricalProtocolCert