Claim #34 — Verification of either::Either::either_with (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-five 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 number45; next_back retains the selected dictionary and value-model assumptions, without arbitrary iterator termination, Drop/panic/unwinding, interior/global effect or independent memory guarantees. The two conversion contracts do not establish Iterator laws, callback correctness/termination, concrete iterator next/size_hint behavior, arbitrary Rust Drop/interior-mutability/global effects or independent heap/alias/provenance. The normal result depends only on the selected IntoIterator callback returning that value. IterEither operations with unresolved extraction assumptions are not verified by constructing the wrapper. The shared iter contract preserves the represented callback Result, including model failure/divergence/visible effects, but does not establish concrete callback correctness or termination, iterator laws/operations, physical shared-reference identity or lifetime/alias safety, or arbitrary Rust Drop/interior-mutability/global effects. iter_mut remains unsupported because its official generated backward-pair use does not match the standard dictionary result type; no mutable mapping or model repair is claimed. The factor_iter result does not establish callback correctness or termination, produced iterator operations/ordering, physical shared-reference identity or lifetime/alias safety, or arbitrary Rust Drop/interior-mutability/global effects. Its two Item families are independent; no additional same-Item condition is imposed. Shared iter retains its own original equal-Item bound. Unsupported mutable iter_mut is still excluded, and constructing IterEither does not prove its next implementation.