Fiber-Internal Paths

Abstract

Paths whose edges stay inside readout fibers cannot change the observed coordinate.

Theorem 1.1 (Fiber-internal paths preserve the readout).

$$\begin{gathered} \forall edge:State\to State\to Prop,readout:\mathrm{Concept}\left(State,Coordinate\right), \\ first,last:State,(\mathrm{FiberInternal}\left(edge,readout\right)\wedge \mathrm{ReflTransGen}\left(edge,first,last\right))\Rightarrow \\ \mathrm{readout}\left(first\right)=\mathrm{readout}\left(last\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DagSemantics/FiberInternalPaths.readout_eq_of_reachable (✓ std3). ∎

Source. Repository-derived.

Commentary.

Quantify a state relation and a readout, and assume every direct edge stays inside one readout fiber. A reflexive-transitive path then connects states with equal readout values.

The conclusion states equality only for the supplied path endpoints. It does not assert that equal readouts create a path in the reverse direction.

References

• Truth anchor: D5/S3/ConceptDynamics/DagSemantics/FiberInternalPaths.readout_eq_of_reachable
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition