proof

P36 Handle-operation ref.

Lean spine source

Declarations: P36_handle_operation_refines_identification

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 P36_handle_operation_refines_identification
    {A : AccessModel} {h : Handle} {u : Operation} {M₁ M₂ : Model}
    (hdist : HandleOperationDistinguishes A h u M₁ M₂) :
    IdentifiableWithHandleOperation A M₁ M₂ :=
  ⟨h, u, hdist⟩

/-- A raw boundary feature is identifiable under observation channel `K` only if
    `K`-equivalent boundaries agree on that feature. -/