Finite Protocol Compression

Abstract

A finite protocol quotient has an exact certificate with at most one fewer protocols than classes.

Theorem 1.1 (Finite quotients admit sharp protocol certificates).

$$\begin{array}{r}\forall Protocol,State,Observation:\mathrm{Type},\\ [\mathrm{Finite}State],Q:\mathrm{Set}(Protocol),e:Protocol\to State\to Observation,\\ \exists Q0:\mathrm{Finset}(Protocol),\\ \mathrm{subset}(Q0,Q)\wedge \\ \mathrm{experimentIndistinguishability}(Q0,e)=\mathrm{experimentIndistinguishability}(Q,e)\wedge \\ \mathrm{card}(Q0)\le \mathrm{card}(\mathrm{ProtocolQuotient}(Q,e))-1.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProtocolEvaluation/FiniteProtocolCompression.finite_protocol_subfamily_card_le_quotient_card_sub_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite state carrier, let K(Q) be equality of all evaluation readouts indexed by the available protocol family Q. The quotient is the actual quotient of the state carrier by this kernel.

There is a finite selected protocol family contained in Q whose kernel equals K(Q), and its cardinality is at most the number of quotient classes minus one.

References

• Truth anchor: D5/S3/Observer/ProtocolEvaluation/FiniteProtocolCompression.finite_protocol_subfamily_card_le_quotient_card_sub_one
• Dependency: D5/S3/ConceptDynamics/Experiment/ExperimentExpansionMonotonicity
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion
• Dependency: D5/S3/ConceptDynamics/Refinement/StrictRefinementBound
• Dependency: D5/S3/ObserverMemory/PredictionCertificates/FiniteDistinguishingCertificate