qiProtocolCount
plain-language theorem explainer
The declaration asserts that the finite set of quantum information protocols in the Recognition Science model has cardinality five. A researcher enumerating discrete protocol types from J-cost correlations would cite this count to confirm the protocol-space dimension. The proof is a direct decision procedure on the enumerated inductive type with its derived Fintype instance.
Claim. The set of quantum information protocols has cardinality five: $ |QIProtocol| = 5 $, where the protocols are teleportation, superdense coding, quantum key distribution, quantum error correction, and quantum sensing.
background
In the module on quantum teleportation from Recognition Science, protocols arise as discrete types from J-cost correlations between remote systems, with entanglement identified as such a correlation. The inductive type QIProtocol enumerates exactly five protocols: teleportation, superdense coding, QKD, QEC, and quantum sensing, each deriving DecidableEq, Repr, BEq, and Fintype. The module states that five protocols equal D plus two, where D is the spatial dimension fixed by the forcing chain at T8.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality of the finite type QIProtocol, using the Fintype instance generated from its five constructors.
why it matters
This count is referenced directly in the downstream definition qITeleportCert to certify the five-protocol structure alongside the relation five equals D plus two. It closes the link from the upstream PrimitiveDistinction axioms to the quantum-information dimension in the RS framework, where T8 sets D equal to three and the protocol count matches the configuration dimension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.