qi_five_Dp2
plain-language theorem explainer
The theorem shows that the inductive type enumerating the five canonical quantum information protocols has cardinality exactly five. A researcher deriving quantum protocols from Recognition Science would cite it to anchor the relation five equals D plus two. The proof is a one-line decide tactic that evaluates the cardinality from the derived Fintype instance on the inductive definition.
Claim. Let QIProtocol be the inductive type with constructors teleportation, superdenseCoding, QKD, QEC, and quantumSensing. Then the finite cardinality satisfies $|$QIProtocol$| = 5$.
background
The module defines quantum teleportation in RS via J-cost correlations for entanglement, requiring an entangled pair plus classical communication. Five protocols (teleportation, superdense coding, quantum key distribution, quantum error correction, quantum sensing) are collected into the inductive type QIProtocol, which derives DecidableEq, Repr, BEq, and Fintype. The local convention is that this count equals configDim D plus two, with D the spatial dimension fixed at three by the upstream forcing chain.
proof idea
The proof is a one-line wrapper that applies the decide tactic. Decide computes the cardinality directly from the Fintype instance generated by the five constructors of QIProtocol.
why it matters
The result is referenced inside qITeleportCert to supply the five_Dp2 field of the certification record. It supplies the concrete count that realizes the module claim five protocols equals D plus two, tying the protocol enumeration to the Recognition Science landmarks of D equals three and the eight-tick octave. No open scaffolding questions are closed by this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.