State-Protocol Quotient Order Commutation

Abstract

Quotienting equal evaluation rows and columns commutes by canonical carrier equivalences.

Theorem 1.1 (The two quotient orders are canonically equivalent).

$$\begin{array}{r}\forall State,Protocol,Value:\mathrm{Type},\\ \forall e:State\to Protocol\to Value,\\ (\forall x:State,\mathrm{stateOrderEquiv}(e)(\mathrm{QuotientMk}(\ker (e),x))=\mathrm{QuotientMk}(\mathrm{stateAfterProtocolSetoid}(e),x))\wedge \\ (\forall p:Protocol,\mathrm{protocolOrderEquiv}(e)(\mathrm{QuotientMk}(\mathrm{protocolAfterStateSetoid}(e),p))=\mathrm{QuotientMk}(\ker (\Lambda p,\Lambda x,e(x,p)),p))\wedge \\ (\forall xbar:\mathrm{Quotient}(\ker (e)),pbar:\mathrm{Quotient}(\mathrm{protocolAfterStateSetoid}(e)),\mathrm{stateFirstEvaluation}(e,xbar,pbar)=\mathrm{protocolFirstEvaluation}(e,\mathrm{stateOrderEquiv}(e)(xbar),\mathrm{protocolOrderEquiv}(e)(pbar))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Refinement/StateProtocolQuotientOrderCommutation.state_protocol_quotient_order_commutes (✓ std3). ∎

Source. Repository-derived.

Commentary.

The state and protocol relations are constructed from equality of the evaluation rows and columns. Each second-stage relation tests the induced evaluation on every class of the first quotient.

The two comparison equivalences are the identity on representatives. Their displayed computation rules make both carrier isomorphisms canonical, while the final conjunct identifies the two descended evaluation maps under those equivalences.

References

• Truth anchor: D5/S3/Observer/Refinement/StateProtocolQuotientOrderCommutation.state_protocol_quotient_order_commutes
• Dependency: D5/S3/Observer/Refinement/DoubleExtensionalEvaluationDescent