Observer and Concept Readout Correspondence

Abstract

Concepts embed as singleton observers and observer identity descends to a quotient.

Theorem 1.1 (Embedding, forgetting, and relative identity).

$$\begin{array}{c}\forall X,C,I:\mathrm{Type},\\ B:I\to \mathrm{Type},q:X\to C,a:X,\\ O:\mathrm{ObserverStructure}\left(X,I,B\right),\\ E:=\mathrm{conceptObserver}\left(q,a\right),\\ J:=\mathrm{jointReadout}\left(\mathrm{readout}\left(O\right)\right),p:=\mathrm{quotientClassMap}\left(J\right),\\ [(\mathrm{readout}\left(E\right)\left(unit\right)=q\wedge \left(\mathrm{admissible}\left(E\right)=\Lambda k,True\wedge \mathrm{anchor}\left(E\right)=a\right))\wedge \\ (\forall x\in X,y\in X,\mathrm{jointReadout}\left(\mathrm{readout}\left(E\right)\right)\left(x\right)=\mathrm{jointReadout}\left(\mathrm{readout}\left(E\right)\right)\left(y\right)\iff q\left(x\right)=q\left(y\right))\wedge \\ (\forall x\in X,y\in X,p\left(x\right)=p\left(y\right)\iff \mathrm{jointReadout}\left(\mathrm{readout}\left(O\right)\right)\left(x\right)=\mathrm{jointReadout}\left(\mathrm{readout}\left(O\right)\right)\left(y\right))\wedge \\ (\exists O1,O2:\mathrm{ObserverStructure}\left(Bool,Unit,\Lambda k,Bool\right),\mathrm{admissible}\left(O1\right)\ne \mathrm{admissible}\left(O2\right)\wedge \ker \left(\mathrm{jointReadout}\left(\mathrm{readout}\left(O1\right)\right)\right)=\ker \left(\mathrm{jointReadout}\left(\mathrm{readout}\left(O2\right)\right)\right))\wedge \\ (\exists O1,O2:\mathrm{ObserverStructure}\left(Bool,Unit,\Lambda k,Unit\right),\mathrm{anchor}\left(O1\right)\ne \mathrm{anchor}\left(O2\right)\wedge \ker \left(\mathrm{jointReadout}\left(\mathrm{readout}\left(O1\right)\right)\right)=\ker \left(\mathrm{jointReadout}\left(\mathrm{readout}\left(O2\right)\right)\right))\wedge \\ (\exists r,s:Bool\to \left(Bool\to Bool\right),r\ne s\wedge \ker \left(\mathrm{jointReadout}\left(r\right)\right)=\ker \left(\mathrm{jointReadout}\left(s\right)\right))].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Fibers/ObserverConceptReadoutCorrespondence.observer_concept_readout_correspondence (✓ std3). ∎

Source. Repository-derived.

Commentary.

The singleton observer is public through its computation rules: its sole readout is the supplied concept, its admission predicate is universally true, and its anchor is the supplied state.

For an arbitrary dependent readout family, forgetting forms the canonical quotient projection by the kernel of the joint readout. Equality in that quotient is exactly observer-relative identity.

Three explicit Boolean countermodels show that equal readout kernels do not retain admission, anchor, or the coordinate decomposition of the joint readout.

References

• Truth anchor: D5/S3/ConceptDynamics/Fibers/ObserverConceptReadoutCorrespondence.observer_concept_readout_correspondence
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion