proof

P09 Observational non-id.

Lean spine source

formal/AlignmentProofSpine/Boundaries.lean

Declarations: P09_observational_equivalence_nonidentifiability

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). 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. -/