Parameterized option elimination with retained input

Option elimination retains the original input for the selected handler. The construction tests the tag and, on the some branch, computes the option again to extract its payload. Its bounds explicitly charge both computations, input retention, and the selected handler. Linear native tag extraction, payload extraction, and pairing costs are absorbed by the native calculus. The bounds are asymptotic expressions with existential machine constants, not exact step counts. No inhabitance assumption is imposed on the payload type. The rule is available to fun_prop, and option_match_to_elim brings a match on an option into its form.

Main results

• Turing.MultiTapeTM.ComputableInO.optionElimWithInput: selected-branch time and space bounds for option elimination retaining the original input.

References

Uses Christian Reitwiessner's native degree/resource calculus. The proof adapts CslibFrontier/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Option.lean while preserving arbitrary resource bounds.

theorem Turing.MultiTapeTM.ComputableInO.optionElimWithInput {α β γ : Type} {encA : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {value : α → Option β} {fallback : α → γ} {body : α → β → γ} {Tv Sv Tnone Snone : α → ℕ} {Tbody Sbody : α × β → ℕ} (hvalue : ComputableInO value encA (encOption encB) Tv Sv) (hfallback : ComputableInO fallback encA encC Tnone Snone) (hbody : ComputableInO (fun (p : α × β) => body p.1 p.2) (encPair encA encB) encC Tbody Sbody) : ComputableInO (fun (a : α) => (value a).elim (fallback a) (body a)) encA encC (fun (a : α) => 2 * Tv a + (encA a).length + (value a).elim (Tnone a) fun (b : β) => Tbody (a, b)) fun (a : α) => 2 * Sv a + (encA a).length + (value a).elim (Snone a) fun (b : β) => Sbody (a, b)

Eliminate an option while retaining the input. The conservative bound charges two option computations even on the none branch; it charges only the selected handler.