protocolSpec_injective
The mapping from combination identifiers to their empirical protocol records (dataset class, predicted observable, failure mode) is injective. Researchers formalizing falsifiable predictions for Option A in Recognition Science cite this to guarantee distinct combinations yield distinguishable experimental records. The proof is a term-mode reduction that applies injectivity of the dataset class map after congruence extraction of the dataset field from the protocol structure.
claimThe function sending each combination identifier $c$ to the record consisting of its dataset class, predicted observable, and failure mode is injective: if two identifiers produce identical records then the identifiers coincide.
background
The Option A Empirical Protocol module formalizes the falsifier registry as a Lean proposition that assigns to every implemented C1-C9 combination a dataset class, predicted observable, and failure mode. The ProtocolSpec structure packages these three components into a single decidable record. This construction rests on the prior result that the dataset class assignment itself is injective, together with the definition that extracts the dataset, observable, and failure fields from each combination identifier.
proof idea
The term proof assumes two combinations a and b map to the same protocol record, invokes the known injectivity of the dataset class function, and extracts the dataset component via congruence on the ProtocolSpec structure.
why it matters in Recognition Science
This injectivity feeds the pipeline specification injectivity theorem, the empirical protocol certificate, and the equivalence relating protocol equality to combination equality. It closes part of the formal coverage requirement that every implemented Option A theorem carries a distinct falsifier protocol, consistent with the framework demand for distinguishable empirical records across the phi-ladder combinations.
scope and limits
- Does not establish existence or content of the dataset classes themselves.
- Does not address physical realizability of the predicted observables.
- Does not extend injectivity to non-implemented combinations.
- Does not constrain the numerical values inside the failure modes.
Lean usage
apply protocolSpec_injective; exact congrArg PipelineSpec.protocol hformal statement (Lean)
68theorem protocolSpec_injective : Function.Injective protocolSpec := by
proof body
Term-mode proof.
69 intro a b h
70 apply datasetClass_injective
71 exact congrArg ProtocolSpec.dataset h
72
73/-- Equality of empirical protocols is exactly equality of combinations. -/