QIProtocol
plain-language theorem explainer
The QIProtocol inductive type enumerates the five canonical quantum information protocols in the RS framework. A physicist deriving the dimension of the quantum information space from the spatial dimension D would cite this enumeration to obtain the relation 5 = D + 2. The definition proceeds by a direct inductive introduction of the five constructors with automatic derivation of Fintype and equality structures.
Claim. Let $P$ be the finite set whose elements are the protocols teleportation, superdense coding, quantum key distribution, quantum error correction, and quantum sensing.
background
In the Recognition Science treatment of quantum information, entanglement is realized as a J-cost correlation between remote systems, where J denotes the uniqueness function J(x) = (x + x^{-1})/2 - 1 from the forcing chain. The module identifies the five listed protocols as the configuration dimension equal to D + 2, with D the number of spatial dimensions fixed at 3 by T8. This identification rests on the requirement that quantum teleportation uses an entangled pair together with classical communication, expressed in RS-native units.
proof idea
The declaration is an inductive definition that introduces five distinct constructors and derives DecidableEq, Repr, BEq, and Fintype automatically via the deriving clause.
why it matters
This enumeration supplies the finite set whose cardinality is asserted equal to 5 in qiProtocolCount and equal to D + 2 in qi_five_Dp2, thereby linking the quantum information protocols to the eight-tick octave and the spatial dimension D = 3. The same set appears inside the QITeleportCert structure that certifies the QI dimension for the S6 / B16 QC Depth section. It closes the enumeration step required for any downstream derivation of quantum teleportation from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.