Dense-overlay control instructions

theorem Complexity.RAM.RegisterStore.Machine.denseZeroJumpInstructionTM_hoareTime_frame {n : ℕ} (tapes : ControlInstructionTapes n) (input : List Bool) (overlay : Store) (pcValue source target : ℕ) (initialWork : Fin n → Tape) (out₀ : Tape) (hvalid : DenseOverlay.Valid overlay) (hready : ControlInstructionReady tapes overlay pcValue initialWork) (houtput : TM.Parked out₀) : (denseZeroJumpInstructionTM tapes source target).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ work = initialWork ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool input)).move Dir3.right ∧ ControlInstructionResult tapes overlay (if DenseOverlay.read input overlay source = 0 then target else pcValue + 1) initialWork work ∧ out = out₀) (denseZeroJumpInstructionTime tapes input overlay pcValue source target)

A dense-overlay conditional read implements jz and restores the shared lookup ABI after the program-counter branch.