docs: PROOF_DIFFICULTY.md - mark MultiCarElevator partial

Update the entry for `MultiCarElevator/Elevator.tla:235` to reflect
the partial proof landed in `Elevator_proof.tla`:

  - TypeInvariant: fully proven (170 obligations)
  - SafetyInvariant: scaffolded (InitImpliesInv2 closed, 223 total;
    Inv2Next OMITTED)
  - TemporalInvariant: not addressed

Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>
Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

PROOF_DIFFICULTY.md

@@ -252,7 +252,7 @@ well-founded termination, or routine WF-based liveness.
 - `specifications/FiniteMonotonic/ReplicatedLog.tla:48` — `Spec => []TypeOK` (small but with monotonic data structures)
 - `specifications/FiniteMonotonic/DistributedReplicatedLog.tla:67` — `Spec => AllExtending` (WF liveness)
 - `specifications/CoffeeCan/CoffeeCan.tla:115` — `TypeInvariant /\ MonotonicDecrease /\ EventuallyTerminates /\ LoopInvariant /\ TerminationHypothesis` (mixed safety + termination)
-- `specifications/MultiCarElevator/Elevator.tla:235` — `Spec => [](TypeInvariant /\ SafetyInvariant /\ TemporalInvariant)`
+- `[partial]` `specifications/MultiCarElevator/Elevator.tla:235` — `Spec => [](TypeInvariant /\ SafetyInvariant /\ TemporalInvariant)`.  *In-progress in `Elevator_proof.tla`*: `THEOREM TypeCorrect == Spec => []TypeInvariant` is fully proven (170 obligations, ~30s) using a `WaitingFloor` strengthening (`~waiting => location \in Floor`).  The proof requires `ASSUME Floor \cap Elevator = {}` (left implicit in the spec; supplied by TLC via model values) and four `LEMMA fEval == ... PROOF OMITTED` primitives stating multi-arg function unfoldings (`GetDistance`, `GetDirection`, `CanServiceCall`, `PeopleWaiting`) that TLAPS' `BY DEF f` doesn't unfold.  `THEOREM SafetyCorrect == Spec => []SafetyInvariant` is scaffolded with the strengthened invariant `Inv2` plus seven mutually-inductive auxiliaries (`WaitingDestinationDistinct`, `DoorsOpen*`, `NoServiceableActiveCall`, `StationaryNoPassenger`, `PersonImpliesButton`); `InitImpliesInv2` is closed (53 additional obligations, 223 total) but `Inv2Next` is OMITTED -- the per-action case analysis is genuine Band-H work.  TemporalInvariant (liveness) not addressed.
 - `specifications/CheckpointCoordination/CheckpointCoordination.tla:527` — `Spec => /\ []TypeInvariant /\ []SafetyInvariant /\ []TemporalInvariant`
 - `specifications/ewd687a/EWD687a_proof.tla:553` & `specifications/ewd687a/EWD687a.tla:430` — `Spec => TreeWithRoot` (needs unfolding of `IsTreeWithRoot` / `SimplePath` from community Graphs module)