proof

Access non-id.

Lean spine source

formal/AlignmentProofSpine/Boundaries.lean

Declarations: access_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 access_equivalence_nonidentifiability
    {A : AccessModel} {M₁ M₂ : Model}
    (heq : AccessEquivalent A M₁ M₂)
    (hgoal : ModelGoal M₁ ≠ ModelGoal M₂) :
    ¬ IdentifiableFromAccess A ModelGoal := by
  intro hId
  exact hgoal (hId M₁ M₂ heq)