Three Closure Nonimplications

Abstract

Prediction, operational, classical-answer, and self-description closure are separated by three concrete observer constructions.

Theorem 1.1 (Prediction, operation, classical answers, and self-description separate).

$$\left(\mathrm{predictionStableAt}\left((x\mapsto x-1),(x\mapsto unit),0\right)\wedge \mathrm{AlgebraAdjoin}\left(Complex,\mathrm{pair}\left(\mathrm{deterministicProjection}\left((x\mapsto unit),unit\right),\mathrm{shiftMatrix}\left(2\right)\right)\right)\ne \mathrm{top}\left(\mathrm{Matrix}\left(\mathrm{ZMod}\left(2\right),\mathrm{ZMod}\left(2\right),Complex\right)\right)\right)\wedge \left(\left(\mathrm{windowGeneratedAlgebra}\left(2\right)=\mathrm{top}\left(\mathrm{Matrix}\left(\mathrm{ZMod}\left(2\right),\mathrm{ZMod}\left(2\right),Complex\right)\right)\wedge \mathrm{IsEmpty}\left(\mathrm{ComplexAlgHom}\left(\mathrm{windowGeneratedAlgebra}\left(2\right),Complex\right)\right)\right)\wedge \left(\exists context\in \mathrm{Fin}\left(2\right)\to \mathrm{RankOneContext}\left(1\right),\mathrm{Injective}\left(\mathrm{contextReadout}\left(context\right)\right)\wedge \left(\exists evaluation\in \mathrm{Matrix}\left(\mathrm{Fin}\left(1\right),\mathrm{Fin}\left(1\right),Complex\right)\to \left(\mathrm{Matrix}\left(\mathrm{Fin}\left(1\right),\mathrm{Fin}\left(1\right),Complex\right)\to Bool\right),twist\in Bool\to Bool,\left(\forall y\in Bool,\mathrm{twist}\left(y\right)\ne y\right)\wedge \left(\neg (a\mapsto \mathrm{twist}\left(\mathrm{evaluation}\left(a,a\right)\right))\in \mathrm{range}\left(evaluation\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/Completion/ClosureNonimplicationTriple.closure_nonimplication_triple (✓ std3). ∎

Source. Repository-derived.

Commentary.

On the two-address cyclic carrier, the constant Unit readout is prediction-stable at depth zero. Its deterministic readout projection together with the cyclic shift generates a proper subalgebra: every generator commutes with the shift, whereas the frozen clock-shift commutator is nonzero.

The second countermodel applies the frozen nontrivial-window theorem: the canonical clock and shift generate the full matrix algebra, but that generated algebra has no unital complex character.

The third countermodel applies the frozen rank-one-context theorem. Its projector-trace readout is injective on the complete matrix carrier, while a Boolean evaluator indexed twice by that same carrier and a fixed-point-free twist exhibit an escaped diagonal.

Repository search found the three exact component owners but no whole-statement owner. Pinned Mathlib supplied only the generic commutation lemma for elements of a generated algebra.

References

• Truth anchor: D5/S3/Observer/Completion/ClosureNonimplicationTriple.closure_nonimplication_triple
• Dependency: D5/S3/Observer/WindowAlgebra/OperationalClassicalSeparation
• Dependency: D5/S3/ObserverMemory/Prediction/ConditionalEntropyStability
• Dependency: D5/S3/Quantum/Algebra/CovariantCommutator
• Dependency: D5/S3/Quantum/Measurements/DeterministicReadoutPvm
• Dependency: D5/S3/Quantum/Tomography/ObserverDiagonalSeparation