proof

P09 Observational non-id.

Lean spine source

Declarations: P09_observational_equivalence_nonidentifiability

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P09_observational_equivalence_nonidentifiability
    {M₁ M₂ : Model}
    (hobs : ObservationallyEquivalent M₁ M₂)
    (hgoal : ModelGoal M₁ ≠ ModelGoal M₂) :
    ¬ IdentifiableFromObservations ModelGoal := by
  intro hId
  exact hgoal (hId M₁ M₂ hobs)

/-- A goal map is identifiable from access only if access-equivalent models agree. -/