protocolSpec_ne_of_ne
Distinct combinations of Option A parameters receive distinct empirical protocols under the protocolSpec mapping. Physicists auditing falsification protocols for cognitive, oncology, and attention tensors would cite this result to guarantee separation of dataset classes and failure modes. The proof reduces the inequality of protocols to the given inequality of combinations via the already-established injectivity of protocolSpec.
claimIf $a, b$ are distinct elements of CombinationID, then the associated empirical protocol records satisfy protocolSpec$(a) ≠$ protocolSpec$(b)$.
background
CombinationID is the inductive type enumerating the implemented Option A combinations, including c1CognitiveTensor, c3OncologyTensor, and c5AttentionTensor. The function protocolSpec maps each such combination to a ProtocolSpec record containing a dataset class, a predicted observable, and a failure mode. This module establishes that every implemented combination has a complete falsifier protocol, with no remaining axioms or sorrys. The upstream result protocolSpec_injective shows that protocolSpec is an injective function, meaning equal protocols imply equal combinations.
proof idea
The proof is a direct term-mode application: assume the protocols are equal, then apply the injectivity of protocolSpec to recover that the combinations are equal, contradicting the hypothesis.
why it matters in Recognition Science
This theorem supports the bundle of distinctness results for specific pairs such as c1 and c3, c3 and c5, and c5 and c8. It contributes to the claim that the empirical protocol coverage is total and that distinct combinations remain distinguishable by their falsification protocols. In the Recognition Science framework it ensures the empirical metadata layer preserves the separation of the underlying combination space.
scope and limits
- Does not specify the internal structure of the ProtocolSpec records.
- Does not prove existence of the protocols, only their distinctness given the mapping.
- Does not extend to unimplemented combinations such as C10.
- Does not address numerical predictions or data analysis.
Lean usage
theorem c1_c3_distinct : protocolSpec .c1CognitiveTensor ≠ protocolSpec .c3OncologyTensor := protocolSpec_ne_of_ne (by decide)formal statement (Lean)
83theorem protocolSpec_ne_of_ne {a b : CombinationID} (h : a ≠ b) :
84 protocolSpec a ≠ protocolSpec b := by
proof body
Term-mode proof.
85 intro hp
86 exact h (protocolSpec_injective hp)
87