Claim #39 — Verification of either::Either::inspect_right (with Aeneas be86ab0f1989d04944292b345b24c435be3ad10a)

Iterator::next writeback is a value/backward-state model guarantee under the supplied inner next dictionary, not verification of that concrete iterator or all Rust memory/external effects. No size_hint/len/count, finite-length or fused-iterator guarantee is added. For inspect_left/right, returning self in the extracted model must not be read as proving that callbacks cannot mutate interior/global state or that physical Rust payloads stay observationally unchanged. Only the forty-one mapped callables and their stated composition helpers are verified, not every public API. The new dispatch contracts establish branch/payload/context forwarding and modeled Result delegation, not arbitrary callback or Into correctness, success, termination, panic freedom or captured-state effects. Their normal-value theorems assume the selected call succeeds at that argument. No arbitrary mutable-context writeback or eager argument-construction claim is added. Rust Drop for discarded callbacks/payloads can panic, diverge or affect global state; destructor execution, unwind/return ordering, resource consumption and external effects are outside the value model. Modeled fail/div propagation is not a specification of every Rust panic payload or unwinding behavior. Default implementation values/termination/effects remain unverified. IntoEither uses the actual blanket dispatch, but its predicate/reference semantics retain the stated model boundary. Other inherent methods, iterator and pinning APIs, most trait/blanket implementations and serde remain unproved. into_inner still fails the untouched generated Lean do-match elaborator for the repeated T parameter; factor_ok/factor_err remain blocked by their current extraction/model limitations. All-feature/no-default configurations and other targets are not proved. The four reference-method results are supplementary model proofs only; ambiguous nominal source keys are not substituted for exact shared/mutable receiver identities. They do not guarantee arbitrary Clone correctness or termination, interior/global state preservation, Drop/panic/unwinding, external effects or physical aliasing/lifetimes. Backward-value equalities are not independent Rust memory proofs. The supplemental model and primary model are compiled in separate Lean module environments because their generated global discriminant-instance names collide on simultaneous import; no simultaneous model-equivalence bridge is claimed. The primary mappings now number41; next_back retains the selected dictionary and value-model assumptions, without arbitrary iterator termination, Drop/panic/unwinding, interior/global effect or independent memory guarantees.