Dynamic Indistinguishability Coordinatewise

Abstract

Dynamic indistinguishability on an independent finite product is exactly coordinatewise, and factorwise action is necessary.

Theorem 1.1 (Dynamic indistinguishability is coordinatewise).

$$\forall k\in \mathbb{N},X\in \mathrm{Fin}(k)\to \mathrm{Type},O\in \mathrm{Fin}(k)\to \mathrm{Type},F\in \pi i:\mathrm{Fin}(k),X(i)\to X(i),q\in \pi i:\mathrm{Fin}(k),X(i)\to O(i),x\in \mathrm{ProductState}(X),y\in \mathrm{ProductState}(X),\mathrm{DynamicIndistinguishable}(\mathrm{coordinateUpdate}(F),\mathrm{coordinateReadout}(q),x,y)\iff \left(\forall i\in \mathrm{Fin}(k),\mathrm{DynamicIndistinguishable}(F(i),q(i),x(i),y(i))\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementGeometry/DynamicIndistinguishabilityCoordinatewise.dynamic_indistinguishability_iff_coordinatewise (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any finite index type and dependent state and output families, the update and readout are formed by applying their local maps at each coordinate.

Equality of every global readout at every time implies equality at each coordinate. Conversely, coordinatewise equality at every time gives equality of the dependent output functions by function extensionality.

The finite index may be empty; no primality, prime-power, finiteness of carriers, injectivity, surjectivity, or nonconstant readout is assumed.

Theorem 1.2 (Factorwise readout is necessary).

$$\mathrm{UpdateActsFactorwise}(id)\wedge \left(\left(\neg \mathrm{ReadoutActsFactorwise}(crossBooleanReadout)\right)\wedge \left(\neg \left(\mathrm{DynamicIndistinguishable}(id,crossBooleanReadout,booleanStateA,booleanStateB)\iff \left(\forall i\in \mathrm{Fin}(2),\mathrm{DynamicIndistinguishable}(id,constantFalse,booleanStateAi,booleanStateBi)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementGeometry/DynamicIndistinguishabilityCoordinatewise.readout_factorwise_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

On a two-coordinate Boolean product, the identity update and constant local readouts make every coordinate pair locally indistinguishable.

A cross-coordinate readout that repeats coordinate zero globally separates two such states at time zero. Thus the iff fails when the readout does not act factorwise.

Theorem 1.3 (Factorwise update is necessary).

$$\mathrm{ReadoutActsFactorwise}(firstCoordinateReadout)\wedge \left(\left(\neg \mathrm{UpdateActsFactorwise}(hiddenCrossUpdate)\right)\wedge \left(\neg \left(\mathrm{DynamicIndistinguishable}(hiddenCrossUpdate,firstCoordinateReadout,hiddenStateA,hiddenStateB)\iff \left(\forall i\in \mathrm{Fin}(2),\mathrm{DynamicIndistinguishable}(id,first,hiddenStateAi,hiddenStateBi)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementGeometry/DynamicIndistinguishabilityCoordinatewise.update_factorwise_is_necessary (✓ std3). ∎

Source. Repository-derived.

Commentary.

On a two-coordinate product of Boolean pairs, the first-coordinate readout is factorwise and the local updates are identities.

A cross-coordinate update copies a hidden second component into the other coordinate. The local relations remain true, but the global relation fails after one step, so factorwise updating is necessary.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementGeometry/DynamicIndistinguishabilityCoordinatewise.dynamic_indistinguishability_iff_coordinatewise
• Truth anchor: D5/S3/ConceptDynamics/RefinementGeometry/DynamicIndistinguishabilityCoordinatewise.readout_factorwise_is_necessary
• Truth anchor: D5/S3/ConceptDynamics/RefinementGeometry/DynamicIndistinguishabilityCoordinatewise.update_factorwise_is_necessary