structure ISAR.TransitionSystem : Type 1

A standard autonomous transition system.

• State : Type
• step : self.State → self.State → Prop

inductive ISAR.Reachable (TS : TransitionSystem) : TS.State → TS.State → Prop

Reflexive transitive closure of the transition relation.

• refl {TS : TransitionSystem} (s : TS.State) : Reachable TS s s
• tail {TS : TransitionSystem} (s1 s2 s3 : TS.State) : Reachable TS s1 s2 → TS.step s2 s3 → Reachable TS s1 s3

def ISAR.IsClosed (TS : TransitionSystem) (C : TS.State → Prop) : Prop

A subset of states C is closed under steps of the transition system.

Equations

• ISAR.IsClosed TS C = ∀ (s1 s2 : TS.State), C s1 → TS.step s1 s2 → C s2

theorem ISAR.closure_preserved_under_reachability (TS : TransitionSystem) (C : TS.State → Prop) (hc : IsClosed TS C) (s1 s2 : TS.State) : C s1 → Reachable TS s1 s2 → C s2

Forward Invariance of Closed Subsystems: If a system state-space subset C is closed under steps (forward invariant), then any state reachable from C remains in C.

structure ISAR.AnchorDependentSystem : Type 1

A transition system where transitions depend on an external anchor (environment/context).

• State : Type
• Anchor : Type
• step : self.State → self.Anchor → self.State → Prop

inductive ISAR.Trace (ADS : AnchorDependentSystem) : ADS.State → List ADS.Anchor → ADS.State → Prop

Trace of an anchor-dependent system under a sequence of anchors.

• nil {ADS : AnchorDependentSystem} (s : ADS.State) : Trace ADS s [] s
• cons {ADS : AnchorDependentSystem} (s1 s2 s3 : ADS.State) (a : ADS.Anchor) (as : List ADS.Anchor) : ADS.step s1 a s2 → Trace ADS s2 as s3 → Trace ADS s1 (a :: as) s3

theorem ISAR.referentially_open_requires_anchor (ADS : AnchorDependentSystem) (Obs : Type) (decode : ADS.State → Obs) (s s1' s2' : ADS.State) (as1 as2 : List ADS.Anchor) (_h1 : Trace ADS s as1 s1') (h2 : Trace ADS s as2 s2') (h_diff : decode s1' ≠ decode s2') : ∃ (as : List ADS.Anchor), ¬∀ (s' : ADS.State), Trace ADS s as s' → decode s' = decode s1'

Referentially Open Requires Anchor Theorem: If a state s can lead to different observations under different anchor sequences as1 and as2, then the trace semantics are not recoverable from the state alone (without the anchors).