Atoms of the Pullback Algebra

Abstract

Minimal nonempty events in the canonical pullback algebra are realized fibers.

Theorem 1.1 (Nonzero pullback atoms are exactly the realized fibers).

$$\begin{array}{c}\forall X,O:\mathrm{Type},q:X\to O,\\ \forall A:\mathrm{Set}(X),\\ (\mathrm{Nonempty}(A)\wedge A\in \mathrm{PullbackAlgebra}(q)\wedge \\ \forall C:\mathrm{Set}(X),\mathrm{Nonempty}(C)\wedge C\in \mathrm{PullbackAlgebra}(q)\wedge C\subseteq A\Rightarrow A\subseteq C)⟺\\ (\exists o:\mathrm{range}(q),A=\{x:X\mid q(x)=\mathrm{val}(o)\}).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementAlgebra/PullbackAlgebraFiberAtoms.nonzero_pullback_atoms_are_effective_fibers (✓ std3). ∎

Source. Repository-derived.

Commentary.

The pullback algebra is the repository’s canonical family of proposition-valued events that factor through the readout.

The left side states nonemptiness, pullback observability, and minimality against every nonempty observable subevent. The right side identifies the event with one fiber over a realized readout value.

A point in a nonempty minimal event selects its fiber. Fiber constancy puts that fiber inside the event, and minimality forces equality. Conversely, any nonempty observable subevent of a fiber contains the whole fiber.

No finiteness assumption is used: the characterization holds for arbitrary state and readout carriers, and therefore includes the finite-carrier corollary.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementAlgebra/PullbackAlgebraFiberAtoms.nonzero_pullback_atoms_are_effective_fibers
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition
• Dependency: D5/S3/ConceptDynamics/Dialectics/DeterministicInterfaceEquivalence