Native case analysis for solver work codes

Reuse the existing native sum projections and option elimination to retain captured work data while branching on a tag. The fallback only makes the intermediate double-option operation total; sum exhaustiveness proves that execution never uses it. This bookkeeping is original. No new machine primitive or global automation rule is introduced.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeCases.sumElimSnd {α β γ δ : Type} {ea : α ↪ List Bool} {eb : β ↪ List Bool} {eg : γ ↪ List Bool} {ed : δ ↪ List Bool} (fallback : δ) {left : γ → α → δ} {right : γ → β → δ} (hl : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : γ × α) => left p.1 p.2) (Turing.MultiTapeTM.encPair eg ea) ed) (hr : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : γ × β) => right p.1 p.2) (Turing.MultiTapeTM.encPair eg eb) ed) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : γ × (α ⊕ β)) => Sum.elim (left p.1) (right p.1) p.2) (Turing.MultiTapeTM.encPair eg (Turing.MultiTapeTM.encSum ea eb)) ed

Native tagged-sum case analysis retaining the original captured input.

theorem Cslib.Complexity.CSP.EdgeSolver.NativeCases.sumElimWithInput {α β γ δ : Type} {ea : α ↪ List Bool} {eb : β ↪ List Bool} {eg : γ ↪ List Bool} {ed : δ ↪ List Bool} (fallback : δ) {value : γ → α ⊕ β} {left : γ → α → δ} {right : γ → β → δ} (hv : Turing.MultiTapeTM.ComputableInPolyTime value eg (Turing.MultiTapeTM.encSum ea eb)) (hl : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : γ × α) => left p.1 p.2) (Turing.MultiTapeTM.encPair eg ea) ed) (hr : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : γ × β) => right p.1 p.2) (Turing.MultiTapeTM.encPair eg eb) ed) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : γ) => Sum.elim (left p) (right p) (value p)) eg ed

Native case analysis on a computed sum, retaining captured original inputs. The fallback only totalizes the existing projection/option implementation and is unreachable for sums.