Law Representations and the Canonical Quotient

Abstract

A law-determining representation refines the canonical law quotient.

Theorem 1.1 (Law-determining representations refine the canonical quotient).

$$\begin{gathered} \forall State,Representation,Law:Type, \\ Lambda:State\to Law,r:State\to Representation, \\ \varphi :Representation\to Law,Lambda=\varphi \circ r\Rightarrow \\ (\forall x,y:State,r\left(x\right)=r\left(y\right)\Rightarrow \mathrm{Lambda}\left(x\right)=\mathrm{Lambda}\left(y\right))\wedge \\ \mathrm{Injective}\left(\mathrm{kerLift}\left(Lambda\right)\right)\wedge Lambda=\mathrm{kerLift}\left(Lambda\right)\circ \mathrm{quotientProjection}\left(\ker \left(Lambda\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/DecisionRisk/LawRepresentationCanonicalQuotient.law_determining_representation_refines_canonical_law_quotient (✓ std3). ∎

Source. Repository-derived.

Commentary.

The complete experiment law is an arbitrary typed map from State to Law. A representation determines it through the displayed decodeLaw factorization.

Equal representation values therefore give equal complete laws. The same law map defines the canonical equality-kernel quotient; its Mathlib kerLift is injective and reconstructs the law after the quotient projection.

Thus the quotient retains exactly the state distinctions visible to the experiment law. No second law, quotient, or equivalence relation is introduced.

References

• Truth anchor: D5/S3/Estimation/DecisionRisk/LawRepresentationCanonicalQuotient.law_determining_representation_refines_canonical_law_quotient