empiricalProtocolCert
plain-language theorem explainer
The definition assembles a concrete certificate asserting that every implemented combination in Option A possesses a falsifiable protocol together with uniqueness and distinctness properties for the cognitive tensor, oncology tensor, attention tensor, and Miller span cases. A researcher formalizing empirical tests within the Recognition Science framework would cite it to confirm completeness of the falsifier registry with no gaps among the covered combinations. The construction proceeds by direct field assignment of the upstream coverage, falsi
Claim. Let $E$ be the structure whose fields comprise an empirical coverage predicate, falsifiability assertions for the C1 cognitive tensor protocol, the C3 oncology tensor protocol, the C5 attention tensor protocol and the C8 Miller span protocol, uniqueness of the protocol specification for each combination, injectivity of the protocol map, uniqueness for the C3 case, an equivalence relating protocol equality to combination equality, and pairwise distinctness of the protocol specifications for the pairs (C1,C3), (C3,C5) and (C5,C8). The term in question is the structure instance that populates these fields with the corresponding coverage theorems, uniqueness results and distinctness lemmas.
background
The module Option A Empirical Protocol converts the falsifier registry into a single Lean proposition guaranteeing that every implemented C1-C9 combination carries a dataset class, a predicted observable and an explicit failure mode. The central definitions are ProtocolFalsifiable (a predicate asserting that a given combination admits a falsifiable protocol) and ProtocolSpec (the concrete specification map from combinations to protocols). EmpiricallyCovered is the top-level predicate that all combinations are covered. Upstream results include the theorem c1_protocol, which states that the C1 cognitive tensor protocol is falsifiable by direct appeal to the universal falsifiability result protocolFalsifiable_all, and the analogous statements for C3, C5 and C8. Distinctness theorems establish that the protocol specifications for C1 and C3 differ, for C3 and C5 differ, and for C5 and C8 differ, each proved by reduction to the inequality of protocol specifications.
proof idea
The definition is a direct structure literal. It sets the all-covered field to the empirical coverage predicate and assigns each remaining field to the corresponding upstream theorem: the C1 coverage field receives the C1 protocol theorem, the C3 coverage field receives the C3 protocol theorem, the uniqueness field receives the unique protocol specification theorem, the distinctness fields receive the three pairwise distinctness theorems, and the injectivity and equivalence fields receive the protocol specification injectivity and equivalence lemmas.
why it matters
This definition supplies the single bundled certificate that realizes the module claim of total coverage: no implemented Option A theorem lacks a falsifier protocol. It serves as the concrete witness for the empirical protocol layer that any downstream formalization of Recognition Science falsification tests can invoke. The construction closes the formal gap between the abstract falsifier registry and the concrete C1-C8 protocols, supporting the overall claim that the Option A development is empirically grounded without remaining stubs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.