Experimental Quotient Characterization

Abstract

Experimental targets are exactly functions on the empirical quotient.

Theorem 1.1 (Experimental targets are quotient functions).

$$\begin{array}{r}\forall A:\mathrm{Type},X:\mathrm{Type},B:\mathrm{Type},Y:\mathrm{Type},\\ F:A\to \left(X\to X\right),O:X\to B,T:X\to Y,\\ (\forall a:\mathrm{List}(A),\exists !d_a:\mathrm{EmpiricalQuotient}(\mathrm{experimentTrace}(F,O))\to \mathrm{List}(B),\mathrm{experimentTrace}(F,O)(a)=d_a\circ \mathrm{empiricalClass}(\mathrm{experimentTrace}(F,O)))\wedge \\ [(\exists !d_T:\mathrm{EmpiricalQuotient}(\mathrm{experimentTrace}(F,O))\to Y,T=d_T\circ \mathrm{empiricalClass}(\mathrm{experimentTrace}(F,O))⟺\forall x:X,y:X,(\forall a:\mathrm{List}(A),\mathrm{experimentTrace}(F,O)(a,x)=\mathrm{experimentTrace}(F,O)(a,y))\Rightarrow T(x)=T(y))\wedge \\ ((\exists x:X,y:X,(\forall a:\mathrm{List}(A),\mathrm{experimentTrace}(F,O)(a,x)=\mathrm{experimentTrace}(F,O)(a,y))\wedge T(x)\ne T(y))\Rightarrow \neg \exists d:\mathrm{EmpiricalQuotient}(\mathrm{experimentTrace}(F,O))\to Y,T=d\circ \mathrm{empiricalClass}(\mathrm{experimentTrace}(F,O)))].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/InterventionLaws/ExperimentalQuotientCharacterization.experimental_quotient_characterization (✓ std3). ∎

Source. Repository-derived.

Commentary.

The protocol trace is the existing recursive trajectory constructed from the intervention channel and public readout. The quotient and class map are the canonical empirical objects for that trace.

Every trace coordinate has a unique quotient factor. For an arbitrary target, unique factorization is equivalent to constancy on states with every trace equal.

The final public clause is the converse obstruction: two states with all traces equal but different target values rule out every quotient factor for that target.

References

• Truth anchor: D5/S3/ConceptDynamics/InterventionLaws/ExperimentalQuotientCharacterization.experimental_quotient_characterization
• Dependency: D5/S3/ConceptDynamics/Interventions/ExperimentalQuotientUniversality