protocolSpec_eq_iff
plain-language theorem explainer
Equality between empirical protocols of two Option A combinations holds exactly when the combinations are identical. Researchers confirming unique falsifiable signatures for each implemented combination would cite this injectivity result. The proof constructs the biconditional by invoking the prior injectivity of protocolSpec in one direction and rewriting by equality in the other.
Claim. Let $a, b$ be elements of the inductive type of implemented Option A combinations. Let $P(c)$ be the empirical protocol record for combination $c$, consisting of its dataset class, predicted observable, and failure mode. Then $P(a) = P(b)$ if and only if $a = b$.
background
The Option A Empirical Protocol module associates each CombinationID with a ProtocolSpec record to encode falsifier protocols. CombinationID enumerates the implemented combinations (c1CognitiveTensor, c2PlanetStrata, c3OncologyTensor, c4QuantumMolecularDepth, c5AttentionTensor). The definition protocolSpec maps a combination to its ProtocolSpec by selecting the corresponding datasetClass, predictedObservable, and failureMode. An upstream theorem establishes that protocolSpec is injective, so distinct combinations produce distinct protocol records. The module setting requires total coverage of implemented Option A theorems by falsifier protocols, with zero sorrys or axioms.
proof idea
The term-mode proof constructs the biconditional. The forward direction applies the upstream injectivity theorem protocolSpec_injective directly to the equality hypothesis. The reverse direction rewrites the goal using the equality hypothesis on the combinations.
why it matters
This theorem supports the downstream empiricalProtocolCert definition, which certifies coverage for combinations including c1, c3, c5, and c8. It ensures that distinct combinations carry distinct empirical protocols, completing the formal requirement of total falsifier coverage stated in the module. Within the Recognition Science framework it secures unique observable signatures for the implemented combinations without overlap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.