Invariant Origin Recovery Obstruction

Abstract

A transitive invariant readout cannot recover or duplicate a nontrivial origin.

Theorem 1.1 (No absolute-origin reconstruction).

$$\begin{array}{c}\forall G,A,Y:Type,\\ \mathrm{Group}(G)\wedge \mathrm{MulAction}(G,A)\wedge \mathrm{IsPretransitive}(G,A)\wedge \mathrm{Nontrivial}(A),\\ \forall q:A\to Y,(\forall g:G,a:A,q(\mathrm{smul}(g,a))=q(a))\Rightarrow \\ (\forall a,b:A,q(a)=q(b))\wedge \\ (\neg \exists d:Y\to A,\mathrm{LeftInverse}(d,q))\wedge \\ (\neg \exists C:Y\to A\times A,\forall a:A,C(q(a))=(a,a))\wedge \\ (\exists a,b:A,a\ne b\wedge q(a)=q(b)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Naturality/InvariantOriginRecoveryObstruction.no_absolute_origin_reconstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

A group G acts transitively on a nontrivial origin type A. The internal readout q is invariant under that action, so every two origins have the same internal description.

The declaration rules out both a left-inverse decoder and a duplicator that would return the ordered pair (a,a) from q(a). It also exposes two distinct origins with equal readout, retaining the relational coordinate distinction in the public statement.

References

• Truth anchor: D5/S3/Observer/Naturality/InvariantOriginRecoveryObstruction.no_absolute_origin_reconstruction
• Dependency: D5/S3/Observer/Completion/StructuralCompletionSignature